(0) Obligation:

Clauses:

div(X1, 0, X2, X3) :- failure(a).
div(0, Y, 0, 0) :- no(zero(Y)).
div(X, Y, s(Z), R) :- ','(no(zero(X)), ','(no(zero(Y)), ','(minus(X, Y, U), ','(!, div(U, Y, Z, R))))).
div(X, Y, X4, X) :- ','(no(zero(X)), no(zero(Y))).
minus(X, 0, X).
minus(s(X), s(Y), Z) :- minus(X, Y, Z).
failure(b).
zero(0).
no(X) :- ','(X, ','(!, failure(a))).
no(X5).

Queries:

div(g,g,a,a).

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph.

(2) Obligation:

Clauses:

div1(0, T10, 0, 0).
div1(s(T29), s(0), s(T15), T16) :- div1(T29, s(0), T15, T16).
div1(s(s(T32)), s(s(0)), s(T15), T16) :- div1(T32, s(s(0)), T15, T16).
div1(s(s(s(T35))), s(s(s(0))), s(T15), T16) :- div1(T35, s(s(s(0))), T15, T16).
div1(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16) :- div1(T38, s(s(s(s(0)))), T15, T16).
div1(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16) :- div1(T41, s(s(s(s(s(0))))), T15, T16).
div1(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16) :- div1(T44, s(s(s(s(s(s(0)))))), T15, T16).
div1(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) :- minus107(T45, T46, X121).
div1(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) :- ','(minus107(T45, T46, T48), div1(T48, s(T47), T15, T16)).
div1(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56))))))).
div1(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63)))))).
div1(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70))))).
div1(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77)))).
div1(s(s(T84)), s(s(T86)), T82, s(s(T84))).
div1(s(T91), s(T93), T89, s(T91)).
div1(T98, T100, T96, T98).
div1(T105, T107, T103, T105).
minus107(T49, 0, T49).
minus107(s(T50), s(T51), X131) :- minus107(T50, T51, X131).

Queries:

div1(g,g,a,a).

(3) PrologToPiTRSProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
div1_in: (b,b,f,f) (b,f,f,f)
minus107_in: (b,b,f) (b,f,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

div1_in_ggaa(0, T10, 0, 0) → div1_out_ggaa(0, T10, 0, 0)
div1_in_ggaa(s(T29), s(0), s(T15), T16) → U1_ggaa(T29, T15, T16, div1_in_ggaa(T29, s(0), T15, T16))
div1_in_ggaa(s(s(T32)), s(s(0)), s(T15), T16) → U2_ggaa(T32, T15, T16, div1_in_ggaa(T32, s(s(0)), T15, T16))
div1_in_ggaa(s(s(s(T35))), s(s(s(0))), s(T15), T16) → U3_ggaa(T35, T15, T16, div1_in_ggaa(T35, s(s(s(0))), T15, T16))
div1_in_ggaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16) → U4_ggaa(T38, T15, T16, div1_in_ggaa(T38, s(s(s(s(0)))), T15, T16))
div1_in_ggaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16) → U5_ggaa(T41, T15, T16, div1_in_ggaa(T41, s(s(s(s(s(0))))), T15, T16))
div1_in_ggaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16) → U6_ggaa(T44, T15, T16, div1_in_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16))
div1_in_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U7_ggaa(T45, T46, T15, T16, minus107_in_gga(T45, T46, X121))
minus107_in_gga(T49, 0, T49) → minus107_out_gga(T49, 0, T49)
minus107_in_gga(s(T50), s(T51), X131) → U10_gga(T50, T51, X131, minus107_in_gga(T50, T51, X131))
U10_gga(T50, T51, X131, minus107_out_gga(T50, T51, X131)) → minus107_out_gga(s(T50), s(T51), X131)
U7_ggaa(T45, T46, T15, T16, minus107_out_gga(T45, T46, X121)) → div1_out_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
div1_in_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U8_ggaa(T45, T46, T15, T16, minus107_in_gga(T45, T46, T48))
U8_ggaa(T45, T46, T15, T16, minus107_out_gga(T45, T46, T48)) → U9_ggaa(T45, T46, T15, T16, div1_in_gaaa(T48, s(T47), T15, T16))
div1_in_gaaa(0, T10, 0, 0) → div1_out_gaaa(0, T10, 0, 0)
div1_in_gaaa(s(T29), s(0), s(T15), T16) → U1_gaaa(T29, T15, T16, div1_in_ggaa(T29, s(0), T15, T16))
div1_in_ggaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56))))))) → div1_out_ggaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56)))))))
div1_in_ggaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63)))))) → div1_out_ggaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63))))))
div1_in_ggaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70))))) → div1_out_ggaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70)))))
div1_in_ggaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77)))) → div1_out_ggaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77))))
div1_in_ggaa(s(s(T84)), s(s(T86)), T82, s(s(T84))) → div1_out_ggaa(s(s(T84)), s(s(T86)), T82, s(s(T84)))
div1_in_ggaa(s(T91), s(T93), T89, s(T91)) → div1_out_ggaa(s(T91), s(T93), T89, s(T91))
div1_in_ggaa(T98, T100, T96, T98) → div1_out_ggaa(T98, T100, T96, T98)
U1_gaaa(T29, T15, T16, div1_out_ggaa(T29, s(0), T15, T16)) → div1_out_gaaa(s(T29), s(0), s(T15), T16)
div1_in_gaaa(s(s(T32)), s(s(0)), s(T15), T16) → U2_gaaa(T32, T15, T16, div1_in_ggaa(T32, s(s(0)), T15, T16))
U2_gaaa(T32, T15, T16, div1_out_ggaa(T32, s(s(0)), T15, T16)) → div1_out_gaaa(s(s(T32)), s(s(0)), s(T15), T16)
div1_in_gaaa(s(s(s(T35))), s(s(s(0))), s(T15), T16) → U3_gaaa(T35, T15, T16, div1_in_ggaa(T35, s(s(s(0))), T15, T16))
U3_gaaa(T35, T15, T16, div1_out_ggaa(T35, s(s(s(0))), T15, T16)) → div1_out_gaaa(s(s(s(T35))), s(s(s(0))), s(T15), T16)
div1_in_gaaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16) → U4_gaaa(T38, T15, T16, div1_in_ggaa(T38, s(s(s(s(0)))), T15, T16))
U4_gaaa(T38, T15, T16, div1_out_ggaa(T38, s(s(s(s(0)))), T15, T16)) → div1_out_gaaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16) → U5_gaaa(T41, T15, T16, div1_in_ggaa(T41, s(s(s(s(s(0))))), T15, T16))
U5_gaaa(T41, T15, T16, div1_out_ggaa(T41, s(s(s(s(s(0))))), T15, T16)) → div1_out_gaaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16) → U6_gaaa(T44, T15, T16, div1_in_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16))
U6_gaaa(T44, T15, T16, div1_out_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16)) → div1_out_gaaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U7_gaaa(T45, T46, T15, T16, minus107_in_gaa(T45, T46, X121))
minus107_in_gaa(T49, 0, T49) → minus107_out_gaa(T49, 0, T49)
minus107_in_gaa(s(T50), s(T51), X131) → U10_gaa(T50, T51, X131, minus107_in_gaa(T50, T51, X131))
U10_gaa(T50, T51, X131, minus107_out_gaa(T50, T51, X131)) → minus107_out_gaa(s(T50), s(T51), X131)
U7_gaaa(T45, T46, T15, T16, minus107_out_gaa(T45, T46, X121)) → div1_out_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U8_gaaa(T45, T46, T15, T16, minus107_in_gaa(T45, T46, T48))
U8_gaaa(T45, T46, T15, T16, minus107_out_gaa(T45, T46, T48)) → U9_gaaa(T45, T46, T15, T16, div1_in_gaaa(T48, s(T47), T15, T16))
div1_in_gaaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56))))))) → div1_out_gaaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56)))))))
div1_in_gaaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63)))))) → div1_out_gaaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63))))))
div1_in_gaaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70))))) → div1_out_gaaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70)))))
div1_in_gaaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77)))) → div1_out_gaaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77))))
div1_in_gaaa(s(s(T84)), s(s(T86)), T82, s(s(T84))) → div1_out_gaaa(s(s(T84)), s(s(T86)), T82, s(s(T84)))
div1_in_gaaa(s(T91), s(T93), T89, s(T91)) → div1_out_gaaa(s(T91), s(T93), T89, s(T91))
div1_in_gaaa(T98, T100, T96, T98) → div1_out_gaaa(T98, T100, T96, T98)
U9_gaaa(T45, T46, T15, T16, div1_out_gaaa(T48, s(T47), T15, T16)) → div1_out_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
U9_ggaa(T45, T46, T15, T16, div1_out_gaaa(T48, s(T47), T15, T16)) → div1_out_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
U6_ggaa(T44, T15, T16, div1_out_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16)) → div1_out_ggaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16)
U5_ggaa(T41, T15, T16, div1_out_ggaa(T41, s(s(s(s(s(0))))), T15, T16)) → div1_out_ggaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16)
U4_ggaa(T38, T15, T16, div1_out_ggaa(T38, s(s(s(s(0)))), T15, T16)) → div1_out_ggaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16)
U3_ggaa(T35, T15, T16, div1_out_ggaa(T35, s(s(s(0))), T15, T16)) → div1_out_ggaa(s(s(s(T35))), s(s(s(0))), s(T15), T16)
U2_ggaa(T32, T15, T16, div1_out_ggaa(T32, s(s(0)), T15, T16)) → div1_out_ggaa(s(s(T32)), s(s(0)), s(T15), T16)
U1_ggaa(T29, T15, T16, div1_out_ggaa(T29, s(0), T15, T16)) → div1_out_ggaa(s(T29), s(0), s(T15), T16)

The argument filtering Pi contains the following mapping:
div1_in_ggaa(x1, x2, x3, x4)  =  div1_in_ggaa(x1, x2)
0  =  0
div1_out_ggaa(x1, x2, x3, x4)  =  div1_out_ggaa
s(x1)  =  s(x1)
U1_ggaa(x1, x2, x3, x4)  =  U1_ggaa(x4)
U2_ggaa(x1, x2, x3, x4)  =  U2_ggaa(x4)
U3_ggaa(x1, x2, x3, x4)  =  U3_ggaa(x4)
U4_ggaa(x1, x2, x3, x4)  =  U4_ggaa(x4)
U5_ggaa(x1, x2, x3, x4)  =  U5_ggaa(x4)
U6_ggaa(x1, x2, x3, x4)  =  U6_ggaa(x4)
U7_ggaa(x1, x2, x3, x4, x5)  =  U7_ggaa(x5)
minus107_in_gga(x1, x2, x3)  =  minus107_in_gga(x1, x2)
minus107_out_gga(x1, x2, x3)  =  minus107_out_gga(x3)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x4)
U8_ggaa(x1, x2, x3, x4, x5)  =  U8_ggaa(x5)
U9_ggaa(x1, x2, x3, x4, x5)  =  U9_ggaa(x5)
div1_in_gaaa(x1, x2, x3, x4)  =  div1_in_gaaa(x1)
div1_out_gaaa(x1, x2, x3, x4)  =  div1_out_gaaa
U1_gaaa(x1, x2, x3, x4)  =  U1_gaaa(x4)
U2_gaaa(x1, x2, x3, x4)  =  U2_gaaa(x4)
U3_gaaa(x1, x2, x3, x4)  =  U3_gaaa(x4)
U4_gaaa(x1, x2, x3, x4)  =  U4_gaaa(x4)
U5_gaaa(x1, x2, x3, x4)  =  U5_gaaa(x4)
U6_gaaa(x1, x2, x3, x4)  =  U6_gaaa(x4)
U7_gaaa(x1, x2, x3, x4, x5)  =  U7_gaaa(x5)
minus107_in_gaa(x1, x2, x3)  =  minus107_in_gaa(x1)
minus107_out_gaa(x1, x2, x3)  =  minus107_out_gaa(x2, x3)
U10_gaa(x1, x2, x3, x4)  =  U10_gaa(x4)
U8_gaaa(x1, x2, x3, x4, x5)  =  U8_gaaa(x5)
U9_gaaa(x1, x2, x3, x4, x5)  =  U9_gaaa(x5)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

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

div1_in_ggaa(0, T10, 0, 0) → div1_out_ggaa(0, T10, 0, 0)
div1_in_ggaa(s(T29), s(0), s(T15), T16) → U1_ggaa(T29, T15, T16, div1_in_ggaa(T29, s(0), T15, T16))
div1_in_ggaa(s(s(T32)), s(s(0)), s(T15), T16) → U2_ggaa(T32, T15, T16, div1_in_ggaa(T32, s(s(0)), T15, T16))
div1_in_ggaa(s(s(s(T35))), s(s(s(0))), s(T15), T16) → U3_ggaa(T35, T15, T16, div1_in_ggaa(T35, s(s(s(0))), T15, T16))
div1_in_ggaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16) → U4_ggaa(T38, T15, T16, div1_in_ggaa(T38, s(s(s(s(0)))), T15, T16))
div1_in_ggaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16) → U5_ggaa(T41, T15, T16, div1_in_ggaa(T41, s(s(s(s(s(0))))), T15, T16))
div1_in_ggaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16) → U6_ggaa(T44, T15, T16, div1_in_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16))
div1_in_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U7_ggaa(T45, T46, T15, T16, minus107_in_gga(T45, T46, X121))
minus107_in_gga(T49, 0, T49) → minus107_out_gga(T49, 0, T49)
minus107_in_gga(s(T50), s(T51), X131) → U10_gga(T50, T51, X131, minus107_in_gga(T50, T51, X131))
U10_gga(T50, T51, X131, minus107_out_gga(T50, T51, X131)) → minus107_out_gga(s(T50), s(T51), X131)
U7_ggaa(T45, T46, T15, T16, minus107_out_gga(T45, T46, X121)) → div1_out_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
div1_in_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U8_ggaa(T45, T46, T15, T16, minus107_in_gga(T45, T46, T48))
U8_ggaa(T45, T46, T15, T16, minus107_out_gga(T45, T46, T48)) → U9_ggaa(T45, T46, T15, T16, div1_in_gaaa(T48, s(T47), T15, T16))
div1_in_gaaa(0, T10, 0, 0) → div1_out_gaaa(0, T10, 0, 0)
div1_in_gaaa(s(T29), s(0), s(T15), T16) → U1_gaaa(T29, T15, T16, div1_in_ggaa(T29, s(0), T15, T16))
div1_in_ggaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56))))))) → div1_out_ggaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56)))))))
div1_in_ggaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63)))))) → div1_out_ggaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63))))))
div1_in_ggaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70))))) → div1_out_ggaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70)))))
div1_in_ggaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77)))) → div1_out_ggaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77))))
div1_in_ggaa(s(s(T84)), s(s(T86)), T82, s(s(T84))) → div1_out_ggaa(s(s(T84)), s(s(T86)), T82, s(s(T84)))
div1_in_ggaa(s(T91), s(T93), T89, s(T91)) → div1_out_ggaa(s(T91), s(T93), T89, s(T91))
div1_in_ggaa(T98, T100, T96, T98) → div1_out_ggaa(T98, T100, T96, T98)
U1_gaaa(T29, T15, T16, div1_out_ggaa(T29, s(0), T15, T16)) → div1_out_gaaa(s(T29), s(0), s(T15), T16)
div1_in_gaaa(s(s(T32)), s(s(0)), s(T15), T16) → U2_gaaa(T32, T15, T16, div1_in_ggaa(T32, s(s(0)), T15, T16))
U2_gaaa(T32, T15, T16, div1_out_ggaa(T32, s(s(0)), T15, T16)) → div1_out_gaaa(s(s(T32)), s(s(0)), s(T15), T16)
div1_in_gaaa(s(s(s(T35))), s(s(s(0))), s(T15), T16) → U3_gaaa(T35, T15, T16, div1_in_ggaa(T35, s(s(s(0))), T15, T16))
U3_gaaa(T35, T15, T16, div1_out_ggaa(T35, s(s(s(0))), T15, T16)) → div1_out_gaaa(s(s(s(T35))), s(s(s(0))), s(T15), T16)
div1_in_gaaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16) → U4_gaaa(T38, T15, T16, div1_in_ggaa(T38, s(s(s(s(0)))), T15, T16))
U4_gaaa(T38, T15, T16, div1_out_ggaa(T38, s(s(s(s(0)))), T15, T16)) → div1_out_gaaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16) → U5_gaaa(T41, T15, T16, div1_in_ggaa(T41, s(s(s(s(s(0))))), T15, T16))
U5_gaaa(T41, T15, T16, div1_out_ggaa(T41, s(s(s(s(s(0))))), T15, T16)) → div1_out_gaaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16) → U6_gaaa(T44, T15, T16, div1_in_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16))
U6_gaaa(T44, T15, T16, div1_out_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16)) → div1_out_gaaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U7_gaaa(T45, T46, T15, T16, minus107_in_gaa(T45, T46, X121))
minus107_in_gaa(T49, 0, T49) → minus107_out_gaa(T49, 0, T49)
minus107_in_gaa(s(T50), s(T51), X131) → U10_gaa(T50, T51, X131, minus107_in_gaa(T50, T51, X131))
U10_gaa(T50, T51, X131, minus107_out_gaa(T50, T51, X131)) → minus107_out_gaa(s(T50), s(T51), X131)
U7_gaaa(T45, T46, T15, T16, minus107_out_gaa(T45, T46, X121)) → div1_out_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U8_gaaa(T45, T46, T15, T16, minus107_in_gaa(T45, T46, T48))
U8_gaaa(T45, T46, T15, T16, minus107_out_gaa(T45, T46, T48)) → U9_gaaa(T45, T46, T15, T16, div1_in_gaaa(T48, s(T47), T15, T16))
div1_in_gaaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56))))))) → div1_out_gaaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56)))))))
div1_in_gaaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63)))))) → div1_out_gaaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63))))))
div1_in_gaaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70))))) → div1_out_gaaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70)))))
div1_in_gaaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77)))) → div1_out_gaaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77))))
div1_in_gaaa(s(s(T84)), s(s(T86)), T82, s(s(T84))) → div1_out_gaaa(s(s(T84)), s(s(T86)), T82, s(s(T84)))
div1_in_gaaa(s(T91), s(T93), T89, s(T91)) → div1_out_gaaa(s(T91), s(T93), T89, s(T91))
div1_in_gaaa(T98, T100, T96, T98) → div1_out_gaaa(T98, T100, T96, T98)
U9_gaaa(T45, T46, T15, T16, div1_out_gaaa(T48, s(T47), T15, T16)) → div1_out_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
U9_ggaa(T45, T46, T15, T16, div1_out_gaaa(T48, s(T47), T15, T16)) → div1_out_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
U6_ggaa(T44, T15, T16, div1_out_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16)) → div1_out_ggaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16)
U5_ggaa(T41, T15, T16, div1_out_ggaa(T41, s(s(s(s(s(0))))), T15, T16)) → div1_out_ggaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16)
U4_ggaa(T38, T15, T16, div1_out_ggaa(T38, s(s(s(s(0)))), T15, T16)) → div1_out_ggaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16)
U3_ggaa(T35, T15, T16, div1_out_ggaa(T35, s(s(s(0))), T15, T16)) → div1_out_ggaa(s(s(s(T35))), s(s(s(0))), s(T15), T16)
U2_ggaa(T32, T15, T16, div1_out_ggaa(T32, s(s(0)), T15, T16)) → div1_out_ggaa(s(s(T32)), s(s(0)), s(T15), T16)
U1_ggaa(T29, T15, T16, div1_out_ggaa(T29, s(0), T15, T16)) → div1_out_ggaa(s(T29), s(0), s(T15), T16)

The argument filtering Pi contains the following mapping:
div1_in_ggaa(x1, x2, x3, x4)  =  div1_in_ggaa(x1, x2)
0  =  0
div1_out_ggaa(x1, x2, x3, x4)  =  div1_out_ggaa
s(x1)  =  s(x1)
U1_ggaa(x1, x2, x3, x4)  =  U1_ggaa(x4)
U2_ggaa(x1, x2, x3, x4)  =  U2_ggaa(x4)
U3_ggaa(x1, x2, x3, x4)  =  U3_ggaa(x4)
U4_ggaa(x1, x2, x3, x4)  =  U4_ggaa(x4)
U5_ggaa(x1, x2, x3, x4)  =  U5_ggaa(x4)
U6_ggaa(x1, x2, x3, x4)  =  U6_ggaa(x4)
U7_ggaa(x1, x2, x3, x4, x5)  =  U7_ggaa(x5)
minus107_in_gga(x1, x2, x3)  =  minus107_in_gga(x1, x2)
minus107_out_gga(x1, x2, x3)  =  minus107_out_gga(x3)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x4)
U8_ggaa(x1, x2, x3, x4, x5)  =  U8_ggaa(x5)
U9_ggaa(x1, x2, x3, x4, x5)  =  U9_ggaa(x5)
div1_in_gaaa(x1, x2, x3, x4)  =  div1_in_gaaa(x1)
div1_out_gaaa(x1, x2, x3, x4)  =  div1_out_gaaa
U1_gaaa(x1, x2, x3, x4)  =  U1_gaaa(x4)
U2_gaaa(x1, x2, x3, x4)  =  U2_gaaa(x4)
U3_gaaa(x1, x2, x3, x4)  =  U3_gaaa(x4)
U4_gaaa(x1, x2, x3, x4)  =  U4_gaaa(x4)
U5_gaaa(x1, x2, x3, x4)  =  U5_gaaa(x4)
U6_gaaa(x1, x2, x3, x4)  =  U6_gaaa(x4)
U7_gaaa(x1, x2, x3, x4, x5)  =  U7_gaaa(x5)
minus107_in_gaa(x1, x2, x3)  =  minus107_in_gaa(x1)
minus107_out_gaa(x1, x2, x3)  =  minus107_out_gaa(x2, x3)
U10_gaa(x1, x2, x3, x4)  =  U10_gaa(x4)
U8_gaaa(x1, x2, x3, x4, x5)  =  U8_gaaa(x5)
U9_gaaa(x1, x2, x3, x4, x5)  =  U9_gaaa(x5)

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

DIV1_IN_GGAA(s(T29), s(0), s(T15), T16) → U1_GGAA(T29, T15, T16, div1_in_ggaa(T29, s(0), T15, T16))
DIV1_IN_GGAA(s(T29), s(0), s(T15), T16) → DIV1_IN_GGAA(T29, s(0), T15, T16)
DIV1_IN_GGAA(s(s(T32)), s(s(0)), s(T15), T16) → U2_GGAA(T32, T15, T16, div1_in_ggaa(T32, s(s(0)), T15, T16))
DIV1_IN_GGAA(s(s(T32)), s(s(0)), s(T15), T16) → DIV1_IN_GGAA(T32, s(s(0)), T15, T16)
DIV1_IN_GGAA(s(s(s(T35))), s(s(s(0))), s(T15), T16) → U3_GGAA(T35, T15, T16, div1_in_ggaa(T35, s(s(s(0))), T15, T16))
DIV1_IN_GGAA(s(s(s(T35))), s(s(s(0))), s(T15), T16) → DIV1_IN_GGAA(T35, s(s(s(0))), T15, T16)
DIV1_IN_GGAA(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16) → U4_GGAA(T38, T15, T16, div1_in_ggaa(T38, s(s(s(s(0)))), T15, T16))
DIV1_IN_GGAA(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16) → DIV1_IN_GGAA(T38, s(s(s(s(0)))), T15, T16)
DIV1_IN_GGAA(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16) → U5_GGAA(T41, T15, T16, div1_in_ggaa(T41, s(s(s(s(s(0))))), T15, T16))
DIV1_IN_GGAA(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16) → DIV1_IN_GGAA(T41, s(s(s(s(s(0))))), T15, T16)
DIV1_IN_GGAA(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16) → U6_GGAA(T44, T15, T16, div1_in_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16))
DIV1_IN_GGAA(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16) → DIV1_IN_GGAA(T44, s(s(s(s(s(s(0)))))), T15, T16)
DIV1_IN_GGAA(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U7_GGAA(T45, T46, T15, T16, minus107_in_gga(T45, T46, X121))
DIV1_IN_GGAA(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → MINUS107_IN_GGA(T45, T46, X121)
MINUS107_IN_GGA(s(T50), s(T51), X131) → U10_GGA(T50, T51, X131, minus107_in_gga(T50, T51, X131))
MINUS107_IN_GGA(s(T50), s(T51), X131) → MINUS107_IN_GGA(T50, T51, X131)
DIV1_IN_GGAA(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U8_GGAA(T45, T46, T15, T16, minus107_in_gga(T45, T46, T48))
U8_GGAA(T45, T46, T15, T16, minus107_out_gga(T45, T46, T48)) → U9_GGAA(T45, T46, T15, T16, div1_in_gaaa(T48, s(T47), T15, T16))
U8_GGAA(T45, T46, T15, T16, minus107_out_gga(T45, T46, T48)) → DIV1_IN_GAAA(T48, s(T47), T15, T16)
DIV1_IN_GAAA(s(T29), s(0), s(T15), T16) → U1_GAAA(T29, T15, T16, div1_in_ggaa(T29, s(0), T15, T16))
DIV1_IN_GAAA(s(T29), s(0), s(T15), T16) → DIV1_IN_GGAA(T29, s(0), T15, T16)
DIV1_IN_GAAA(s(s(T32)), s(s(0)), s(T15), T16) → U2_GAAA(T32, T15, T16, div1_in_ggaa(T32, s(s(0)), T15, T16))
DIV1_IN_GAAA(s(s(T32)), s(s(0)), s(T15), T16) → DIV1_IN_GGAA(T32, s(s(0)), T15, T16)
DIV1_IN_GAAA(s(s(s(T35))), s(s(s(0))), s(T15), T16) → U3_GAAA(T35, T15, T16, div1_in_ggaa(T35, s(s(s(0))), T15, T16))
DIV1_IN_GAAA(s(s(s(T35))), s(s(s(0))), s(T15), T16) → DIV1_IN_GGAA(T35, s(s(s(0))), T15, T16)
DIV1_IN_GAAA(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16) → U4_GAAA(T38, T15, T16, div1_in_ggaa(T38, s(s(s(s(0)))), T15, T16))
DIV1_IN_GAAA(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16) → DIV1_IN_GGAA(T38, s(s(s(s(0)))), T15, T16)
DIV1_IN_GAAA(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16) → U5_GAAA(T41, T15, T16, div1_in_ggaa(T41, s(s(s(s(s(0))))), T15, T16))
DIV1_IN_GAAA(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16) → DIV1_IN_GGAA(T41, s(s(s(s(s(0))))), T15, T16)
DIV1_IN_GAAA(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16) → U6_GAAA(T44, T15, T16, div1_in_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16))
DIV1_IN_GAAA(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16) → DIV1_IN_GGAA(T44, s(s(s(s(s(s(0)))))), T15, T16)
DIV1_IN_GAAA(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U7_GAAA(T45, T46, T15, T16, minus107_in_gaa(T45, T46, X121))
DIV1_IN_GAAA(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → MINUS107_IN_GAA(T45, T46, X121)
MINUS107_IN_GAA(s(T50), s(T51), X131) → U10_GAA(T50, T51, X131, minus107_in_gaa(T50, T51, X131))
MINUS107_IN_GAA(s(T50), s(T51), X131) → MINUS107_IN_GAA(T50, T51, X131)
DIV1_IN_GAAA(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U8_GAAA(T45, T46, T15, T16, minus107_in_gaa(T45, T46, T48))
U8_GAAA(T45, T46, T15, T16, minus107_out_gaa(T45, T46, T48)) → U9_GAAA(T45, T46, T15, T16, div1_in_gaaa(T48, s(T47), T15, T16))
U8_GAAA(T45, T46, T15, T16, minus107_out_gaa(T45, T46, T48)) → DIV1_IN_GAAA(T48, s(T47), T15, T16)

The TRS R consists of the following rules:

div1_in_ggaa(0, T10, 0, 0) → div1_out_ggaa(0, T10, 0, 0)
div1_in_ggaa(s(T29), s(0), s(T15), T16) → U1_ggaa(T29, T15, T16, div1_in_ggaa(T29, s(0), T15, T16))
div1_in_ggaa(s(s(T32)), s(s(0)), s(T15), T16) → U2_ggaa(T32, T15, T16, div1_in_ggaa(T32, s(s(0)), T15, T16))
div1_in_ggaa(s(s(s(T35))), s(s(s(0))), s(T15), T16) → U3_ggaa(T35, T15, T16, div1_in_ggaa(T35, s(s(s(0))), T15, T16))
div1_in_ggaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16) → U4_ggaa(T38, T15, T16, div1_in_ggaa(T38, s(s(s(s(0)))), T15, T16))
div1_in_ggaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16) → U5_ggaa(T41, T15, T16, div1_in_ggaa(T41, s(s(s(s(s(0))))), T15, T16))
div1_in_ggaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16) → U6_ggaa(T44, T15, T16, div1_in_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16))
div1_in_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U7_ggaa(T45, T46, T15, T16, minus107_in_gga(T45, T46, X121))
minus107_in_gga(T49, 0, T49) → minus107_out_gga(T49, 0, T49)
minus107_in_gga(s(T50), s(T51), X131) → U10_gga(T50, T51, X131, minus107_in_gga(T50, T51, X131))
U10_gga(T50, T51, X131, minus107_out_gga(T50, T51, X131)) → minus107_out_gga(s(T50), s(T51), X131)
U7_ggaa(T45, T46, T15, T16, minus107_out_gga(T45, T46, X121)) → div1_out_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
div1_in_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U8_ggaa(T45, T46, T15, T16, minus107_in_gga(T45, T46, T48))
U8_ggaa(T45, T46, T15, T16, minus107_out_gga(T45, T46, T48)) → U9_ggaa(T45, T46, T15, T16, div1_in_gaaa(T48, s(T47), T15, T16))
div1_in_gaaa(0, T10, 0, 0) → div1_out_gaaa(0, T10, 0, 0)
div1_in_gaaa(s(T29), s(0), s(T15), T16) → U1_gaaa(T29, T15, T16, div1_in_ggaa(T29, s(0), T15, T16))
div1_in_ggaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56))))))) → div1_out_ggaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56)))))))
div1_in_ggaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63)))))) → div1_out_ggaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63))))))
div1_in_ggaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70))))) → div1_out_ggaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70)))))
div1_in_ggaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77)))) → div1_out_ggaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77))))
div1_in_ggaa(s(s(T84)), s(s(T86)), T82, s(s(T84))) → div1_out_ggaa(s(s(T84)), s(s(T86)), T82, s(s(T84)))
div1_in_ggaa(s(T91), s(T93), T89, s(T91)) → div1_out_ggaa(s(T91), s(T93), T89, s(T91))
div1_in_ggaa(T98, T100, T96, T98) → div1_out_ggaa(T98, T100, T96, T98)
U1_gaaa(T29, T15, T16, div1_out_ggaa(T29, s(0), T15, T16)) → div1_out_gaaa(s(T29), s(0), s(T15), T16)
div1_in_gaaa(s(s(T32)), s(s(0)), s(T15), T16) → U2_gaaa(T32, T15, T16, div1_in_ggaa(T32, s(s(0)), T15, T16))
U2_gaaa(T32, T15, T16, div1_out_ggaa(T32, s(s(0)), T15, T16)) → div1_out_gaaa(s(s(T32)), s(s(0)), s(T15), T16)
div1_in_gaaa(s(s(s(T35))), s(s(s(0))), s(T15), T16) → U3_gaaa(T35, T15, T16, div1_in_ggaa(T35, s(s(s(0))), T15, T16))
U3_gaaa(T35, T15, T16, div1_out_ggaa(T35, s(s(s(0))), T15, T16)) → div1_out_gaaa(s(s(s(T35))), s(s(s(0))), s(T15), T16)
div1_in_gaaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16) → U4_gaaa(T38, T15, T16, div1_in_ggaa(T38, s(s(s(s(0)))), T15, T16))
U4_gaaa(T38, T15, T16, div1_out_ggaa(T38, s(s(s(s(0)))), T15, T16)) → div1_out_gaaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16) → U5_gaaa(T41, T15, T16, div1_in_ggaa(T41, s(s(s(s(s(0))))), T15, T16))
U5_gaaa(T41, T15, T16, div1_out_ggaa(T41, s(s(s(s(s(0))))), T15, T16)) → div1_out_gaaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16) → U6_gaaa(T44, T15, T16, div1_in_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16))
U6_gaaa(T44, T15, T16, div1_out_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16)) → div1_out_gaaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U7_gaaa(T45, T46, T15, T16, minus107_in_gaa(T45, T46, X121))
minus107_in_gaa(T49, 0, T49) → minus107_out_gaa(T49, 0, T49)
minus107_in_gaa(s(T50), s(T51), X131) → U10_gaa(T50, T51, X131, minus107_in_gaa(T50, T51, X131))
U10_gaa(T50, T51, X131, minus107_out_gaa(T50, T51, X131)) → minus107_out_gaa(s(T50), s(T51), X131)
U7_gaaa(T45, T46, T15, T16, minus107_out_gaa(T45, T46, X121)) → div1_out_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U8_gaaa(T45, T46, T15, T16, minus107_in_gaa(T45, T46, T48))
U8_gaaa(T45, T46, T15, T16, minus107_out_gaa(T45, T46, T48)) → U9_gaaa(T45, T46, T15, T16, div1_in_gaaa(T48, s(T47), T15, T16))
div1_in_gaaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56))))))) → div1_out_gaaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56)))))))
div1_in_gaaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63)))))) → div1_out_gaaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63))))))
div1_in_gaaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70))))) → div1_out_gaaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70)))))
div1_in_gaaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77)))) → div1_out_gaaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77))))
div1_in_gaaa(s(s(T84)), s(s(T86)), T82, s(s(T84))) → div1_out_gaaa(s(s(T84)), s(s(T86)), T82, s(s(T84)))
div1_in_gaaa(s(T91), s(T93), T89, s(T91)) → div1_out_gaaa(s(T91), s(T93), T89, s(T91))
div1_in_gaaa(T98, T100, T96, T98) → div1_out_gaaa(T98, T100, T96, T98)
U9_gaaa(T45, T46, T15, T16, div1_out_gaaa(T48, s(T47), T15, T16)) → div1_out_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
U9_ggaa(T45, T46, T15, T16, div1_out_gaaa(T48, s(T47), T15, T16)) → div1_out_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
U6_ggaa(T44, T15, T16, div1_out_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16)) → div1_out_ggaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16)
U5_ggaa(T41, T15, T16, div1_out_ggaa(T41, s(s(s(s(s(0))))), T15, T16)) → div1_out_ggaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16)
U4_ggaa(T38, T15, T16, div1_out_ggaa(T38, s(s(s(s(0)))), T15, T16)) → div1_out_ggaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16)
U3_ggaa(T35, T15, T16, div1_out_ggaa(T35, s(s(s(0))), T15, T16)) → div1_out_ggaa(s(s(s(T35))), s(s(s(0))), s(T15), T16)
U2_ggaa(T32, T15, T16, div1_out_ggaa(T32, s(s(0)), T15, T16)) → div1_out_ggaa(s(s(T32)), s(s(0)), s(T15), T16)
U1_ggaa(T29, T15, T16, div1_out_ggaa(T29, s(0), T15, T16)) → div1_out_ggaa(s(T29), s(0), s(T15), T16)

The argument filtering Pi contains the following mapping:
div1_in_ggaa(x1, x2, x3, x4)  =  div1_in_ggaa(x1, x2)
0  =  0
div1_out_ggaa(x1, x2, x3, x4)  =  div1_out_ggaa
s(x1)  =  s(x1)
U1_ggaa(x1, x2, x3, x4)  =  U1_ggaa(x4)
U2_ggaa(x1, x2, x3, x4)  =  U2_ggaa(x4)
U3_ggaa(x1, x2, x3, x4)  =  U3_ggaa(x4)
U4_ggaa(x1, x2, x3, x4)  =  U4_ggaa(x4)
U5_ggaa(x1, x2, x3, x4)  =  U5_ggaa(x4)
U6_ggaa(x1, x2, x3, x4)  =  U6_ggaa(x4)
U7_ggaa(x1, x2, x3, x4, x5)  =  U7_ggaa(x5)
minus107_in_gga(x1, x2, x3)  =  minus107_in_gga(x1, x2)
minus107_out_gga(x1, x2, x3)  =  minus107_out_gga(x3)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x4)
U8_ggaa(x1, x2, x3, x4, x5)  =  U8_ggaa(x5)
U9_ggaa(x1, x2, x3, x4, x5)  =  U9_ggaa(x5)
div1_in_gaaa(x1, x2, x3, x4)  =  div1_in_gaaa(x1)
div1_out_gaaa(x1, x2, x3, x4)  =  div1_out_gaaa
U1_gaaa(x1, x2, x3, x4)  =  U1_gaaa(x4)
U2_gaaa(x1, x2, x3, x4)  =  U2_gaaa(x4)
U3_gaaa(x1, x2, x3, x4)  =  U3_gaaa(x4)
U4_gaaa(x1, x2, x3, x4)  =  U4_gaaa(x4)
U5_gaaa(x1, x2, x3, x4)  =  U5_gaaa(x4)
U6_gaaa(x1, x2, x3, x4)  =  U6_gaaa(x4)
U7_gaaa(x1, x2, x3, x4, x5)  =  U7_gaaa(x5)
minus107_in_gaa(x1, x2, x3)  =  minus107_in_gaa(x1)
minus107_out_gaa(x1, x2, x3)  =  minus107_out_gaa(x2, x3)
U10_gaa(x1, x2, x3, x4)  =  U10_gaa(x4)
U8_gaaa(x1, x2, x3, x4, x5)  =  U8_gaaa(x5)
U9_gaaa(x1, x2, x3, x4, x5)  =  U9_gaaa(x5)
DIV1_IN_GGAA(x1, x2, x3, x4)  =  DIV1_IN_GGAA(x1, x2)
U1_GGAA(x1, x2, x3, x4)  =  U1_GGAA(x4)
U2_GGAA(x1, x2, x3, x4)  =  U2_GGAA(x4)
U3_GGAA(x1, x2, x3, x4)  =  U3_GGAA(x4)
U4_GGAA(x1, x2, x3, x4)  =  U4_GGAA(x4)
U5_GGAA(x1, x2, x3, x4)  =  U5_GGAA(x4)
U6_GGAA(x1, x2, x3, x4)  =  U6_GGAA(x4)
U7_GGAA(x1, x2, x3, x4, x5)  =  U7_GGAA(x5)
MINUS107_IN_GGA(x1, x2, x3)  =  MINUS107_IN_GGA(x1, x2)
U10_GGA(x1, x2, x3, x4)  =  U10_GGA(x4)
U8_GGAA(x1, x2, x3, x4, x5)  =  U8_GGAA(x5)
U9_GGAA(x1, x2, x3, x4, x5)  =  U9_GGAA(x5)
DIV1_IN_GAAA(x1, x2, x3, x4)  =  DIV1_IN_GAAA(x1)
U1_GAAA(x1, x2, x3, x4)  =  U1_GAAA(x4)
U2_GAAA(x1, x2, x3, x4)  =  U2_GAAA(x4)
U3_GAAA(x1, x2, x3, x4)  =  U3_GAAA(x4)
U4_GAAA(x1, x2, x3, x4)  =  U4_GAAA(x4)
U5_GAAA(x1, x2, x3, x4)  =  U5_GAAA(x4)
U6_GAAA(x1, x2, x3, x4)  =  U6_GAAA(x4)
U7_GAAA(x1, x2, x3, x4, x5)  =  U7_GAAA(x5)
MINUS107_IN_GAA(x1, x2, x3)  =  MINUS107_IN_GAA(x1)
U10_GAA(x1, x2, x3, x4)  =  U10_GAA(x4)
U8_GAAA(x1, x2, x3, x4, x5)  =  U8_GAAA(x5)
U9_GAAA(x1, x2, x3, x4, x5)  =  U9_GAAA(x5)

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

(6) Obligation:

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

DIV1_IN_GGAA(s(T29), s(0), s(T15), T16) → U1_GGAA(T29, T15, T16, div1_in_ggaa(T29, s(0), T15, T16))
DIV1_IN_GGAA(s(T29), s(0), s(T15), T16) → DIV1_IN_GGAA(T29, s(0), T15, T16)
DIV1_IN_GGAA(s(s(T32)), s(s(0)), s(T15), T16) → U2_GGAA(T32, T15, T16, div1_in_ggaa(T32, s(s(0)), T15, T16))
DIV1_IN_GGAA(s(s(T32)), s(s(0)), s(T15), T16) → DIV1_IN_GGAA(T32, s(s(0)), T15, T16)
DIV1_IN_GGAA(s(s(s(T35))), s(s(s(0))), s(T15), T16) → U3_GGAA(T35, T15, T16, div1_in_ggaa(T35, s(s(s(0))), T15, T16))
DIV1_IN_GGAA(s(s(s(T35))), s(s(s(0))), s(T15), T16) → DIV1_IN_GGAA(T35, s(s(s(0))), T15, T16)
DIV1_IN_GGAA(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16) → U4_GGAA(T38, T15, T16, div1_in_ggaa(T38, s(s(s(s(0)))), T15, T16))
DIV1_IN_GGAA(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16) → DIV1_IN_GGAA(T38, s(s(s(s(0)))), T15, T16)
DIV1_IN_GGAA(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16) → U5_GGAA(T41, T15, T16, div1_in_ggaa(T41, s(s(s(s(s(0))))), T15, T16))
DIV1_IN_GGAA(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16) → DIV1_IN_GGAA(T41, s(s(s(s(s(0))))), T15, T16)
DIV1_IN_GGAA(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16) → U6_GGAA(T44, T15, T16, div1_in_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16))
DIV1_IN_GGAA(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16) → DIV1_IN_GGAA(T44, s(s(s(s(s(s(0)))))), T15, T16)
DIV1_IN_GGAA(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U7_GGAA(T45, T46, T15, T16, minus107_in_gga(T45, T46, X121))
DIV1_IN_GGAA(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → MINUS107_IN_GGA(T45, T46, X121)
MINUS107_IN_GGA(s(T50), s(T51), X131) → U10_GGA(T50, T51, X131, minus107_in_gga(T50, T51, X131))
MINUS107_IN_GGA(s(T50), s(T51), X131) → MINUS107_IN_GGA(T50, T51, X131)
DIV1_IN_GGAA(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U8_GGAA(T45, T46, T15, T16, minus107_in_gga(T45, T46, T48))
U8_GGAA(T45, T46, T15, T16, minus107_out_gga(T45, T46, T48)) → U9_GGAA(T45, T46, T15, T16, div1_in_gaaa(T48, s(T47), T15, T16))
U8_GGAA(T45, T46, T15, T16, minus107_out_gga(T45, T46, T48)) → DIV1_IN_GAAA(T48, s(T47), T15, T16)
DIV1_IN_GAAA(s(T29), s(0), s(T15), T16) → U1_GAAA(T29, T15, T16, div1_in_ggaa(T29, s(0), T15, T16))
DIV1_IN_GAAA(s(T29), s(0), s(T15), T16) → DIV1_IN_GGAA(T29, s(0), T15, T16)
DIV1_IN_GAAA(s(s(T32)), s(s(0)), s(T15), T16) → U2_GAAA(T32, T15, T16, div1_in_ggaa(T32, s(s(0)), T15, T16))
DIV1_IN_GAAA(s(s(T32)), s(s(0)), s(T15), T16) → DIV1_IN_GGAA(T32, s(s(0)), T15, T16)
DIV1_IN_GAAA(s(s(s(T35))), s(s(s(0))), s(T15), T16) → U3_GAAA(T35, T15, T16, div1_in_ggaa(T35, s(s(s(0))), T15, T16))
DIV1_IN_GAAA(s(s(s(T35))), s(s(s(0))), s(T15), T16) → DIV1_IN_GGAA(T35, s(s(s(0))), T15, T16)
DIV1_IN_GAAA(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16) → U4_GAAA(T38, T15, T16, div1_in_ggaa(T38, s(s(s(s(0)))), T15, T16))
DIV1_IN_GAAA(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16) → DIV1_IN_GGAA(T38, s(s(s(s(0)))), T15, T16)
DIV1_IN_GAAA(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16) → U5_GAAA(T41, T15, T16, div1_in_ggaa(T41, s(s(s(s(s(0))))), T15, T16))
DIV1_IN_GAAA(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16) → DIV1_IN_GGAA(T41, s(s(s(s(s(0))))), T15, T16)
DIV1_IN_GAAA(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16) → U6_GAAA(T44, T15, T16, div1_in_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16))
DIV1_IN_GAAA(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16) → DIV1_IN_GGAA(T44, s(s(s(s(s(s(0)))))), T15, T16)
DIV1_IN_GAAA(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U7_GAAA(T45, T46, T15, T16, minus107_in_gaa(T45, T46, X121))
DIV1_IN_GAAA(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → MINUS107_IN_GAA(T45, T46, X121)
MINUS107_IN_GAA(s(T50), s(T51), X131) → U10_GAA(T50, T51, X131, minus107_in_gaa(T50, T51, X131))
MINUS107_IN_GAA(s(T50), s(T51), X131) → MINUS107_IN_GAA(T50, T51, X131)
DIV1_IN_GAAA(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U8_GAAA(T45, T46, T15, T16, minus107_in_gaa(T45, T46, T48))
U8_GAAA(T45, T46, T15, T16, minus107_out_gaa(T45, T46, T48)) → U9_GAAA(T45, T46, T15, T16, div1_in_gaaa(T48, s(T47), T15, T16))
U8_GAAA(T45, T46, T15, T16, minus107_out_gaa(T45, T46, T48)) → DIV1_IN_GAAA(T48, s(T47), T15, T16)

The TRS R consists of the following rules:

div1_in_ggaa(0, T10, 0, 0) → div1_out_ggaa(0, T10, 0, 0)
div1_in_ggaa(s(T29), s(0), s(T15), T16) → U1_ggaa(T29, T15, T16, div1_in_ggaa(T29, s(0), T15, T16))
div1_in_ggaa(s(s(T32)), s(s(0)), s(T15), T16) → U2_ggaa(T32, T15, T16, div1_in_ggaa(T32, s(s(0)), T15, T16))
div1_in_ggaa(s(s(s(T35))), s(s(s(0))), s(T15), T16) → U3_ggaa(T35, T15, T16, div1_in_ggaa(T35, s(s(s(0))), T15, T16))
div1_in_ggaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16) → U4_ggaa(T38, T15, T16, div1_in_ggaa(T38, s(s(s(s(0)))), T15, T16))
div1_in_ggaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16) → U5_ggaa(T41, T15, T16, div1_in_ggaa(T41, s(s(s(s(s(0))))), T15, T16))
div1_in_ggaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16) → U6_ggaa(T44, T15, T16, div1_in_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16))
div1_in_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U7_ggaa(T45, T46, T15, T16, minus107_in_gga(T45, T46, X121))
minus107_in_gga(T49, 0, T49) → minus107_out_gga(T49, 0, T49)
minus107_in_gga(s(T50), s(T51), X131) → U10_gga(T50, T51, X131, minus107_in_gga(T50, T51, X131))
U10_gga(T50, T51, X131, minus107_out_gga(T50, T51, X131)) → minus107_out_gga(s(T50), s(T51), X131)
U7_ggaa(T45, T46, T15, T16, minus107_out_gga(T45, T46, X121)) → div1_out_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
div1_in_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U8_ggaa(T45, T46, T15, T16, minus107_in_gga(T45, T46, T48))
U8_ggaa(T45, T46, T15, T16, minus107_out_gga(T45, T46, T48)) → U9_ggaa(T45, T46, T15, T16, div1_in_gaaa(T48, s(T47), T15, T16))
div1_in_gaaa(0, T10, 0, 0) → div1_out_gaaa(0, T10, 0, 0)
div1_in_gaaa(s(T29), s(0), s(T15), T16) → U1_gaaa(T29, T15, T16, div1_in_ggaa(T29, s(0), T15, T16))
div1_in_ggaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56))))))) → div1_out_ggaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56)))))))
div1_in_ggaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63)))))) → div1_out_ggaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63))))))
div1_in_ggaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70))))) → div1_out_ggaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70)))))
div1_in_ggaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77)))) → div1_out_ggaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77))))
div1_in_ggaa(s(s(T84)), s(s(T86)), T82, s(s(T84))) → div1_out_ggaa(s(s(T84)), s(s(T86)), T82, s(s(T84)))
div1_in_ggaa(s(T91), s(T93), T89, s(T91)) → div1_out_ggaa(s(T91), s(T93), T89, s(T91))
div1_in_ggaa(T98, T100, T96, T98) → div1_out_ggaa(T98, T100, T96, T98)
U1_gaaa(T29, T15, T16, div1_out_ggaa(T29, s(0), T15, T16)) → div1_out_gaaa(s(T29), s(0), s(T15), T16)
div1_in_gaaa(s(s(T32)), s(s(0)), s(T15), T16) → U2_gaaa(T32, T15, T16, div1_in_ggaa(T32, s(s(0)), T15, T16))
U2_gaaa(T32, T15, T16, div1_out_ggaa(T32, s(s(0)), T15, T16)) → div1_out_gaaa(s(s(T32)), s(s(0)), s(T15), T16)
div1_in_gaaa(s(s(s(T35))), s(s(s(0))), s(T15), T16) → U3_gaaa(T35, T15, T16, div1_in_ggaa(T35, s(s(s(0))), T15, T16))
U3_gaaa(T35, T15, T16, div1_out_ggaa(T35, s(s(s(0))), T15, T16)) → div1_out_gaaa(s(s(s(T35))), s(s(s(0))), s(T15), T16)
div1_in_gaaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16) → U4_gaaa(T38, T15, T16, div1_in_ggaa(T38, s(s(s(s(0)))), T15, T16))
U4_gaaa(T38, T15, T16, div1_out_ggaa(T38, s(s(s(s(0)))), T15, T16)) → div1_out_gaaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16) → U5_gaaa(T41, T15, T16, div1_in_ggaa(T41, s(s(s(s(s(0))))), T15, T16))
U5_gaaa(T41, T15, T16, div1_out_ggaa(T41, s(s(s(s(s(0))))), T15, T16)) → div1_out_gaaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16) → U6_gaaa(T44, T15, T16, div1_in_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16))
U6_gaaa(T44, T15, T16, div1_out_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16)) → div1_out_gaaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U7_gaaa(T45, T46, T15, T16, minus107_in_gaa(T45, T46, X121))
minus107_in_gaa(T49, 0, T49) → minus107_out_gaa(T49, 0, T49)
minus107_in_gaa(s(T50), s(T51), X131) → U10_gaa(T50, T51, X131, minus107_in_gaa(T50, T51, X131))
U10_gaa(T50, T51, X131, minus107_out_gaa(T50, T51, X131)) → minus107_out_gaa(s(T50), s(T51), X131)
U7_gaaa(T45, T46, T15, T16, minus107_out_gaa(T45, T46, X121)) → div1_out_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U8_gaaa(T45, T46, T15, T16, minus107_in_gaa(T45, T46, T48))
U8_gaaa(T45, T46, T15, T16, minus107_out_gaa(T45, T46, T48)) → U9_gaaa(T45, T46, T15, T16, div1_in_gaaa(T48, s(T47), T15, T16))
div1_in_gaaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56))))))) → div1_out_gaaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56)))))))
div1_in_gaaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63)))))) → div1_out_gaaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63))))))
div1_in_gaaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70))))) → div1_out_gaaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70)))))
div1_in_gaaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77)))) → div1_out_gaaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77))))
div1_in_gaaa(s(s(T84)), s(s(T86)), T82, s(s(T84))) → div1_out_gaaa(s(s(T84)), s(s(T86)), T82, s(s(T84)))
div1_in_gaaa(s(T91), s(T93), T89, s(T91)) → div1_out_gaaa(s(T91), s(T93), T89, s(T91))
div1_in_gaaa(T98, T100, T96, T98) → div1_out_gaaa(T98, T100, T96, T98)
U9_gaaa(T45, T46, T15, T16, div1_out_gaaa(T48, s(T47), T15, T16)) → div1_out_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
U9_ggaa(T45, T46, T15, T16, div1_out_gaaa(T48, s(T47), T15, T16)) → div1_out_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
U6_ggaa(T44, T15, T16, div1_out_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16)) → div1_out_ggaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16)
U5_ggaa(T41, T15, T16, div1_out_ggaa(T41, s(s(s(s(s(0))))), T15, T16)) → div1_out_ggaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16)
U4_ggaa(T38, T15, T16, div1_out_ggaa(T38, s(s(s(s(0)))), T15, T16)) → div1_out_ggaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16)
U3_ggaa(T35, T15, T16, div1_out_ggaa(T35, s(s(s(0))), T15, T16)) → div1_out_ggaa(s(s(s(T35))), s(s(s(0))), s(T15), T16)
U2_ggaa(T32, T15, T16, div1_out_ggaa(T32, s(s(0)), T15, T16)) → div1_out_ggaa(s(s(T32)), s(s(0)), s(T15), T16)
U1_ggaa(T29, T15, T16, div1_out_ggaa(T29, s(0), T15, T16)) → div1_out_ggaa(s(T29), s(0), s(T15), T16)

The argument filtering Pi contains the following mapping:
div1_in_ggaa(x1, x2, x3, x4)  =  div1_in_ggaa(x1, x2)
0  =  0
div1_out_ggaa(x1, x2, x3, x4)  =  div1_out_ggaa
s(x1)  =  s(x1)
U1_ggaa(x1, x2, x3, x4)  =  U1_ggaa(x4)
U2_ggaa(x1, x2, x3, x4)  =  U2_ggaa(x4)
U3_ggaa(x1, x2, x3, x4)  =  U3_ggaa(x4)
U4_ggaa(x1, x2, x3, x4)  =  U4_ggaa(x4)
U5_ggaa(x1, x2, x3, x4)  =  U5_ggaa(x4)
U6_ggaa(x1, x2, x3, x4)  =  U6_ggaa(x4)
U7_ggaa(x1, x2, x3, x4, x5)  =  U7_ggaa(x5)
minus107_in_gga(x1, x2, x3)  =  minus107_in_gga(x1, x2)
minus107_out_gga(x1, x2, x3)  =  minus107_out_gga(x3)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x4)
U8_ggaa(x1, x2, x3, x4, x5)  =  U8_ggaa(x5)
U9_ggaa(x1, x2, x3, x4, x5)  =  U9_ggaa(x5)
div1_in_gaaa(x1, x2, x3, x4)  =  div1_in_gaaa(x1)
div1_out_gaaa(x1, x2, x3, x4)  =  div1_out_gaaa
U1_gaaa(x1, x2, x3, x4)  =  U1_gaaa(x4)
U2_gaaa(x1, x2, x3, x4)  =  U2_gaaa(x4)
U3_gaaa(x1, x2, x3, x4)  =  U3_gaaa(x4)
U4_gaaa(x1, x2, x3, x4)  =  U4_gaaa(x4)
U5_gaaa(x1, x2, x3, x4)  =  U5_gaaa(x4)
U6_gaaa(x1, x2, x3, x4)  =  U6_gaaa(x4)
U7_gaaa(x1, x2, x3, x4, x5)  =  U7_gaaa(x5)
minus107_in_gaa(x1, x2, x3)  =  minus107_in_gaa(x1)
minus107_out_gaa(x1, x2, x3)  =  minus107_out_gaa(x2, x3)
U10_gaa(x1, x2, x3, x4)  =  U10_gaa(x4)
U8_gaaa(x1, x2, x3, x4, x5)  =  U8_gaaa(x5)
U9_gaaa(x1, x2, x3, x4, x5)  =  U9_gaaa(x5)
DIV1_IN_GGAA(x1, x2, x3, x4)  =  DIV1_IN_GGAA(x1, x2)
U1_GGAA(x1, x2, x3, x4)  =  U1_GGAA(x4)
U2_GGAA(x1, x2, x3, x4)  =  U2_GGAA(x4)
U3_GGAA(x1, x2, x3, x4)  =  U3_GGAA(x4)
U4_GGAA(x1, x2, x3, x4)  =  U4_GGAA(x4)
U5_GGAA(x1, x2, x3, x4)  =  U5_GGAA(x4)
U6_GGAA(x1, x2, x3, x4)  =  U6_GGAA(x4)
U7_GGAA(x1, x2, x3, x4, x5)  =  U7_GGAA(x5)
MINUS107_IN_GGA(x1, x2, x3)  =  MINUS107_IN_GGA(x1, x2)
U10_GGA(x1, x2, x3, x4)  =  U10_GGA(x4)
U8_GGAA(x1, x2, x3, x4, x5)  =  U8_GGAA(x5)
U9_GGAA(x1, x2, x3, x4, x5)  =  U9_GGAA(x5)
DIV1_IN_GAAA(x1, x2, x3, x4)  =  DIV1_IN_GAAA(x1)
U1_GAAA(x1, x2, x3, x4)  =  U1_GAAA(x4)
U2_GAAA(x1, x2, x3, x4)  =  U2_GAAA(x4)
U3_GAAA(x1, x2, x3, x4)  =  U3_GAAA(x4)
U4_GAAA(x1, x2, x3, x4)  =  U4_GAAA(x4)
U5_GAAA(x1, x2, x3, x4)  =  U5_GAAA(x4)
U6_GAAA(x1, x2, x3, x4)  =  U6_GAAA(x4)
U7_GAAA(x1, x2, x3, x4, x5)  =  U7_GAAA(x5)
MINUS107_IN_GAA(x1, x2, x3)  =  MINUS107_IN_GAA(x1)
U10_GAA(x1, x2, x3, x4)  =  U10_GAA(x4)
U8_GAAA(x1, x2, x3, x4, x5)  =  U8_GAAA(x5)
U9_GAAA(x1, x2, x3, x4, x5)  =  U9_GAAA(x5)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 9 SCCs with 28 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

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

MINUS107_IN_GAA(s(T50), s(T51), X131) → MINUS107_IN_GAA(T50, T51, X131)

The TRS R consists of the following rules:

div1_in_ggaa(0, T10, 0, 0) → div1_out_ggaa(0, T10, 0, 0)
div1_in_ggaa(s(T29), s(0), s(T15), T16) → U1_ggaa(T29, T15, T16, div1_in_ggaa(T29, s(0), T15, T16))
div1_in_ggaa(s(s(T32)), s(s(0)), s(T15), T16) → U2_ggaa(T32, T15, T16, div1_in_ggaa(T32, s(s(0)), T15, T16))
div1_in_ggaa(s(s(s(T35))), s(s(s(0))), s(T15), T16) → U3_ggaa(T35, T15, T16, div1_in_ggaa(T35, s(s(s(0))), T15, T16))
div1_in_ggaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16) → U4_ggaa(T38, T15, T16, div1_in_ggaa(T38, s(s(s(s(0)))), T15, T16))
div1_in_ggaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16) → U5_ggaa(T41, T15, T16, div1_in_ggaa(T41, s(s(s(s(s(0))))), T15, T16))
div1_in_ggaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16) → U6_ggaa(T44, T15, T16, div1_in_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16))
div1_in_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U7_ggaa(T45, T46, T15, T16, minus107_in_gga(T45, T46, X121))
minus107_in_gga(T49, 0, T49) → minus107_out_gga(T49, 0, T49)
minus107_in_gga(s(T50), s(T51), X131) → U10_gga(T50, T51, X131, minus107_in_gga(T50, T51, X131))
U10_gga(T50, T51, X131, minus107_out_gga(T50, T51, X131)) → minus107_out_gga(s(T50), s(T51), X131)
U7_ggaa(T45, T46, T15, T16, minus107_out_gga(T45, T46, X121)) → div1_out_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
div1_in_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U8_ggaa(T45, T46, T15, T16, minus107_in_gga(T45, T46, T48))
U8_ggaa(T45, T46, T15, T16, minus107_out_gga(T45, T46, T48)) → U9_ggaa(T45, T46, T15, T16, div1_in_gaaa(T48, s(T47), T15, T16))
div1_in_gaaa(0, T10, 0, 0) → div1_out_gaaa(0, T10, 0, 0)
div1_in_gaaa(s(T29), s(0), s(T15), T16) → U1_gaaa(T29, T15, T16, div1_in_ggaa(T29, s(0), T15, T16))
div1_in_ggaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56))))))) → div1_out_ggaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56)))))))
div1_in_ggaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63)))))) → div1_out_ggaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63))))))
div1_in_ggaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70))))) → div1_out_ggaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70)))))
div1_in_ggaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77)))) → div1_out_ggaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77))))
div1_in_ggaa(s(s(T84)), s(s(T86)), T82, s(s(T84))) → div1_out_ggaa(s(s(T84)), s(s(T86)), T82, s(s(T84)))
div1_in_ggaa(s(T91), s(T93), T89, s(T91)) → div1_out_ggaa(s(T91), s(T93), T89, s(T91))
div1_in_ggaa(T98, T100, T96, T98) → div1_out_ggaa(T98, T100, T96, T98)
U1_gaaa(T29, T15, T16, div1_out_ggaa(T29, s(0), T15, T16)) → div1_out_gaaa(s(T29), s(0), s(T15), T16)
div1_in_gaaa(s(s(T32)), s(s(0)), s(T15), T16) → U2_gaaa(T32, T15, T16, div1_in_ggaa(T32, s(s(0)), T15, T16))
U2_gaaa(T32, T15, T16, div1_out_ggaa(T32, s(s(0)), T15, T16)) → div1_out_gaaa(s(s(T32)), s(s(0)), s(T15), T16)
div1_in_gaaa(s(s(s(T35))), s(s(s(0))), s(T15), T16) → U3_gaaa(T35, T15, T16, div1_in_ggaa(T35, s(s(s(0))), T15, T16))
U3_gaaa(T35, T15, T16, div1_out_ggaa(T35, s(s(s(0))), T15, T16)) → div1_out_gaaa(s(s(s(T35))), s(s(s(0))), s(T15), T16)
div1_in_gaaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16) → U4_gaaa(T38, T15, T16, div1_in_ggaa(T38, s(s(s(s(0)))), T15, T16))
U4_gaaa(T38, T15, T16, div1_out_ggaa(T38, s(s(s(s(0)))), T15, T16)) → div1_out_gaaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16) → U5_gaaa(T41, T15, T16, div1_in_ggaa(T41, s(s(s(s(s(0))))), T15, T16))
U5_gaaa(T41, T15, T16, div1_out_ggaa(T41, s(s(s(s(s(0))))), T15, T16)) → div1_out_gaaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16) → U6_gaaa(T44, T15, T16, div1_in_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16))
U6_gaaa(T44, T15, T16, div1_out_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16)) → div1_out_gaaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U7_gaaa(T45, T46, T15, T16, minus107_in_gaa(T45, T46, X121))
minus107_in_gaa(T49, 0, T49) → minus107_out_gaa(T49, 0, T49)
minus107_in_gaa(s(T50), s(T51), X131) → U10_gaa(T50, T51, X131, minus107_in_gaa(T50, T51, X131))
U10_gaa(T50, T51, X131, minus107_out_gaa(T50, T51, X131)) → minus107_out_gaa(s(T50), s(T51), X131)
U7_gaaa(T45, T46, T15, T16, minus107_out_gaa(T45, T46, X121)) → div1_out_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U8_gaaa(T45, T46, T15, T16, minus107_in_gaa(T45, T46, T48))
U8_gaaa(T45, T46, T15, T16, minus107_out_gaa(T45, T46, T48)) → U9_gaaa(T45, T46, T15, T16, div1_in_gaaa(T48, s(T47), T15, T16))
div1_in_gaaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56))))))) → div1_out_gaaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56)))))))
div1_in_gaaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63)))))) → div1_out_gaaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63))))))
div1_in_gaaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70))))) → div1_out_gaaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70)))))
div1_in_gaaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77)))) → div1_out_gaaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77))))
div1_in_gaaa(s(s(T84)), s(s(T86)), T82, s(s(T84))) → div1_out_gaaa(s(s(T84)), s(s(T86)), T82, s(s(T84)))
div1_in_gaaa(s(T91), s(T93), T89, s(T91)) → div1_out_gaaa(s(T91), s(T93), T89, s(T91))
div1_in_gaaa(T98, T100, T96, T98) → div1_out_gaaa(T98, T100, T96, T98)
U9_gaaa(T45, T46, T15, T16, div1_out_gaaa(T48, s(T47), T15, T16)) → div1_out_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
U9_ggaa(T45, T46, T15, T16, div1_out_gaaa(T48, s(T47), T15, T16)) → div1_out_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
U6_ggaa(T44, T15, T16, div1_out_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16)) → div1_out_ggaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16)
U5_ggaa(T41, T15, T16, div1_out_ggaa(T41, s(s(s(s(s(0))))), T15, T16)) → div1_out_ggaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16)
U4_ggaa(T38, T15, T16, div1_out_ggaa(T38, s(s(s(s(0)))), T15, T16)) → div1_out_ggaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16)
U3_ggaa(T35, T15, T16, div1_out_ggaa(T35, s(s(s(0))), T15, T16)) → div1_out_ggaa(s(s(s(T35))), s(s(s(0))), s(T15), T16)
U2_ggaa(T32, T15, T16, div1_out_ggaa(T32, s(s(0)), T15, T16)) → div1_out_ggaa(s(s(T32)), s(s(0)), s(T15), T16)
U1_ggaa(T29, T15, T16, div1_out_ggaa(T29, s(0), T15, T16)) → div1_out_ggaa(s(T29), s(0), s(T15), T16)

The argument filtering Pi contains the following mapping:
div1_in_ggaa(x1, x2, x3, x4)  =  div1_in_ggaa(x1, x2)
0  =  0
div1_out_ggaa(x1, x2, x3, x4)  =  div1_out_ggaa
s(x1)  =  s(x1)
U1_ggaa(x1, x2, x3, x4)  =  U1_ggaa(x4)
U2_ggaa(x1, x2, x3, x4)  =  U2_ggaa(x4)
U3_ggaa(x1, x2, x3, x4)  =  U3_ggaa(x4)
U4_ggaa(x1, x2, x3, x4)  =  U4_ggaa(x4)
U5_ggaa(x1, x2, x3, x4)  =  U5_ggaa(x4)
U6_ggaa(x1, x2, x3, x4)  =  U6_ggaa(x4)
U7_ggaa(x1, x2, x3, x4, x5)  =  U7_ggaa(x5)
minus107_in_gga(x1, x2, x3)  =  minus107_in_gga(x1, x2)
minus107_out_gga(x1, x2, x3)  =  minus107_out_gga(x3)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x4)
U8_ggaa(x1, x2, x3, x4, x5)  =  U8_ggaa(x5)
U9_ggaa(x1, x2, x3, x4, x5)  =  U9_ggaa(x5)
div1_in_gaaa(x1, x2, x3, x4)  =  div1_in_gaaa(x1)
div1_out_gaaa(x1, x2, x3, x4)  =  div1_out_gaaa
U1_gaaa(x1, x2, x3, x4)  =  U1_gaaa(x4)
U2_gaaa(x1, x2, x3, x4)  =  U2_gaaa(x4)
U3_gaaa(x1, x2, x3, x4)  =  U3_gaaa(x4)
U4_gaaa(x1, x2, x3, x4)  =  U4_gaaa(x4)
U5_gaaa(x1, x2, x3, x4)  =  U5_gaaa(x4)
U6_gaaa(x1, x2, x3, x4)  =  U6_gaaa(x4)
U7_gaaa(x1, x2, x3, x4, x5)  =  U7_gaaa(x5)
minus107_in_gaa(x1, x2, x3)  =  minus107_in_gaa(x1)
minus107_out_gaa(x1, x2, x3)  =  minus107_out_gaa(x2, x3)
U10_gaa(x1, x2, x3, x4)  =  U10_gaa(x4)
U8_gaaa(x1, x2, x3, x4, x5)  =  U8_gaaa(x5)
U9_gaaa(x1, x2, x3, x4, x5)  =  U9_gaaa(x5)
MINUS107_IN_GAA(x1, x2, x3)  =  MINUS107_IN_GAA(x1)

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

(10) UsableRulesProof (EQUIVALENT transformation)

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

(11) Obligation:

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

MINUS107_IN_GAA(s(T50), s(T51), X131) → MINUS107_IN_GAA(T50, T51, X131)

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

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

(12) PiDPToQDPProof (SOUND transformation)

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

(13) Obligation:

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

MINUS107_IN_GAA(s(T50)) → MINUS107_IN_GAA(T50)

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

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

  • MINUS107_IN_GAA(s(T50)) → MINUS107_IN_GAA(T50)
    The graph contains the following edges 1 > 1

(15) TRUE

(16) Obligation:

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

MINUS107_IN_GGA(s(T50), s(T51), X131) → MINUS107_IN_GGA(T50, T51, X131)

The TRS R consists of the following rules:

div1_in_ggaa(0, T10, 0, 0) → div1_out_ggaa(0, T10, 0, 0)
div1_in_ggaa(s(T29), s(0), s(T15), T16) → U1_ggaa(T29, T15, T16, div1_in_ggaa(T29, s(0), T15, T16))
div1_in_ggaa(s(s(T32)), s(s(0)), s(T15), T16) → U2_ggaa(T32, T15, T16, div1_in_ggaa(T32, s(s(0)), T15, T16))
div1_in_ggaa(s(s(s(T35))), s(s(s(0))), s(T15), T16) → U3_ggaa(T35, T15, T16, div1_in_ggaa(T35, s(s(s(0))), T15, T16))
div1_in_ggaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16) → U4_ggaa(T38, T15, T16, div1_in_ggaa(T38, s(s(s(s(0)))), T15, T16))
div1_in_ggaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16) → U5_ggaa(T41, T15, T16, div1_in_ggaa(T41, s(s(s(s(s(0))))), T15, T16))
div1_in_ggaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16) → U6_ggaa(T44, T15, T16, div1_in_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16))
div1_in_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U7_ggaa(T45, T46, T15, T16, minus107_in_gga(T45, T46, X121))
minus107_in_gga(T49, 0, T49) → minus107_out_gga(T49, 0, T49)
minus107_in_gga(s(T50), s(T51), X131) → U10_gga(T50, T51, X131, minus107_in_gga(T50, T51, X131))
U10_gga(T50, T51, X131, minus107_out_gga(T50, T51, X131)) → minus107_out_gga(s(T50), s(T51), X131)
U7_ggaa(T45, T46, T15, T16, minus107_out_gga(T45, T46, X121)) → div1_out_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
div1_in_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U8_ggaa(T45, T46, T15, T16, minus107_in_gga(T45, T46, T48))
U8_ggaa(T45, T46, T15, T16, minus107_out_gga(T45, T46, T48)) → U9_ggaa(T45, T46, T15, T16, div1_in_gaaa(T48, s(T47), T15, T16))
div1_in_gaaa(0, T10, 0, 0) → div1_out_gaaa(0, T10, 0, 0)
div1_in_gaaa(s(T29), s(0), s(T15), T16) → U1_gaaa(T29, T15, T16, div1_in_ggaa(T29, s(0), T15, T16))
div1_in_ggaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56))))))) → div1_out_ggaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56)))))))
div1_in_ggaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63)))))) → div1_out_ggaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63))))))
div1_in_ggaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70))))) → div1_out_ggaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70)))))
div1_in_ggaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77)))) → div1_out_ggaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77))))
div1_in_ggaa(s(s(T84)), s(s(T86)), T82, s(s(T84))) → div1_out_ggaa(s(s(T84)), s(s(T86)), T82, s(s(T84)))
div1_in_ggaa(s(T91), s(T93), T89, s(T91)) → div1_out_ggaa(s(T91), s(T93), T89, s(T91))
div1_in_ggaa(T98, T100, T96, T98) → div1_out_ggaa(T98, T100, T96, T98)
U1_gaaa(T29, T15, T16, div1_out_ggaa(T29, s(0), T15, T16)) → div1_out_gaaa(s(T29), s(0), s(T15), T16)
div1_in_gaaa(s(s(T32)), s(s(0)), s(T15), T16) → U2_gaaa(T32, T15, T16, div1_in_ggaa(T32, s(s(0)), T15, T16))
U2_gaaa(T32, T15, T16, div1_out_ggaa(T32, s(s(0)), T15, T16)) → div1_out_gaaa(s(s(T32)), s(s(0)), s(T15), T16)
div1_in_gaaa(s(s(s(T35))), s(s(s(0))), s(T15), T16) → U3_gaaa(T35, T15, T16, div1_in_ggaa(T35, s(s(s(0))), T15, T16))
U3_gaaa(T35, T15, T16, div1_out_ggaa(T35, s(s(s(0))), T15, T16)) → div1_out_gaaa(s(s(s(T35))), s(s(s(0))), s(T15), T16)
div1_in_gaaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16) → U4_gaaa(T38, T15, T16, div1_in_ggaa(T38, s(s(s(s(0)))), T15, T16))
U4_gaaa(T38, T15, T16, div1_out_ggaa(T38, s(s(s(s(0)))), T15, T16)) → div1_out_gaaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16) → U5_gaaa(T41, T15, T16, div1_in_ggaa(T41, s(s(s(s(s(0))))), T15, T16))
U5_gaaa(T41, T15, T16, div1_out_ggaa(T41, s(s(s(s(s(0))))), T15, T16)) → div1_out_gaaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16) → U6_gaaa(T44, T15, T16, div1_in_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16))
U6_gaaa(T44, T15, T16, div1_out_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16)) → div1_out_gaaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U7_gaaa(T45, T46, T15, T16, minus107_in_gaa(T45, T46, X121))
minus107_in_gaa(T49, 0, T49) → minus107_out_gaa(T49, 0, T49)
minus107_in_gaa(s(T50), s(T51), X131) → U10_gaa(T50, T51, X131, minus107_in_gaa(T50, T51, X131))
U10_gaa(T50, T51, X131, minus107_out_gaa(T50, T51, X131)) → minus107_out_gaa(s(T50), s(T51), X131)
U7_gaaa(T45, T46, T15, T16, minus107_out_gaa(T45, T46, X121)) → div1_out_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U8_gaaa(T45, T46, T15, T16, minus107_in_gaa(T45, T46, T48))
U8_gaaa(T45, T46, T15, T16, minus107_out_gaa(T45, T46, T48)) → U9_gaaa(T45, T46, T15, T16, div1_in_gaaa(T48, s(T47), T15, T16))
div1_in_gaaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56))))))) → div1_out_gaaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56)))))))
div1_in_gaaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63)))))) → div1_out_gaaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63))))))
div1_in_gaaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70))))) → div1_out_gaaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70)))))
div1_in_gaaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77)))) → div1_out_gaaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77))))
div1_in_gaaa(s(s(T84)), s(s(T86)), T82, s(s(T84))) → div1_out_gaaa(s(s(T84)), s(s(T86)), T82, s(s(T84)))
div1_in_gaaa(s(T91), s(T93), T89, s(T91)) → div1_out_gaaa(s(T91), s(T93), T89, s(T91))
div1_in_gaaa(T98, T100, T96, T98) → div1_out_gaaa(T98, T100, T96, T98)
U9_gaaa(T45, T46, T15, T16, div1_out_gaaa(T48, s(T47), T15, T16)) → div1_out_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
U9_ggaa(T45, T46, T15, T16, div1_out_gaaa(T48, s(T47), T15, T16)) → div1_out_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
U6_ggaa(T44, T15, T16, div1_out_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16)) → div1_out_ggaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16)
U5_ggaa(T41, T15, T16, div1_out_ggaa(T41, s(s(s(s(s(0))))), T15, T16)) → div1_out_ggaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16)
U4_ggaa(T38, T15, T16, div1_out_ggaa(T38, s(s(s(s(0)))), T15, T16)) → div1_out_ggaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16)
U3_ggaa(T35, T15, T16, div1_out_ggaa(T35, s(s(s(0))), T15, T16)) → div1_out_ggaa(s(s(s(T35))), s(s(s(0))), s(T15), T16)
U2_ggaa(T32, T15, T16, div1_out_ggaa(T32, s(s(0)), T15, T16)) → div1_out_ggaa(s(s(T32)), s(s(0)), s(T15), T16)
U1_ggaa(T29, T15, T16, div1_out_ggaa(T29, s(0), T15, T16)) → div1_out_ggaa(s(T29), s(0), s(T15), T16)

The argument filtering Pi contains the following mapping:
div1_in_ggaa(x1, x2, x3, x4)  =  div1_in_ggaa(x1, x2)
0  =  0
div1_out_ggaa(x1, x2, x3, x4)  =  div1_out_ggaa
s(x1)  =  s(x1)
U1_ggaa(x1, x2, x3, x4)  =  U1_ggaa(x4)
U2_ggaa(x1, x2, x3, x4)  =  U2_ggaa(x4)
U3_ggaa(x1, x2, x3, x4)  =  U3_ggaa(x4)
U4_ggaa(x1, x2, x3, x4)  =  U4_ggaa(x4)
U5_ggaa(x1, x2, x3, x4)  =  U5_ggaa(x4)
U6_ggaa(x1, x2, x3, x4)  =  U6_ggaa(x4)
U7_ggaa(x1, x2, x3, x4, x5)  =  U7_ggaa(x5)
minus107_in_gga(x1, x2, x3)  =  minus107_in_gga(x1, x2)
minus107_out_gga(x1, x2, x3)  =  minus107_out_gga(x3)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x4)
U8_ggaa(x1, x2, x3, x4, x5)  =  U8_ggaa(x5)
U9_ggaa(x1, x2, x3, x4, x5)  =  U9_ggaa(x5)
div1_in_gaaa(x1, x2, x3, x4)  =  div1_in_gaaa(x1)
div1_out_gaaa(x1, x2, x3, x4)  =  div1_out_gaaa
U1_gaaa(x1, x2, x3, x4)  =  U1_gaaa(x4)
U2_gaaa(x1, x2, x3, x4)  =  U2_gaaa(x4)
U3_gaaa(x1, x2, x3, x4)  =  U3_gaaa(x4)
U4_gaaa(x1, x2, x3, x4)  =  U4_gaaa(x4)
U5_gaaa(x1, x2, x3, x4)  =  U5_gaaa(x4)
U6_gaaa(x1, x2, x3, x4)  =  U6_gaaa(x4)
U7_gaaa(x1, x2, x3, x4, x5)  =  U7_gaaa(x5)
minus107_in_gaa(x1, x2, x3)  =  minus107_in_gaa(x1)
minus107_out_gaa(x1, x2, x3)  =  minus107_out_gaa(x2, x3)
U10_gaa(x1, x2, x3, x4)  =  U10_gaa(x4)
U8_gaaa(x1, x2, x3, x4, x5)  =  U8_gaaa(x5)
U9_gaaa(x1, x2, x3, x4, x5)  =  U9_gaaa(x5)
MINUS107_IN_GGA(x1, x2, x3)  =  MINUS107_IN_GGA(x1, x2)

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

(17) UsableRulesProof (EQUIVALENT transformation)

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

(18) Obligation:

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

MINUS107_IN_GGA(s(T50), s(T51), X131) → MINUS107_IN_GGA(T50, T51, X131)

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

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

(19) PiDPToQDPProof (SOUND transformation)

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

(20) Obligation:

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

MINUS107_IN_GGA(s(T50), s(T51)) → MINUS107_IN_GGA(T50, T51)

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

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

  • MINUS107_IN_GGA(s(T50), s(T51)) → MINUS107_IN_GGA(T50, T51)
    The graph contains the following edges 1 > 1, 2 > 2

(22) TRUE

(23) Obligation:

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

DIV1_IN_GGAA(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16) → DIV1_IN_GGAA(T44, s(s(s(s(s(s(0)))))), T15, T16)

The TRS R consists of the following rules:

div1_in_ggaa(0, T10, 0, 0) → div1_out_ggaa(0, T10, 0, 0)
div1_in_ggaa(s(T29), s(0), s(T15), T16) → U1_ggaa(T29, T15, T16, div1_in_ggaa(T29, s(0), T15, T16))
div1_in_ggaa(s(s(T32)), s(s(0)), s(T15), T16) → U2_ggaa(T32, T15, T16, div1_in_ggaa(T32, s(s(0)), T15, T16))
div1_in_ggaa(s(s(s(T35))), s(s(s(0))), s(T15), T16) → U3_ggaa(T35, T15, T16, div1_in_ggaa(T35, s(s(s(0))), T15, T16))
div1_in_ggaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16) → U4_ggaa(T38, T15, T16, div1_in_ggaa(T38, s(s(s(s(0)))), T15, T16))
div1_in_ggaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16) → U5_ggaa(T41, T15, T16, div1_in_ggaa(T41, s(s(s(s(s(0))))), T15, T16))
div1_in_ggaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16) → U6_ggaa(T44, T15, T16, div1_in_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16))
div1_in_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U7_ggaa(T45, T46, T15, T16, minus107_in_gga(T45, T46, X121))
minus107_in_gga(T49, 0, T49) → minus107_out_gga(T49, 0, T49)
minus107_in_gga(s(T50), s(T51), X131) → U10_gga(T50, T51, X131, minus107_in_gga(T50, T51, X131))
U10_gga(T50, T51, X131, minus107_out_gga(T50, T51, X131)) → minus107_out_gga(s(T50), s(T51), X131)
U7_ggaa(T45, T46, T15, T16, minus107_out_gga(T45, T46, X121)) → div1_out_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
div1_in_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U8_ggaa(T45, T46, T15, T16, minus107_in_gga(T45, T46, T48))
U8_ggaa(T45, T46, T15, T16, minus107_out_gga(T45, T46, T48)) → U9_ggaa(T45, T46, T15, T16, div1_in_gaaa(T48, s(T47), T15, T16))
div1_in_gaaa(0, T10, 0, 0) → div1_out_gaaa(0, T10, 0, 0)
div1_in_gaaa(s(T29), s(0), s(T15), T16) → U1_gaaa(T29, T15, T16, div1_in_ggaa(T29, s(0), T15, T16))
div1_in_ggaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56))))))) → div1_out_ggaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56)))))))
div1_in_ggaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63)))))) → div1_out_ggaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63))))))
div1_in_ggaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70))))) → div1_out_ggaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70)))))
div1_in_ggaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77)))) → div1_out_ggaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77))))
div1_in_ggaa(s(s(T84)), s(s(T86)), T82, s(s(T84))) → div1_out_ggaa(s(s(T84)), s(s(T86)), T82, s(s(T84)))
div1_in_ggaa(s(T91), s(T93), T89, s(T91)) → div1_out_ggaa(s(T91), s(T93), T89, s(T91))
div1_in_ggaa(T98, T100, T96, T98) → div1_out_ggaa(T98, T100, T96, T98)
U1_gaaa(T29, T15, T16, div1_out_ggaa(T29, s(0), T15, T16)) → div1_out_gaaa(s(T29), s(0), s(T15), T16)
div1_in_gaaa(s(s(T32)), s(s(0)), s(T15), T16) → U2_gaaa(T32, T15, T16, div1_in_ggaa(T32, s(s(0)), T15, T16))
U2_gaaa(T32, T15, T16, div1_out_ggaa(T32, s(s(0)), T15, T16)) → div1_out_gaaa(s(s(T32)), s(s(0)), s(T15), T16)
div1_in_gaaa(s(s(s(T35))), s(s(s(0))), s(T15), T16) → U3_gaaa(T35, T15, T16, div1_in_ggaa(T35, s(s(s(0))), T15, T16))
U3_gaaa(T35, T15, T16, div1_out_ggaa(T35, s(s(s(0))), T15, T16)) → div1_out_gaaa(s(s(s(T35))), s(s(s(0))), s(T15), T16)
div1_in_gaaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16) → U4_gaaa(T38, T15, T16, div1_in_ggaa(T38, s(s(s(s(0)))), T15, T16))
U4_gaaa(T38, T15, T16, div1_out_ggaa(T38, s(s(s(s(0)))), T15, T16)) → div1_out_gaaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16) → U5_gaaa(T41, T15, T16, div1_in_ggaa(T41, s(s(s(s(s(0))))), T15, T16))
U5_gaaa(T41, T15, T16, div1_out_ggaa(T41, s(s(s(s(s(0))))), T15, T16)) → div1_out_gaaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16) → U6_gaaa(T44, T15, T16, div1_in_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16))
U6_gaaa(T44, T15, T16, div1_out_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16)) → div1_out_gaaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U7_gaaa(T45, T46, T15, T16, minus107_in_gaa(T45, T46, X121))
minus107_in_gaa(T49, 0, T49) → minus107_out_gaa(T49, 0, T49)
minus107_in_gaa(s(T50), s(T51), X131) → U10_gaa(T50, T51, X131, minus107_in_gaa(T50, T51, X131))
U10_gaa(T50, T51, X131, minus107_out_gaa(T50, T51, X131)) → minus107_out_gaa(s(T50), s(T51), X131)
U7_gaaa(T45, T46, T15, T16, minus107_out_gaa(T45, T46, X121)) → div1_out_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U8_gaaa(T45, T46, T15, T16, minus107_in_gaa(T45, T46, T48))
U8_gaaa(T45, T46, T15, T16, minus107_out_gaa(T45, T46, T48)) → U9_gaaa(T45, T46, T15, T16, div1_in_gaaa(T48, s(T47), T15, T16))
div1_in_gaaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56))))))) → div1_out_gaaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56)))))))
div1_in_gaaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63)))))) → div1_out_gaaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63))))))
div1_in_gaaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70))))) → div1_out_gaaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70)))))
div1_in_gaaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77)))) → div1_out_gaaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77))))
div1_in_gaaa(s(s(T84)), s(s(T86)), T82, s(s(T84))) → div1_out_gaaa(s(s(T84)), s(s(T86)), T82, s(s(T84)))
div1_in_gaaa(s(T91), s(T93), T89, s(T91)) → div1_out_gaaa(s(T91), s(T93), T89, s(T91))
div1_in_gaaa(T98, T100, T96, T98) → div1_out_gaaa(T98, T100, T96, T98)
U9_gaaa(T45, T46, T15, T16, div1_out_gaaa(T48, s(T47), T15, T16)) → div1_out_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
U9_ggaa(T45, T46, T15, T16, div1_out_gaaa(T48, s(T47), T15, T16)) → div1_out_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
U6_ggaa(T44, T15, T16, div1_out_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16)) → div1_out_ggaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16)
U5_ggaa(T41, T15, T16, div1_out_ggaa(T41, s(s(s(s(s(0))))), T15, T16)) → div1_out_ggaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16)
U4_ggaa(T38, T15, T16, div1_out_ggaa(T38, s(s(s(s(0)))), T15, T16)) → div1_out_ggaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16)
U3_ggaa(T35, T15, T16, div1_out_ggaa(T35, s(s(s(0))), T15, T16)) → div1_out_ggaa(s(s(s(T35))), s(s(s(0))), s(T15), T16)
U2_ggaa(T32, T15, T16, div1_out_ggaa(T32, s(s(0)), T15, T16)) → div1_out_ggaa(s(s(T32)), s(s(0)), s(T15), T16)
U1_ggaa(T29, T15, T16, div1_out_ggaa(T29, s(0), T15, T16)) → div1_out_ggaa(s(T29), s(0), s(T15), T16)

The argument filtering Pi contains the following mapping:
div1_in_ggaa(x1, x2, x3, x4)  =  div1_in_ggaa(x1, x2)
0  =  0
div1_out_ggaa(x1, x2, x3, x4)  =  div1_out_ggaa
s(x1)  =  s(x1)
U1_ggaa(x1, x2, x3, x4)  =  U1_ggaa(x4)
U2_ggaa(x1, x2, x3, x4)  =  U2_ggaa(x4)
U3_ggaa(x1, x2, x3, x4)  =  U3_ggaa(x4)
U4_ggaa(x1, x2, x3, x4)  =  U4_ggaa(x4)
U5_ggaa(x1, x2, x3, x4)  =  U5_ggaa(x4)
U6_ggaa(x1, x2, x3, x4)  =  U6_ggaa(x4)
U7_ggaa(x1, x2, x3, x4, x5)  =  U7_ggaa(x5)
minus107_in_gga(x1, x2, x3)  =  minus107_in_gga(x1, x2)
minus107_out_gga(x1, x2, x3)  =  minus107_out_gga(x3)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x4)
U8_ggaa(x1, x2, x3, x4, x5)  =  U8_ggaa(x5)
U9_ggaa(x1, x2, x3, x4, x5)  =  U9_ggaa(x5)
div1_in_gaaa(x1, x2, x3, x4)  =  div1_in_gaaa(x1)
div1_out_gaaa(x1, x2, x3, x4)  =  div1_out_gaaa
U1_gaaa(x1, x2, x3, x4)  =  U1_gaaa(x4)
U2_gaaa(x1, x2, x3, x4)  =  U2_gaaa(x4)
U3_gaaa(x1, x2, x3, x4)  =  U3_gaaa(x4)
U4_gaaa(x1, x2, x3, x4)  =  U4_gaaa(x4)
U5_gaaa(x1, x2, x3, x4)  =  U5_gaaa(x4)
U6_gaaa(x1, x2, x3, x4)  =  U6_gaaa(x4)
U7_gaaa(x1, x2, x3, x4, x5)  =  U7_gaaa(x5)
minus107_in_gaa(x1, x2, x3)  =  minus107_in_gaa(x1)
minus107_out_gaa(x1, x2, x3)  =  minus107_out_gaa(x2, x3)
U10_gaa(x1, x2, x3, x4)  =  U10_gaa(x4)
U8_gaaa(x1, x2, x3, x4, x5)  =  U8_gaaa(x5)
U9_gaaa(x1, x2, x3, x4, x5)  =  U9_gaaa(x5)
DIV1_IN_GGAA(x1, x2, x3, x4)  =  DIV1_IN_GGAA(x1, x2)

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

(24) UsableRulesProof (EQUIVALENT transformation)

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

(25) Obligation:

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

DIV1_IN_GGAA(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16) → DIV1_IN_GGAA(T44, s(s(s(s(s(s(0)))))), T15, T16)

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

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

(26) PiDPToQDPProof (SOUND transformation)

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

(27) Obligation:

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

DIV1_IN_GGAA(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0))))))) → DIV1_IN_GGAA(T44, s(s(s(s(s(s(0)))))))

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

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

  • DIV1_IN_GGAA(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0))))))) → DIV1_IN_GGAA(T44, s(s(s(s(s(s(0)))))))
    The graph contains the following edges 1 > 1, 2 >= 2

(29) TRUE

(30) Obligation:

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

DIV1_IN_GGAA(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16) → DIV1_IN_GGAA(T41, s(s(s(s(s(0))))), T15, T16)

The TRS R consists of the following rules:

div1_in_ggaa(0, T10, 0, 0) → div1_out_ggaa(0, T10, 0, 0)
div1_in_ggaa(s(T29), s(0), s(T15), T16) → U1_ggaa(T29, T15, T16, div1_in_ggaa(T29, s(0), T15, T16))
div1_in_ggaa(s(s(T32)), s(s(0)), s(T15), T16) → U2_ggaa(T32, T15, T16, div1_in_ggaa(T32, s(s(0)), T15, T16))
div1_in_ggaa(s(s(s(T35))), s(s(s(0))), s(T15), T16) → U3_ggaa(T35, T15, T16, div1_in_ggaa(T35, s(s(s(0))), T15, T16))
div1_in_ggaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16) → U4_ggaa(T38, T15, T16, div1_in_ggaa(T38, s(s(s(s(0)))), T15, T16))
div1_in_ggaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16) → U5_ggaa(T41, T15, T16, div1_in_ggaa(T41, s(s(s(s(s(0))))), T15, T16))
div1_in_ggaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16) → U6_ggaa(T44, T15, T16, div1_in_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16))
div1_in_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U7_ggaa(T45, T46, T15, T16, minus107_in_gga(T45, T46, X121))
minus107_in_gga(T49, 0, T49) → minus107_out_gga(T49, 0, T49)
minus107_in_gga(s(T50), s(T51), X131) → U10_gga(T50, T51, X131, minus107_in_gga(T50, T51, X131))
U10_gga(T50, T51, X131, minus107_out_gga(T50, T51, X131)) → minus107_out_gga(s(T50), s(T51), X131)
U7_ggaa(T45, T46, T15, T16, minus107_out_gga(T45, T46, X121)) → div1_out_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
div1_in_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U8_ggaa(T45, T46, T15, T16, minus107_in_gga(T45, T46, T48))
U8_ggaa(T45, T46, T15, T16, minus107_out_gga(T45, T46, T48)) → U9_ggaa(T45, T46, T15, T16, div1_in_gaaa(T48, s(T47), T15, T16))
div1_in_gaaa(0, T10, 0, 0) → div1_out_gaaa(0, T10, 0, 0)
div1_in_gaaa(s(T29), s(0), s(T15), T16) → U1_gaaa(T29, T15, T16, div1_in_ggaa(T29, s(0), T15, T16))
div1_in_ggaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56))))))) → div1_out_ggaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56)))))))
div1_in_ggaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63)))))) → div1_out_ggaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63))))))
div1_in_ggaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70))))) → div1_out_ggaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70)))))
div1_in_ggaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77)))) → div1_out_ggaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77))))
div1_in_ggaa(s(s(T84)), s(s(T86)), T82, s(s(T84))) → div1_out_ggaa(s(s(T84)), s(s(T86)), T82, s(s(T84)))
div1_in_ggaa(s(T91), s(T93), T89, s(T91)) → div1_out_ggaa(s(T91), s(T93), T89, s(T91))
div1_in_ggaa(T98, T100, T96, T98) → div1_out_ggaa(T98, T100, T96, T98)
U1_gaaa(T29, T15, T16, div1_out_ggaa(T29, s(0), T15, T16)) → div1_out_gaaa(s(T29), s(0), s(T15), T16)
div1_in_gaaa(s(s(T32)), s(s(0)), s(T15), T16) → U2_gaaa(T32, T15, T16, div1_in_ggaa(T32, s(s(0)), T15, T16))
U2_gaaa(T32, T15, T16, div1_out_ggaa(T32, s(s(0)), T15, T16)) → div1_out_gaaa(s(s(T32)), s(s(0)), s(T15), T16)
div1_in_gaaa(s(s(s(T35))), s(s(s(0))), s(T15), T16) → U3_gaaa(T35, T15, T16, div1_in_ggaa(T35, s(s(s(0))), T15, T16))
U3_gaaa(T35, T15, T16, div1_out_ggaa(T35, s(s(s(0))), T15, T16)) → div1_out_gaaa(s(s(s(T35))), s(s(s(0))), s(T15), T16)
div1_in_gaaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16) → U4_gaaa(T38, T15, T16, div1_in_ggaa(T38, s(s(s(s(0)))), T15, T16))
U4_gaaa(T38, T15, T16, div1_out_ggaa(T38, s(s(s(s(0)))), T15, T16)) → div1_out_gaaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16) → U5_gaaa(T41, T15, T16, div1_in_ggaa(T41, s(s(s(s(s(0))))), T15, T16))
U5_gaaa(T41, T15, T16, div1_out_ggaa(T41, s(s(s(s(s(0))))), T15, T16)) → div1_out_gaaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16) → U6_gaaa(T44, T15, T16, div1_in_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16))
U6_gaaa(T44, T15, T16, div1_out_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16)) → div1_out_gaaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U7_gaaa(T45, T46, T15, T16, minus107_in_gaa(T45, T46, X121))
minus107_in_gaa(T49, 0, T49) → minus107_out_gaa(T49, 0, T49)
minus107_in_gaa(s(T50), s(T51), X131) → U10_gaa(T50, T51, X131, minus107_in_gaa(T50, T51, X131))
U10_gaa(T50, T51, X131, minus107_out_gaa(T50, T51, X131)) → minus107_out_gaa(s(T50), s(T51), X131)
U7_gaaa(T45, T46, T15, T16, minus107_out_gaa(T45, T46, X121)) → div1_out_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U8_gaaa(T45, T46, T15, T16, minus107_in_gaa(T45, T46, T48))
U8_gaaa(T45, T46, T15, T16, minus107_out_gaa(T45, T46, T48)) → U9_gaaa(T45, T46, T15, T16, div1_in_gaaa(T48, s(T47), T15, T16))
div1_in_gaaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56))))))) → div1_out_gaaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56)))))))
div1_in_gaaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63)))))) → div1_out_gaaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63))))))
div1_in_gaaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70))))) → div1_out_gaaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70)))))
div1_in_gaaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77)))) → div1_out_gaaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77))))
div1_in_gaaa(s(s(T84)), s(s(T86)), T82, s(s(T84))) → div1_out_gaaa(s(s(T84)), s(s(T86)), T82, s(s(T84)))
div1_in_gaaa(s(T91), s(T93), T89, s(T91)) → div1_out_gaaa(s(T91), s(T93), T89, s(T91))
div1_in_gaaa(T98, T100, T96, T98) → div1_out_gaaa(T98, T100, T96, T98)
U9_gaaa(T45, T46, T15, T16, div1_out_gaaa(T48, s(T47), T15, T16)) → div1_out_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
U9_ggaa(T45, T46, T15, T16, div1_out_gaaa(T48, s(T47), T15, T16)) → div1_out_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
U6_ggaa(T44, T15, T16, div1_out_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16)) → div1_out_ggaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16)
U5_ggaa(T41, T15, T16, div1_out_ggaa(T41, s(s(s(s(s(0))))), T15, T16)) → div1_out_ggaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16)
U4_ggaa(T38, T15, T16, div1_out_ggaa(T38, s(s(s(s(0)))), T15, T16)) → div1_out_ggaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16)
U3_ggaa(T35, T15, T16, div1_out_ggaa(T35, s(s(s(0))), T15, T16)) → div1_out_ggaa(s(s(s(T35))), s(s(s(0))), s(T15), T16)
U2_ggaa(T32, T15, T16, div1_out_ggaa(T32, s(s(0)), T15, T16)) → div1_out_ggaa(s(s(T32)), s(s(0)), s(T15), T16)
U1_ggaa(T29, T15, T16, div1_out_ggaa(T29, s(0), T15, T16)) → div1_out_ggaa(s(T29), s(0), s(T15), T16)

The argument filtering Pi contains the following mapping:
div1_in_ggaa(x1, x2, x3, x4)  =  div1_in_ggaa(x1, x2)
0  =  0
div1_out_ggaa(x1, x2, x3, x4)  =  div1_out_ggaa
s(x1)  =  s(x1)
U1_ggaa(x1, x2, x3, x4)  =  U1_ggaa(x4)
U2_ggaa(x1, x2, x3, x4)  =  U2_ggaa(x4)
U3_ggaa(x1, x2, x3, x4)  =  U3_ggaa(x4)
U4_ggaa(x1, x2, x3, x4)  =  U4_ggaa(x4)
U5_ggaa(x1, x2, x3, x4)  =  U5_ggaa(x4)
U6_ggaa(x1, x2, x3, x4)  =  U6_ggaa(x4)
U7_ggaa(x1, x2, x3, x4, x5)  =  U7_ggaa(x5)
minus107_in_gga(x1, x2, x3)  =  minus107_in_gga(x1, x2)
minus107_out_gga(x1, x2, x3)  =  minus107_out_gga(x3)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x4)
U8_ggaa(x1, x2, x3, x4, x5)  =  U8_ggaa(x5)
U9_ggaa(x1, x2, x3, x4, x5)  =  U9_ggaa(x5)
div1_in_gaaa(x1, x2, x3, x4)  =  div1_in_gaaa(x1)
div1_out_gaaa(x1, x2, x3, x4)  =  div1_out_gaaa
U1_gaaa(x1, x2, x3, x4)  =  U1_gaaa(x4)
U2_gaaa(x1, x2, x3, x4)  =  U2_gaaa(x4)
U3_gaaa(x1, x2, x3, x4)  =  U3_gaaa(x4)
U4_gaaa(x1, x2, x3, x4)  =  U4_gaaa(x4)
U5_gaaa(x1, x2, x3, x4)  =  U5_gaaa(x4)
U6_gaaa(x1, x2, x3, x4)  =  U6_gaaa(x4)
U7_gaaa(x1, x2, x3, x4, x5)  =  U7_gaaa(x5)
minus107_in_gaa(x1, x2, x3)  =  minus107_in_gaa(x1)
minus107_out_gaa(x1, x2, x3)  =  minus107_out_gaa(x2, x3)
U10_gaa(x1, x2, x3, x4)  =  U10_gaa(x4)
U8_gaaa(x1, x2, x3, x4, x5)  =  U8_gaaa(x5)
U9_gaaa(x1, x2, x3, x4, x5)  =  U9_gaaa(x5)
DIV1_IN_GGAA(x1, x2, x3, x4)  =  DIV1_IN_GGAA(x1, x2)

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

(31) UsableRulesProof (EQUIVALENT transformation)

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

(32) Obligation:

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

DIV1_IN_GGAA(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16) → DIV1_IN_GGAA(T41, s(s(s(s(s(0))))), T15, T16)

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

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

(33) PiDPToQDPProof (SOUND transformation)

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

(34) Obligation:

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

DIV1_IN_GGAA(s(s(s(s(s(T41))))), s(s(s(s(s(0)))))) → DIV1_IN_GGAA(T41, s(s(s(s(s(0))))))

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

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

  • DIV1_IN_GGAA(s(s(s(s(s(T41))))), s(s(s(s(s(0)))))) → DIV1_IN_GGAA(T41, s(s(s(s(s(0))))))
    The graph contains the following edges 1 > 1, 2 >= 2

(36) TRUE

(37) Obligation:

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

DIV1_IN_GGAA(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16) → DIV1_IN_GGAA(T38, s(s(s(s(0)))), T15, T16)

The TRS R consists of the following rules:

div1_in_ggaa(0, T10, 0, 0) → div1_out_ggaa(0, T10, 0, 0)
div1_in_ggaa(s(T29), s(0), s(T15), T16) → U1_ggaa(T29, T15, T16, div1_in_ggaa(T29, s(0), T15, T16))
div1_in_ggaa(s(s(T32)), s(s(0)), s(T15), T16) → U2_ggaa(T32, T15, T16, div1_in_ggaa(T32, s(s(0)), T15, T16))
div1_in_ggaa(s(s(s(T35))), s(s(s(0))), s(T15), T16) → U3_ggaa(T35, T15, T16, div1_in_ggaa(T35, s(s(s(0))), T15, T16))
div1_in_ggaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16) → U4_ggaa(T38, T15, T16, div1_in_ggaa(T38, s(s(s(s(0)))), T15, T16))
div1_in_ggaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16) → U5_ggaa(T41, T15, T16, div1_in_ggaa(T41, s(s(s(s(s(0))))), T15, T16))
div1_in_ggaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16) → U6_ggaa(T44, T15, T16, div1_in_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16))
div1_in_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U7_ggaa(T45, T46, T15, T16, minus107_in_gga(T45, T46, X121))
minus107_in_gga(T49, 0, T49) → minus107_out_gga(T49, 0, T49)
minus107_in_gga(s(T50), s(T51), X131) → U10_gga(T50, T51, X131, minus107_in_gga(T50, T51, X131))
U10_gga(T50, T51, X131, minus107_out_gga(T50, T51, X131)) → minus107_out_gga(s(T50), s(T51), X131)
U7_ggaa(T45, T46, T15, T16, minus107_out_gga(T45, T46, X121)) → div1_out_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
div1_in_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U8_ggaa(T45, T46, T15, T16, minus107_in_gga(T45, T46, T48))
U8_ggaa(T45, T46, T15, T16, minus107_out_gga(T45, T46, T48)) → U9_ggaa(T45, T46, T15, T16, div1_in_gaaa(T48, s(T47), T15, T16))
div1_in_gaaa(0, T10, 0, 0) → div1_out_gaaa(0, T10, 0, 0)
div1_in_gaaa(s(T29), s(0), s(T15), T16) → U1_gaaa(T29, T15, T16, div1_in_ggaa(T29, s(0), T15, T16))
div1_in_ggaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56))))))) → div1_out_ggaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56)))))))
div1_in_ggaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63)))))) → div1_out_ggaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63))))))
div1_in_ggaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70))))) → div1_out_ggaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70)))))
div1_in_ggaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77)))) → div1_out_ggaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77))))
div1_in_ggaa(s(s(T84)), s(s(T86)), T82, s(s(T84))) → div1_out_ggaa(s(s(T84)), s(s(T86)), T82, s(s(T84)))
div1_in_ggaa(s(T91), s(T93), T89, s(T91)) → div1_out_ggaa(s(T91), s(T93), T89, s(T91))
div1_in_ggaa(T98, T100, T96, T98) → div1_out_ggaa(T98, T100, T96, T98)
U1_gaaa(T29, T15, T16, div1_out_ggaa(T29, s(0), T15, T16)) → div1_out_gaaa(s(T29), s(0), s(T15), T16)
div1_in_gaaa(s(s(T32)), s(s(0)), s(T15), T16) → U2_gaaa(T32, T15, T16, div1_in_ggaa(T32, s(s(0)), T15, T16))
U2_gaaa(T32, T15, T16, div1_out_ggaa(T32, s(s(0)), T15, T16)) → div1_out_gaaa(s(s(T32)), s(s(0)), s(T15), T16)
div1_in_gaaa(s(s(s(T35))), s(s(s(0))), s(T15), T16) → U3_gaaa(T35, T15, T16, div1_in_ggaa(T35, s(s(s(0))), T15, T16))
U3_gaaa(T35, T15, T16, div1_out_ggaa(T35, s(s(s(0))), T15, T16)) → div1_out_gaaa(s(s(s(T35))), s(s(s(0))), s(T15), T16)
div1_in_gaaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16) → U4_gaaa(T38, T15, T16, div1_in_ggaa(T38, s(s(s(s(0)))), T15, T16))
U4_gaaa(T38, T15, T16, div1_out_ggaa(T38, s(s(s(s(0)))), T15, T16)) → div1_out_gaaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16) → U5_gaaa(T41, T15, T16, div1_in_ggaa(T41, s(s(s(s(s(0))))), T15, T16))
U5_gaaa(T41, T15, T16, div1_out_ggaa(T41, s(s(s(s(s(0))))), T15, T16)) → div1_out_gaaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16) → U6_gaaa(T44, T15, T16, div1_in_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16))
U6_gaaa(T44, T15, T16, div1_out_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16)) → div1_out_gaaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U7_gaaa(T45, T46, T15, T16, minus107_in_gaa(T45, T46, X121))
minus107_in_gaa(T49, 0, T49) → minus107_out_gaa(T49, 0, T49)
minus107_in_gaa(s(T50), s(T51), X131) → U10_gaa(T50, T51, X131, minus107_in_gaa(T50, T51, X131))
U10_gaa(T50, T51, X131, minus107_out_gaa(T50, T51, X131)) → minus107_out_gaa(s(T50), s(T51), X131)
U7_gaaa(T45, T46, T15, T16, minus107_out_gaa(T45, T46, X121)) → div1_out_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U8_gaaa(T45, T46, T15, T16, minus107_in_gaa(T45, T46, T48))
U8_gaaa(T45, T46, T15, T16, minus107_out_gaa(T45, T46, T48)) → U9_gaaa(T45, T46, T15, T16, div1_in_gaaa(T48, s(T47), T15, T16))
div1_in_gaaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56))))))) → div1_out_gaaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56)))))))
div1_in_gaaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63)))))) → div1_out_gaaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63))))))
div1_in_gaaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70))))) → div1_out_gaaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70)))))
div1_in_gaaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77)))) → div1_out_gaaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77))))
div1_in_gaaa(s(s(T84)), s(s(T86)), T82, s(s(T84))) → div1_out_gaaa(s(s(T84)), s(s(T86)), T82, s(s(T84)))
div1_in_gaaa(s(T91), s(T93), T89, s(T91)) → div1_out_gaaa(s(T91), s(T93), T89, s(T91))
div1_in_gaaa(T98, T100, T96, T98) → div1_out_gaaa(T98, T100, T96, T98)
U9_gaaa(T45, T46, T15, T16, div1_out_gaaa(T48, s(T47), T15, T16)) → div1_out_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
U9_ggaa(T45, T46, T15, T16, div1_out_gaaa(T48, s(T47), T15, T16)) → div1_out_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
U6_ggaa(T44, T15, T16, div1_out_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16)) → div1_out_ggaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16)
U5_ggaa(T41, T15, T16, div1_out_ggaa(T41, s(s(s(s(s(0))))), T15, T16)) → div1_out_ggaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16)
U4_ggaa(T38, T15, T16, div1_out_ggaa(T38, s(s(s(s(0)))), T15, T16)) → div1_out_ggaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16)
U3_ggaa(T35, T15, T16, div1_out_ggaa(T35, s(s(s(0))), T15, T16)) → div1_out_ggaa(s(s(s(T35))), s(s(s(0))), s(T15), T16)
U2_ggaa(T32, T15, T16, div1_out_ggaa(T32, s(s(0)), T15, T16)) → div1_out_ggaa(s(s(T32)), s(s(0)), s(T15), T16)
U1_ggaa(T29, T15, T16, div1_out_ggaa(T29, s(0), T15, T16)) → div1_out_ggaa(s(T29), s(0), s(T15), T16)

The argument filtering Pi contains the following mapping:
div1_in_ggaa(x1, x2, x3, x4)  =  div1_in_ggaa(x1, x2)
0  =  0
div1_out_ggaa(x1, x2, x3, x4)  =  div1_out_ggaa
s(x1)  =  s(x1)
U1_ggaa(x1, x2, x3, x4)  =  U1_ggaa(x4)
U2_ggaa(x1, x2, x3, x4)  =  U2_ggaa(x4)
U3_ggaa(x1, x2, x3, x4)  =  U3_ggaa(x4)
U4_ggaa(x1, x2, x3, x4)  =  U4_ggaa(x4)
U5_ggaa(x1, x2, x3, x4)  =  U5_ggaa(x4)
U6_ggaa(x1, x2, x3, x4)  =  U6_ggaa(x4)
U7_ggaa(x1, x2, x3, x4, x5)  =  U7_ggaa(x5)
minus107_in_gga(x1, x2, x3)  =  minus107_in_gga(x1, x2)
minus107_out_gga(x1, x2, x3)  =  minus107_out_gga(x3)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x4)
U8_ggaa(x1, x2, x3, x4, x5)  =  U8_ggaa(x5)
U9_ggaa(x1, x2, x3, x4, x5)  =  U9_ggaa(x5)
div1_in_gaaa(x1, x2, x3, x4)  =  div1_in_gaaa(x1)
div1_out_gaaa(x1, x2, x3, x4)  =  div1_out_gaaa
U1_gaaa(x1, x2, x3, x4)  =  U1_gaaa(x4)
U2_gaaa(x1, x2, x3, x4)  =  U2_gaaa(x4)
U3_gaaa(x1, x2, x3, x4)  =  U3_gaaa(x4)
U4_gaaa(x1, x2, x3, x4)  =  U4_gaaa(x4)
U5_gaaa(x1, x2, x3, x4)  =  U5_gaaa(x4)
U6_gaaa(x1, x2, x3, x4)  =  U6_gaaa(x4)
U7_gaaa(x1, x2, x3, x4, x5)  =  U7_gaaa(x5)
minus107_in_gaa(x1, x2, x3)  =  minus107_in_gaa(x1)
minus107_out_gaa(x1, x2, x3)  =  minus107_out_gaa(x2, x3)
U10_gaa(x1, x2, x3, x4)  =  U10_gaa(x4)
U8_gaaa(x1, x2, x3, x4, x5)  =  U8_gaaa(x5)
U9_gaaa(x1, x2, x3, x4, x5)  =  U9_gaaa(x5)
DIV1_IN_GGAA(x1, x2, x3, x4)  =  DIV1_IN_GGAA(x1, x2)

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

(38) UsableRulesProof (EQUIVALENT transformation)

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

(39) Obligation:

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

DIV1_IN_GGAA(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16) → DIV1_IN_GGAA(T38, s(s(s(s(0)))), T15, T16)

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

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

(40) PiDPToQDPProof (SOUND transformation)

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

(41) Obligation:

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

DIV1_IN_GGAA(s(s(s(s(T38)))), s(s(s(s(0))))) → DIV1_IN_GGAA(T38, s(s(s(s(0)))))

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

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

  • DIV1_IN_GGAA(s(s(s(s(T38)))), s(s(s(s(0))))) → DIV1_IN_GGAA(T38, s(s(s(s(0)))))
    The graph contains the following edges 1 > 1, 2 >= 2

(43) TRUE

(44) Obligation:

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

DIV1_IN_GGAA(s(s(s(T35))), s(s(s(0))), s(T15), T16) → DIV1_IN_GGAA(T35, s(s(s(0))), T15, T16)

The TRS R consists of the following rules:

div1_in_ggaa(0, T10, 0, 0) → div1_out_ggaa(0, T10, 0, 0)
div1_in_ggaa(s(T29), s(0), s(T15), T16) → U1_ggaa(T29, T15, T16, div1_in_ggaa(T29, s(0), T15, T16))
div1_in_ggaa(s(s(T32)), s(s(0)), s(T15), T16) → U2_ggaa(T32, T15, T16, div1_in_ggaa(T32, s(s(0)), T15, T16))
div1_in_ggaa(s(s(s(T35))), s(s(s(0))), s(T15), T16) → U3_ggaa(T35, T15, T16, div1_in_ggaa(T35, s(s(s(0))), T15, T16))
div1_in_ggaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16) → U4_ggaa(T38, T15, T16, div1_in_ggaa(T38, s(s(s(s(0)))), T15, T16))
div1_in_ggaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16) → U5_ggaa(T41, T15, T16, div1_in_ggaa(T41, s(s(s(s(s(0))))), T15, T16))
div1_in_ggaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16) → U6_ggaa(T44, T15, T16, div1_in_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16))
div1_in_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U7_ggaa(T45, T46, T15, T16, minus107_in_gga(T45, T46, X121))
minus107_in_gga(T49, 0, T49) → minus107_out_gga(T49, 0, T49)
minus107_in_gga(s(T50), s(T51), X131) → U10_gga(T50, T51, X131, minus107_in_gga(T50, T51, X131))
U10_gga(T50, T51, X131, minus107_out_gga(T50, T51, X131)) → minus107_out_gga(s(T50), s(T51), X131)
U7_ggaa(T45, T46, T15, T16, minus107_out_gga(T45, T46, X121)) → div1_out_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
div1_in_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U8_ggaa(T45, T46, T15, T16, minus107_in_gga(T45, T46, T48))
U8_ggaa(T45, T46, T15, T16, minus107_out_gga(T45, T46, T48)) → U9_ggaa(T45, T46, T15, T16, div1_in_gaaa(T48, s(T47), T15, T16))
div1_in_gaaa(0, T10, 0, 0) → div1_out_gaaa(0, T10, 0, 0)
div1_in_gaaa(s(T29), s(0), s(T15), T16) → U1_gaaa(T29, T15, T16, div1_in_ggaa(T29, s(0), T15, T16))
div1_in_ggaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56))))))) → div1_out_ggaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56)))))))
div1_in_ggaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63)))))) → div1_out_ggaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63))))))
div1_in_ggaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70))))) → div1_out_ggaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70)))))
div1_in_ggaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77)))) → div1_out_ggaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77))))
div1_in_ggaa(s(s(T84)), s(s(T86)), T82, s(s(T84))) → div1_out_ggaa(s(s(T84)), s(s(T86)), T82, s(s(T84)))
div1_in_ggaa(s(T91), s(T93), T89, s(T91)) → div1_out_ggaa(s(T91), s(T93), T89, s(T91))
div1_in_ggaa(T98, T100, T96, T98) → div1_out_ggaa(T98, T100, T96, T98)
U1_gaaa(T29, T15, T16, div1_out_ggaa(T29, s(0), T15, T16)) → div1_out_gaaa(s(T29), s(0), s(T15), T16)
div1_in_gaaa(s(s(T32)), s(s(0)), s(T15), T16) → U2_gaaa(T32, T15, T16, div1_in_ggaa(T32, s(s(0)), T15, T16))
U2_gaaa(T32, T15, T16, div1_out_ggaa(T32, s(s(0)), T15, T16)) → div1_out_gaaa(s(s(T32)), s(s(0)), s(T15), T16)
div1_in_gaaa(s(s(s(T35))), s(s(s(0))), s(T15), T16) → U3_gaaa(T35, T15, T16, div1_in_ggaa(T35, s(s(s(0))), T15, T16))
U3_gaaa(T35, T15, T16, div1_out_ggaa(T35, s(s(s(0))), T15, T16)) → div1_out_gaaa(s(s(s(T35))), s(s(s(0))), s(T15), T16)
div1_in_gaaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16) → U4_gaaa(T38, T15, T16, div1_in_ggaa(T38, s(s(s(s(0)))), T15, T16))
U4_gaaa(T38, T15, T16, div1_out_ggaa(T38, s(s(s(s(0)))), T15, T16)) → div1_out_gaaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16) → U5_gaaa(T41, T15, T16, div1_in_ggaa(T41, s(s(s(s(s(0))))), T15, T16))
U5_gaaa(T41, T15, T16, div1_out_ggaa(T41, s(s(s(s(s(0))))), T15, T16)) → div1_out_gaaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16) → U6_gaaa(T44, T15, T16, div1_in_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16))
U6_gaaa(T44, T15, T16, div1_out_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16)) → div1_out_gaaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U7_gaaa(T45, T46, T15, T16, minus107_in_gaa(T45, T46, X121))
minus107_in_gaa(T49, 0, T49) → minus107_out_gaa(T49, 0, T49)
minus107_in_gaa(s(T50), s(T51), X131) → U10_gaa(T50, T51, X131, minus107_in_gaa(T50, T51, X131))
U10_gaa(T50, T51, X131, minus107_out_gaa(T50, T51, X131)) → minus107_out_gaa(s(T50), s(T51), X131)
U7_gaaa(T45, T46, T15, T16, minus107_out_gaa(T45, T46, X121)) → div1_out_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U8_gaaa(T45, T46, T15, T16, minus107_in_gaa(T45, T46, T48))
U8_gaaa(T45, T46, T15, T16, minus107_out_gaa(T45, T46, T48)) → U9_gaaa(T45, T46, T15, T16, div1_in_gaaa(T48, s(T47), T15, T16))
div1_in_gaaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56))))))) → div1_out_gaaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56)))))))
div1_in_gaaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63)))))) → div1_out_gaaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63))))))
div1_in_gaaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70))))) → div1_out_gaaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70)))))
div1_in_gaaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77)))) → div1_out_gaaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77))))
div1_in_gaaa(s(s(T84)), s(s(T86)), T82, s(s(T84))) → div1_out_gaaa(s(s(T84)), s(s(T86)), T82, s(s(T84)))
div1_in_gaaa(s(T91), s(T93), T89, s(T91)) → div1_out_gaaa(s(T91), s(T93), T89, s(T91))
div1_in_gaaa(T98, T100, T96, T98) → div1_out_gaaa(T98, T100, T96, T98)
U9_gaaa(T45, T46, T15, T16, div1_out_gaaa(T48, s(T47), T15, T16)) → div1_out_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
U9_ggaa(T45, T46, T15, T16, div1_out_gaaa(T48, s(T47), T15, T16)) → div1_out_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
U6_ggaa(T44, T15, T16, div1_out_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16)) → div1_out_ggaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16)
U5_ggaa(T41, T15, T16, div1_out_ggaa(T41, s(s(s(s(s(0))))), T15, T16)) → div1_out_ggaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16)
U4_ggaa(T38, T15, T16, div1_out_ggaa(T38, s(s(s(s(0)))), T15, T16)) → div1_out_ggaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16)
U3_ggaa(T35, T15, T16, div1_out_ggaa(T35, s(s(s(0))), T15, T16)) → div1_out_ggaa(s(s(s(T35))), s(s(s(0))), s(T15), T16)
U2_ggaa(T32, T15, T16, div1_out_ggaa(T32, s(s(0)), T15, T16)) → div1_out_ggaa(s(s(T32)), s(s(0)), s(T15), T16)
U1_ggaa(T29, T15, T16, div1_out_ggaa(T29, s(0), T15, T16)) → div1_out_ggaa(s(T29), s(0), s(T15), T16)

The argument filtering Pi contains the following mapping:
div1_in_ggaa(x1, x2, x3, x4)  =  div1_in_ggaa(x1, x2)
0  =  0
div1_out_ggaa(x1, x2, x3, x4)  =  div1_out_ggaa
s(x1)  =  s(x1)
U1_ggaa(x1, x2, x3, x4)  =  U1_ggaa(x4)
U2_ggaa(x1, x2, x3, x4)  =  U2_ggaa(x4)
U3_ggaa(x1, x2, x3, x4)  =  U3_ggaa(x4)
U4_ggaa(x1, x2, x3, x4)  =  U4_ggaa(x4)
U5_ggaa(x1, x2, x3, x4)  =  U5_ggaa(x4)
U6_ggaa(x1, x2, x3, x4)  =  U6_ggaa(x4)
U7_ggaa(x1, x2, x3, x4, x5)  =  U7_ggaa(x5)
minus107_in_gga(x1, x2, x3)  =  minus107_in_gga(x1, x2)
minus107_out_gga(x1, x2, x3)  =  minus107_out_gga(x3)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x4)
U8_ggaa(x1, x2, x3, x4, x5)  =  U8_ggaa(x5)
U9_ggaa(x1, x2, x3, x4, x5)  =  U9_ggaa(x5)
div1_in_gaaa(x1, x2, x3, x4)  =  div1_in_gaaa(x1)
div1_out_gaaa(x1, x2, x3, x4)  =  div1_out_gaaa
U1_gaaa(x1, x2, x3, x4)  =  U1_gaaa(x4)
U2_gaaa(x1, x2, x3, x4)  =  U2_gaaa(x4)
U3_gaaa(x1, x2, x3, x4)  =  U3_gaaa(x4)
U4_gaaa(x1, x2, x3, x4)  =  U4_gaaa(x4)
U5_gaaa(x1, x2, x3, x4)  =  U5_gaaa(x4)
U6_gaaa(x1, x2, x3, x4)  =  U6_gaaa(x4)
U7_gaaa(x1, x2, x3, x4, x5)  =  U7_gaaa(x5)
minus107_in_gaa(x1, x2, x3)  =  minus107_in_gaa(x1)
minus107_out_gaa(x1, x2, x3)  =  minus107_out_gaa(x2, x3)
U10_gaa(x1, x2, x3, x4)  =  U10_gaa(x4)
U8_gaaa(x1, x2, x3, x4, x5)  =  U8_gaaa(x5)
U9_gaaa(x1, x2, x3, x4, x5)  =  U9_gaaa(x5)
DIV1_IN_GGAA(x1, x2, x3, x4)  =  DIV1_IN_GGAA(x1, x2)

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

(45) UsableRulesProof (EQUIVALENT transformation)

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

(46) Obligation:

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

DIV1_IN_GGAA(s(s(s(T35))), s(s(s(0))), s(T15), T16) → DIV1_IN_GGAA(T35, s(s(s(0))), T15, T16)

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

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

(47) PiDPToQDPProof (SOUND transformation)

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

(48) Obligation:

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

DIV1_IN_GGAA(s(s(s(T35))), s(s(s(0)))) → DIV1_IN_GGAA(T35, s(s(s(0))))

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

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

  • DIV1_IN_GGAA(s(s(s(T35))), s(s(s(0)))) → DIV1_IN_GGAA(T35, s(s(s(0))))
    The graph contains the following edges 1 > 1, 2 >= 2

(50) TRUE

(51) Obligation:

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

DIV1_IN_GGAA(s(s(T32)), s(s(0)), s(T15), T16) → DIV1_IN_GGAA(T32, s(s(0)), T15, T16)

The TRS R consists of the following rules:

div1_in_ggaa(0, T10, 0, 0) → div1_out_ggaa(0, T10, 0, 0)
div1_in_ggaa(s(T29), s(0), s(T15), T16) → U1_ggaa(T29, T15, T16, div1_in_ggaa(T29, s(0), T15, T16))
div1_in_ggaa(s(s(T32)), s(s(0)), s(T15), T16) → U2_ggaa(T32, T15, T16, div1_in_ggaa(T32, s(s(0)), T15, T16))
div1_in_ggaa(s(s(s(T35))), s(s(s(0))), s(T15), T16) → U3_ggaa(T35, T15, T16, div1_in_ggaa(T35, s(s(s(0))), T15, T16))
div1_in_ggaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16) → U4_ggaa(T38, T15, T16, div1_in_ggaa(T38, s(s(s(s(0)))), T15, T16))
div1_in_ggaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16) → U5_ggaa(T41, T15, T16, div1_in_ggaa(T41, s(s(s(s(s(0))))), T15, T16))
div1_in_ggaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16) → U6_ggaa(T44, T15, T16, div1_in_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16))
div1_in_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U7_ggaa(T45, T46, T15, T16, minus107_in_gga(T45, T46, X121))
minus107_in_gga(T49, 0, T49) → minus107_out_gga(T49, 0, T49)
minus107_in_gga(s(T50), s(T51), X131) → U10_gga(T50, T51, X131, minus107_in_gga(T50, T51, X131))
U10_gga(T50, T51, X131, minus107_out_gga(T50, T51, X131)) → minus107_out_gga(s(T50), s(T51), X131)
U7_ggaa(T45, T46, T15, T16, minus107_out_gga(T45, T46, X121)) → div1_out_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
div1_in_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U8_ggaa(T45, T46, T15, T16, minus107_in_gga(T45, T46, T48))
U8_ggaa(T45, T46, T15, T16, minus107_out_gga(T45, T46, T48)) → U9_ggaa(T45, T46, T15, T16, div1_in_gaaa(T48, s(T47), T15, T16))
div1_in_gaaa(0, T10, 0, 0) → div1_out_gaaa(0, T10, 0, 0)
div1_in_gaaa(s(T29), s(0), s(T15), T16) → U1_gaaa(T29, T15, T16, div1_in_ggaa(T29, s(0), T15, T16))
div1_in_ggaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56))))))) → div1_out_ggaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56)))))))
div1_in_ggaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63)))))) → div1_out_ggaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63))))))
div1_in_ggaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70))))) → div1_out_ggaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70)))))
div1_in_ggaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77)))) → div1_out_ggaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77))))
div1_in_ggaa(s(s(T84)), s(s(T86)), T82, s(s(T84))) → div1_out_ggaa(s(s(T84)), s(s(T86)), T82, s(s(T84)))
div1_in_ggaa(s(T91), s(T93), T89, s(T91)) → div1_out_ggaa(s(T91), s(T93), T89, s(T91))
div1_in_ggaa(T98, T100, T96, T98) → div1_out_ggaa(T98, T100, T96, T98)
U1_gaaa(T29, T15, T16, div1_out_ggaa(T29, s(0), T15, T16)) → div1_out_gaaa(s(T29), s(0), s(T15), T16)
div1_in_gaaa(s(s(T32)), s(s(0)), s(T15), T16) → U2_gaaa(T32, T15, T16, div1_in_ggaa(T32, s(s(0)), T15, T16))
U2_gaaa(T32, T15, T16, div1_out_ggaa(T32, s(s(0)), T15, T16)) → div1_out_gaaa(s(s(T32)), s(s(0)), s(T15), T16)
div1_in_gaaa(s(s(s(T35))), s(s(s(0))), s(T15), T16) → U3_gaaa(T35, T15, T16, div1_in_ggaa(T35, s(s(s(0))), T15, T16))
U3_gaaa(T35, T15, T16, div1_out_ggaa(T35, s(s(s(0))), T15, T16)) → div1_out_gaaa(s(s(s(T35))), s(s(s(0))), s(T15), T16)
div1_in_gaaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16) → U4_gaaa(T38, T15, T16, div1_in_ggaa(T38, s(s(s(s(0)))), T15, T16))
U4_gaaa(T38, T15, T16, div1_out_ggaa(T38, s(s(s(s(0)))), T15, T16)) → div1_out_gaaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16) → U5_gaaa(T41, T15, T16, div1_in_ggaa(T41, s(s(s(s(s(0))))), T15, T16))
U5_gaaa(T41, T15, T16, div1_out_ggaa(T41, s(s(s(s(s(0))))), T15, T16)) → div1_out_gaaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16) → U6_gaaa(T44, T15, T16, div1_in_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16))
U6_gaaa(T44, T15, T16, div1_out_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16)) → div1_out_gaaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U7_gaaa(T45, T46, T15, T16, minus107_in_gaa(T45, T46, X121))
minus107_in_gaa(T49, 0, T49) → minus107_out_gaa(T49, 0, T49)
minus107_in_gaa(s(T50), s(T51), X131) → U10_gaa(T50, T51, X131, minus107_in_gaa(T50, T51, X131))
U10_gaa(T50, T51, X131, minus107_out_gaa(T50, T51, X131)) → minus107_out_gaa(s(T50), s(T51), X131)
U7_gaaa(T45, T46, T15, T16, minus107_out_gaa(T45, T46, X121)) → div1_out_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U8_gaaa(T45, T46, T15, T16, minus107_in_gaa(T45, T46, T48))
U8_gaaa(T45, T46, T15, T16, minus107_out_gaa(T45, T46, T48)) → U9_gaaa(T45, T46, T15, T16, div1_in_gaaa(T48, s(T47), T15, T16))
div1_in_gaaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56))))))) → div1_out_gaaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56)))))))
div1_in_gaaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63)))))) → div1_out_gaaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63))))))
div1_in_gaaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70))))) → div1_out_gaaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70)))))
div1_in_gaaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77)))) → div1_out_gaaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77))))
div1_in_gaaa(s(s(T84)), s(s(T86)), T82, s(s(T84))) → div1_out_gaaa(s(s(T84)), s(s(T86)), T82, s(s(T84)))
div1_in_gaaa(s(T91), s(T93), T89, s(T91)) → div1_out_gaaa(s(T91), s(T93), T89, s(T91))
div1_in_gaaa(T98, T100, T96, T98) → div1_out_gaaa(T98, T100, T96, T98)
U9_gaaa(T45, T46, T15, T16, div1_out_gaaa(T48, s(T47), T15, T16)) → div1_out_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
U9_ggaa(T45, T46, T15, T16, div1_out_gaaa(T48, s(T47), T15, T16)) → div1_out_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
U6_ggaa(T44, T15, T16, div1_out_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16)) → div1_out_ggaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16)
U5_ggaa(T41, T15, T16, div1_out_ggaa(T41, s(s(s(s(s(0))))), T15, T16)) → div1_out_ggaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16)
U4_ggaa(T38, T15, T16, div1_out_ggaa(T38, s(s(s(s(0)))), T15, T16)) → div1_out_ggaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16)
U3_ggaa(T35, T15, T16, div1_out_ggaa(T35, s(s(s(0))), T15, T16)) → div1_out_ggaa(s(s(s(T35))), s(s(s(0))), s(T15), T16)
U2_ggaa(T32, T15, T16, div1_out_ggaa(T32, s(s(0)), T15, T16)) → div1_out_ggaa(s(s(T32)), s(s(0)), s(T15), T16)
U1_ggaa(T29, T15, T16, div1_out_ggaa(T29, s(0), T15, T16)) → div1_out_ggaa(s(T29), s(0), s(T15), T16)

The argument filtering Pi contains the following mapping:
div1_in_ggaa(x1, x2, x3, x4)  =  div1_in_ggaa(x1, x2)
0  =  0
div1_out_ggaa(x1, x2, x3, x4)  =  div1_out_ggaa
s(x1)  =  s(x1)
U1_ggaa(x1, x2, x3, x4)  =  U1_ggaa(x4)
U2_ggaa(x1, x2, x3, x4)  =  U2_ggaa(x4)
U3_ggaa(x1, x2, x3, x4)  =  U3_ggaa(x4)
U4_ggaa(x1, x2, x3, x4)  =  U4_ggaa(x4)
U5_ggaa(x1, x2, x3, x4)  =  U5_ggaa(x4)
U6_ggaa(x1, x2, x3, x4)  =  U6_ggaa(x4)
U7_ggaa(x1, x2, x3, x4, x5)  =  U7_ggaa(x5)
minus107_in_gga(x1, x2, x3)  =  minus107_in_gga(x1, x2)
minus107_out_gga(x1, x2, x3)  =  minus107_out_gga(x3)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x4)
U8_ggaa(x1, x2, x3, x4, x5)  =  U8_ggaa(x5)
U9_ggaa(x1, x2, x3, x4, x5)  =  U9_ggaa(x5)
div1_in_gaaa(x1, x2, x3, x4)  =  div1_in_gaaa(x1)
div1_out_gaaa(x1, x2, x3, x4)  =  div1_out_gaaa
U1_gaaa(x1, x2, x3, x4)  =  U1_gaaa(x4)
U2_gaaa(x1, x2, x3, x4)  =  U2_gaaa(x4)
U3_gaaa(x1, x2, x3, x4)  =  U3_gaaa(x4)
U4_gaaa(x1, x2, x3, x4)  =  U4_gaaa(x4)
U5_gaaa(x1, x2, x3, x4)  =  U5_gaaa(x4)
U6_gaaa(x1, x2, x3, x4)  =  U6_gaaa(x4)
U7_gaaa(x1, x2, x3, x4, x5)  =  U7_gaaa(x5)
minus107_in_gaa(x1, x2, x3)  =  minus107_in_gaa(x1)
minus107_out_gaa(x1, x2, x3)  =  minus107_out_gaa(x2, x3)
U10_gaa(x1, x2, x3, x4)  =  U10_gaa(x4)
U8_gaaa(x1, x2, x3, x4, x5)  =  U8_gaaa(x5)
U9_gaaa(x1, x2, x3, x4, x5)  =  U9_gaaa(x5)
DIV1_IN_GGAA(x1, x2, x3, x4)  =  DIV1_IN_GGAA(x1, x2)

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

(52) UsableRulesProof (EQUIVALENT transformation)

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

(53) Obligation:

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

DIV1_IN_GGAA(s(s(T32)), s(s(0)), s(T15), T16) → DIV1_IN_GGAA(T32, s(s(0)), T15, T16)

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

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

(54) PiDPToQDPProof (SOUND transformation)

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

(55) Obligation:

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

DIV1_IN_GGAA(s(s(T32)), s(s(0))) → DIV1_IN_GGAA(T32, s(s(0)))

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

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

  • DIV1_IN_GGAA(s(s(T32)), s(s(0))) → DIV1_IN_GGAA(T32, s(s(0)))
    The graph contains the following edges 1 > 1, 2 >= 2

(57) TRUE

(58) Obligation:

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

DIV1_IN_GGAA(s(T29), s(0), s(T15), T16) → DIV1_IN_GGAA(T29, s(0), T15, T16)

The TRS R consists of the following rules:

div1_in_ggaa(0, T10, 0, 0) → div1_out_ggaa(0, T10, 0, 0)
div1_in_ggaa(s(T29), s(0), s(T15), T16) → U1_ggaa(T29, T15, T16, div1_in_ggaa(T29, s(0), T15, T16))
div1_in_ggaa(s(s(T32)), s(s(0)), s(T15), T16) → U2_ggaa(T32, T15, T16, div1_in_ggaa(T32, s(s(0)), T15, T16))
div1_in_ggaa(s(s(s(T35))), s(s(s(0))), s(T15), T16) → U3_ggaa(T35, T15, T16, div1_in_ggaa(T35, s(s(s(0))), T15, T16))
div1_in_ggaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16) → U4_ggaa(T38, T15, T16, div1_in_ggaa(T38, s(s(s(s(0)))), T15, T16))
div1_in_ggaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16) → U5_ggaa(T41, T15, T16, div1_in_ggaa(T41, s(s(s(s(s(0))))), T15, T16))
div1_in_ggaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16) → U6_ggaa(T44, T15, T16, div1_in_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16))
div1_in_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U7_ggaa(T45, T46, T15, T16, minus107_in_gga(T45, T46, X121))
minus107_in_gga(T49, 0, T49) → minus107_out_gga(T49, 0, T49)
minus107_in_gga(s(T50), s(T51), X131) → U10_gga(T50, T51, X131, minus107_in_gga(T50, T51, X131))
U10_gga(T50, T51, X131, minus107_out_gga(T50, T51, X131)) → minus107_out_gga(s(T50), s(T51), X131)
U7_ggaa(T45, T46, T15, T16, minus107_out_gga(T45, T46, X121)) → div1_out_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
div1_in_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U8_ggaa(T45, T46, T15, T16, minus107_in_gga(T45, T46, T48))
U8_ggaa(T45, T46, T15, T16, minus107_out_gga(T45, T46, T48)) → U9_ggaa(T45, T46, T15, T16, div1_in_gaaa(T48, s(T47), T15, T16))
div1_in_gaaa(0, T10, 0, 0) → div1_out_gaaa(0, T10, 0, 0)
div1_in_gaaa(s(T29), s(0), s(T15), T16) → U1_gaaa(T29, T15, T16, div1_in_ggaa(T29, s(0), T15, T16))
div1_in_ggaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56))))))) → div1_out_ggaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56)))))))
div1_in_ggaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63)))))) → div1_out_ggaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63))))))
div1_in_ggaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70))))) → div1_out_ggaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70)))))
div1_in_ggaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77)))) → div1_out_ggaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77))))
div1_in_ggaa(s(s(T84)), s(s(T86)), T82, s(s(T84))) → div1_out_ggaa(s(s(T84)), s(s(T86)), T82, s(s(T84)))
div1_in_ggaa(s(T91), s(T93), T89, s(T91)) → div1_out_ggaa(s(T91), s(T93), T89, s(T91))
div1_in_ggaa(T98, T100, T96, T98) → div1_out_ggaa(T98, T100, T96, T98)
U1_gaaa(T29, T15, T16, div1_out_ggaa(T29, s(0), T15, T16)) → div1_out_gaaa(s(T29), s(0), s(T15), T16)
div1_in_gaaa(s(s(T32)), s(s(0)), s(T15), T16) → U2_gaaa(T32, T15, T16, div1_in_ggaa(T32, s(s(0)), T15, T16))
U2_gaaa(T32, T15, T16, div1_out_ggaa(T32, s(s(0)), T15, T16)) → div1_out_gaaa(s(s(T32)), s(s(0)), s(T15), T16)
div1_in_gaaa(s(s(s(T35))), s(s(s(0))), s(T15), T16) → U3_gaaa(T35, T15, T16, div1_in_ggaa(T35, s(s(s(0))), T15, T16))
U3_gaaa(T35, T15, T16, div1_out_ggaa(T35, s(s(s(0))), T15, T16)) → div1_out_gaaa(s(s(s(T35))), s(s(s(0))), s(T15), T16)
div1_in_gaaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16) → U4_gaaa(T38, T15, T16, div1_in_ggaa(T38, s(s(s(s(0)))), T15, T16))
U4_gaaa(T38, T15, T16, div1_out_ggaa(T38, s(s(s(s(0)))), T15, T16)) → div1_out_gaaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16) → U5_gaaa(T41, T15, T16, div1_in_ggaa(T41, s(s(s(s(s(0))))), T15, T16))
U5_gaaa(T41, T15, T16, div1_out_ggaa(T41, s(s(s(s(s(0))))), T15, T16)) → div1_out_gaaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16) → U6_gaaa(T44, T15, T16, div1_in_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16))
U6_gaaa(T44, T15, T16, div1_out_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16)) → div1_out_gaaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U7_gaaa(T45, T46, T15, T16, minus107_in_gaa(T45, T46, X121))
minus107_in_gaa(T49, 0, T49) → minus107_out_gaa(T49, 0, T49)
minus107_in_gaa(s(T50), s(T51), X131) → U10_gaa(T50, T51, X131, minus107_in_gaa(T50, T51, X131))
U10_gaa(T50, T51, X131, minus107_out_gaa(T50, T51, X131)) → minus107_out_gaa(s(T50), s(T51), X131)
U7_gaaa(T45, T46, T15, T16, minus107_out_gaa(T45, T46, X121)) → div1_out_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U8_gaaa(T45, T46, T15, T16, minus107_in_gaa(T45, T46, T48))
U8_gaaa(T45, T46, T15, T16, minus107_out_gaa(T45, T46, T48)) → U9_gaaa(T45, T46, T15, T16, div1_in_gaaa(T48, s(T47), T15, T16))
div1_in_gaaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56))))))) → div1_out_gaaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56)))))))
div1_in_gaaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63)))))) → div1_out_gaaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63))))))
div1_in_gaaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70))))) → div1_out_gaaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70)))))
div1_in_gaaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77)))) → div1_out_gaaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77))))
div1_in_gaaa(s(s(T84)), s(s(T86)), T82, s(s(T84))) → div1_out_gaaa(s(s(T84)), s(s(T86)), T82, s(s(T84)))
div1_in_gaaa(s(T91), s(T93), T89, s(T91)) → div1_out_gaaa(s(T91), s(T93), T89, s(T91))
div1_in_gaaa(T98, T100, T96, T98) → div1_out_gaaa(T98, T100, T96, T98)
U9_gaaa(T45, T46, T15, T16, div1_out_gaaa(T48, s(T47), T15, T16)) → div1_out_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
U9_ggaa(T45, T46, T15, T16, div1_out_gaaa(T48, s(T47), T15, T16)) → div1_out_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
U6_ggaa(T44, T15, T16, div1_out_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16)) → div1_out_ggaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16)
U5_ggaa(T41, T15, T16, div1_out_ggaa(T41, s(s(s(s(s(0))))), T15, T16)) → div1_out_ggaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16)
U4_ggaa(T38, T15, T16, div1_out_ggaa(T38, s(s(s(s(0)))), T15, T16)) → div1_out_ggaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16)
U3_ggaa(T35, T15, T16, div1_out_ggaa(T35, s(s(s(0))), T15, T16)) → div1_out_ggaa(s(s(s(T35))), s(s(s(0))), s(T15), T16)
U2_ggaa(T32, T15, T16, div1_out_ggaa(T32, s(s(0)), T15, T16)) → div1_out_ggaa(s(s(T32)), s(s(0)), s(T15), T16)
U1_ggaa(T29, T15, T16, div1_out_ggaa(T29, s(0), T15, T16)) → div1_out_ggaa(s(T29), s(0), s(T15), T16)

The argument filtering Pi contains the following mapping:
div1_in_ggaa(x1, x2, x3, x4)  =  div1_in_ggaa(x1, x2)
0  =  0
div1_out_ggaa(x1, x2, x3, x4)  =  div1_out_ggaa
s(x1)  =  s(x1)
U1_ggaa(x1, x2, x3, x4)  =  U1_ggaa(x4)
U2_ggaa(x1, x2, x3, x4)  =  U2_ggaa(x4)
U3_ggaa(x1, x2, x3, x4)  =  U3_ggaa(x4)
U4_ggaa(x1, x2, x3, x4)  =  U4_ggaa(x4)
U5_ggaa(x1, x2, x3, x4)  =  U5_ggaa(x4)
U6_ggaa(x1, x2, x3, x4)  =  U6_ggaa(x4)
U7_ggaa(x1, x2, x3, x4, x5)  =  U7_ggaa(x5)
minus107_in_gga(x1, x2, x3)  =  minus107_in_gga(x1, x2)
minus107_out_gga(x1, x2, x3)  =  minus107_out_gga(x3)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x4)
U8_ggaa(x1, x2, x3, x4, x5)  =  U8_ggaa(x5)
U9_ggaa(x1, x2, x3, x4, x5)  =  U9_ggaa(x5)
div1_in_gaaa(x1, x2, x3, x4)  =  div1_in_gaaa(x1)
div1_out_gaaa(x1, x2, x3, x4)  =  div1_out_gaaa
U1_gaaa(x1, x2, x3, x4)  =  U1_gaaa(x4)
U2_gaaa(x1, x2, x3, x4)  =  U2_gaaa(x4)
U3_gaaa(x1, x2, x3, x4)  =  U3_gaaa(x4)
U4_gaaa(x1, x2, x3, x4)  =  U4_gaaa(x4)
U5_gaaa(x1, x2, x3, x4)  =  U5_gaaa(x4)
U6_gaaa(x1, x2, x3, x4)  =  U6_gaaa(x4)
U7_gaaa(x1, x2, x3, x4, x5)  =  U7_gaaa(x5)
minus107_in_gaa(x1, x2, x3)  =  minus107_in_gaa(x1)
minus107_out_gaa(x1, x2, x3)  =  minus107_out_gaa(x2, x3)
U10_gaa(x1, x2, x3, x4)  =  U10_gaa(x4)
U8_gaaa(x1, x2, x3, x4, x5)  =  U8_gaaa(x5)
U9_gaaa(x1, x2, x3, x4, x5)  =  U9_gaaa(x5)
DIV1_IN_GGAA(x1, x2, x3, x4)  =  DIV1_IN_GGAA(x1, x2)

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

(59) UsableRulesProof (EQUIVALENT transformation)

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

(60) Obligation:

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

DIV1_IN_GGAA(s(T29), s(0), s(T15), T16) → DIV1_IN_GGAA(T29, s(0), T15, T16)

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

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

(61) PiDPToQDPProof (SOUND transformation)

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

(62) Obligation:

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

DIV1_IN_GGAA(s(T29), s(0)) → DIV1_IN_GGAA(T29, s(0))

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

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

  • DIV1_IN_GGAA(s(T29), s(0)) → DIV1_IN_GGAA(T29, s(0))
    The graph contains the following edges 1 > 1, 2 >= 2

(64) TRUE

(65) Obligation:

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

DIV1_IN_GAAA(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U8_GAAA(T45, T46, T15, T16, minus107_in_gaa(T45, T46, T48))
U8_GAAA(T45, T46, T15, T16, minus107_out_gaa(T45, T46, T48)) → DIV1_IN_GAAA(T48, s(T47), T15, T16)

The TRS R consists of the following rules:

div1_in_ggaa(0, T10, 0, 0) → div1_out_ggaa(0, T10, 0, 0)
div1_in_ggaa(s(T29), s(0), s(T15), T16) → U1_ggaa(T29, T15, T16, div1_in_ggaa(T29, s(0), T15, T16))
div1_in_ggaa(s(s(T32)), s(s(0)), s(T15), T16) → U2_ggaa(T32, T15, T16, div1_in_ggaa(T32, s(s(0)), T15, T16))
div1_in_ggaa(s(s(s(T35))), s(s(s(0))), s(T15), T16) → U3_ggaa(T35, T15, T16, div1_in_ggaa(T35, s(s(s(0))), T15, T16))
div1_in_ggaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16) → U4_ggaa(T38, T15, T16, div1_in_ggaa(T38, s(s(s(s(0)))), T15, T16))
div1_in_ggaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16) → U5_ggaa(T41, T15, T16, div1_in_ggaa(T41, s(s(s(s(s(0))))), T15, T16))
div1_in_ggaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16) → U6_ggaa(T44, T15, T16, div1_in_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16))
div1_in_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U7_ggaa(T45, T46, T15, T16, minus107_in_gga(T45, T46, X121))
minus107_in_gga(T49, 0, T49) → minus107_out_gga(T49, 0, T49)
minus107_in_gga(s(T50), s(T51), X131) → U10_gga(T50, T51, X131, minus107_in_gga(T50, T51, X131))
U10_gga(T50, T51, X131, minus107_out_gga(T50, T51, X131)) → minus107_out_gga(s(T50), s(T51), X131)
U7_ggaa(T45, T46, T15, T16, minus107_out_gga(T45, T46, X121)) → div1_out_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
div1_in_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U8_ggaa(T45, T46, T15, T16, minus107_in_gga(T45, T46, T48))
U8_ggaa(T45, T46, T15, T16, minus107_out_gga(T45, T46, T48)) → U9_ggaa(T45, T46, T15, T16, div1_in_gaaa(T48, s(T47), T15, T16))
div1_in_gaaa(0, T10, 0, 0) → div1_out_gaaa(0, T10, 0, 0)
div1_in_gaaa(s(T29), s(0), s(T15), T16) → U1_gaaa(T29, T15, T16, div1_in_ggaa(T29, s(0), T15, T16))
div1_in_ggaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56))))))) → div1_out_ggaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56)))))))
div1_in_ggaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63)))))) → div1_out_ggaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63))))))
div1_in_ggaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70))))) → div1_out_ggaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70)))))
div1_in_ggaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77)))) → div1_out_ggaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77))))
div1_in_ggaa(s(s(T84)), s(s(T86)), T82, s(s(T84))) → div1_out_ggaa(s(s(T84)), s(s(T86)), T82, s(s(T84)))
div1_in_ggaa(s(T91), s(T93), T89, s(T91)) → div1_out_ggaa(s(T91), s(T93), T89, s(T91))
div1_in_ggaa(T98, T100, T96, T98) → div1_out_ggaa(T98, T100, T96, T98)
U1_gaaa(T29, T15, T16, div1_out_ggaa(T29, s(0), T15, T16)) → div1_out_gaaa(s(T29), s(0), s(T15), T16)
div1_in_gaaa(s(s(T32)), s(s(0)), s(T15), T16) → U2_gaaa(T32, T15, T16, div1_in_ggaa(T32, s(s(0)), T15, T16))
U2_gaaa(T32, T15, T16, div1_out_ggaa(T32, s(s(0)), T15, T16)) → div1_out_gaaa(s(s(T32)), s(s(0)), s(T15), T16)
div1_in_gaaa(s(s(s(T35))), s(s(s(0))), s(T15), T16) → U3_gaaa(T35, T15, T16, div1_in_ggaa(T35, s(s(s(0))), T15, T16))
U3_gaaa(T35, T15, T16, div1_out_ggaa(T35, s(s(s(0))), T15, T16)) → div1_out_gaaa(s(s(s(T35))), s(s(s(0))), s(T15), T16)
div1_in_gaaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16) → U4_gaaa(T38, T15, T16, div1_in_ggaa(T38, s(s(s(s(0)))), T15, T16))
U4_gaaa(T38, T15, T16, div1_out_ggaa(T38, s(s(s(s(0)))), T15, T16)) → div1_out_gaaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16) → U5_gaaa(T41, T15, T16, div1_in_ggaa(T41, s(s(s(s(s(0))))), T15, T16))
U5_gaaa(T41, T15, T16, div1_out_ggaa(T41, s(s(s(s(s(0))))), T15, T16)) → div1_out_gaaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16) → U6_gaaa(T44, T15, T16, div1_in_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16))
U6_gaaa(T44, T15, T16, div1_out_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16)) → div1_out_gaaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U7_gaaa(T45, T46, T15, T16, minus107_in_gaa(T45, T46, X121))
minus107_in_gaa(T49, 0, T49) → minus107_out_gaa(T49, 0, T49)
minus107_in_gaa(s(T50), s(T51), X131) → U10_gaa(T50, T51, X131, minus107_in_gaa(T50, T51, X131))
U10_gaa(T50, T51, X131, minus107_out_gaa(T50, T51, X131)) → minus107_out_gaa(s(T50), s(T51), X131)
U7_gaaa(T45, T46, T15, T16, minus107_out_gaa(T45, T46, X121)) → div1_out_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
div1_in_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U8_gaaa(T45, T46, T15, T16, minus107_in_gaa(T45, T46, T48))
U8_gaaa(T45, T46, T15, T16, minus107_out_gaa(T45, T46, T48)) → U9_gaaa(T45, T46, T15, T16, div1_in_gaaa(T48, s(T47), T15, T16))
div1_in_gaaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56))))))) → div1_out_gaaa(s(s(s(s(s(s(T56)))))), s(s(s(s(s(s(T58)))))), T54, s(s(s(s(s(s(T56)))))))
div1_in_gaaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63)))))) → div1_out_gaaa(s(s(s(s(s(T63))))), s(s(s(s(s(T65))))), T61, s(s(s(s(s(T63))))))
div1_in_gaaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70))))) → div1_out_gaaa(s(s(s(s(T70)))), s(s(s(s(T72)))), T68, s(s(s(s(T70)))))
div1_in_gaaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77)))) → div1_out_gaaa(s(s(s(T77))), s(s(s(T79))), T75, s(s(s(T77))))
div1_in_gaaa(s(s(T84)), s(s(T86)), T82, s(s(T84))) → div1_out_gaaa(s(s(T84)), s(s(T86)), T82, s(s(T84)))
div1_in_gaaa(s(T91), s(T93), T89, s(T91)) → div1_out_gaaa(s(T91), s(T93), T89, s(T91))
div1_in_gaaa(T98, T100, T96, T98) → div1_out_gaaa(T98, T100, T96, T98)
U9_gaaa(T45, T46, T15, T16, div1_out_gaaa(T48, s(T47), T15, T16)) → div1_out_gaaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
U9_ggaa(T45, T46, T15, T16, div1_out_gaaa(T48, s(T47), T15, T16)) → div1_out_ggaa(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16)
U6_ggaa(T44, T15, T16, div1_out_ggaa(T44, s(s(s(s(s(s(0)))))), T15, T16)) → div1_out_ggaa(s(s(s(s(s(s(T44)))))), s(s(s(s(s(s(0)))))), s(T15), T16)
U5_ggaa(T41, T15, T16, div1_out_ggaa(T41, s(s(s(s(s(0))))), T15, T16)) → div1_out_ggaa(s(s(s(s(s(T41))))), s(s(s(s(s(0))))), s(T15), T16)
U4_ggaa(T38, T15, T16, div1_out_ggaa(T38, s(s(s(s(0)))), T15, T16)) → div1_out_ggaa(s(s(s(s(T38)))), s(s(s(s(0)))), s(T15), T16)
U3_ggaa(T35, T15, T16, div1_out_ggaa(T35, s(s(s(0))), T15, T16)) → div1_out_ggaa(s(s(s(T35))), s(s(s(0))), s(T15), T16)
U2_ggaa(T32, T15, T16, div1_out_ggaa(T32, s(s(0)), T15, T16)) → div1_out_ggaa(s(s(T32)), s(s(0)), s(T15), T16)
U1_ggaa(T29, T15, T16, div1_out_ggaa(T29, s(0), T15, T16)) → div1_out_ggaa(s(T29), s(0), s(T15), T16)

The argument filtering Pi contains the following mapping:
div1_in_ggaa(x1, x2, x3, x4)  =  div1_in_ggaa(x1, x2)
0  =  0
div1_out_ggaa(x1, x2, x3, x4)  =  div1_out_ggaa
s(x1)  =  s(x1)
U1_ggaa(x1, x2, x3, x4)  =  U1_ggaa(x4)
U2_ggaa(x1, x2, x3, x4)  =  U2_ggaa(x4)
U3_ggaa(x1, x2, x3, x4)  =  U3_ggaa(x4)
U4_ggaa(x1, x2, x3, x4)  =  U4_ggaa(x4)
U5_ggaa(x1, x2, x3, x4)  =  U5_ggaa(x4)
U6_ggaa(x1, x2, x3, x4)  =  U6_ggaa(x4)
U7_ggaa(x1, x2, x3, x4, x5)  =  U7_ggaa(x5)
minus107_in_gga(x1, x2, x3)  =  minus107_in_gga(x1, x2)
minus107_out_gga(x1, x2, x3)  =  minus107_out_gga(x3)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x4)
U8_ggaa(x1, x2, x3, x4, x5)  =  U8_ggaa(x5)
U9_ggaa(x1, x2, x3, x4, x5)  =  U9_ggaa(x5)
div1_in_gaaa(x1, x2, x3, x4)  =  div1_in_gaaa(x1)
div1_out_gaaa(x1, x2, x3, x4)  =  div1_out_gaaa
U1_gaaa(x1, x2, x3, x4)  =  U1_gaaa(x4)
U2_gaaa(x1, x2, x3, x4)  =  U2_gaaa(x4)
U3_gaaa(x1, x2, x3, x4)  =  U3_gaaa(x4)
U4_gaaa(x1, x2, x3, x4)  =  U4_gaaa(x4)
U5_gaaa(x1, x2, x3, x4)  =  U5_gaaa(x4)
U6_gaaa(x1, x2, x3, x4)  =  U6_gaaa(x4)
U7_gaaa(x1, x2, x3, x4, x5)  =  U7_gaaa(x5)
minus107_in_gaa(x1, x2, x3)  =  minus107_in_gaa(x1)
minus107_out_gaa(x1, x2, x3)  =  minus107_out_gaa(x2, x3)
U10_gaa(x1, x2, x3, x4)  =  U10_gaa(x4)
U8_gaaa(x1, x2, x3, x4, x5)  =  U8_gaaa(x5)
U9_gaaa(x1, x2, x3, x4, x5)  =  U9_gaaa(x5)
DIV1_IN_GAAA(x1, x2, x3, x4)  =  DIV1_IN_GAAA(x1)
U8_GAAA(x1, x2, x3, x4, x5)  =  U8_GAAA(x5)

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

(66) UsableRulesProof (EQUIVALENT transformation)

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

(67) Obligation:

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

DIV1_IN_GAAA(s(s(s(s(s(s(s(T45))))))), s(s(s(s(s(s(s(T46))))))), s(T15), T16) → U8_GAAA(T45, T46, T15, T16, minus107_in_gaa(T45, T46, T48))
U8_GAAA(T45, T46, T15, T16, minus107_out_gaa(T45, T46, T48)) → DIV1_IN_GAAA(T48, s(T47), T15, T16)

The TRS R consists of the following rules:

minus107_in_gaa(T49, 0, T49) → minus107_out_gaa(T49, 0, T49)
minus107_in_gaa(s(T50), s(T51), X131) → U10_gaa(T50, T51, X131, minus107_in_gaa(T50, T51, X131))
U10_gaa(T50, T51, X131, minus107_out_gaa(T50, T51, X131)) → minus107_out_gaa(s(T50), s(T51), X131)

The argument filtering Pi contains the following mapping:
0  =  0
s(x1)  =  s(x1)
minus107_in_gaa(x1, x2, x3)  =  minus107_in_gaa(x1)
minus107_out_gaa(x1, x2, x3)  =  minus107_out_gaa(x2, x3)
U10_gaa(x1, x2, x3, x4)  =  U10_gaa(x4)
DIV1_IN_GAAA(x1, x2, x3, x4)  =  DIV1_IN_GAAA(x1)
U8_GAAA(x1, x2, x3, x4, x5)  =  U8_GAAA(x5)

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

(68) PiDPToQDPProof (SOUND transformation)

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

(69) Obligation:

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

DIV1_IN_GAAA(s(s(s(s(s(s(s(T45)))))))) → U8_GAAA(minus107_in_gaa(T45))
U8_GAAA(minus107_out_gaa(T46, T48)) → DIV1_IN_GAAA(T48)

The TRS R consists of the following rules:

minus107_in_gaa(T49) → minus107_out_gaa(0, T49)
minus107_in_gaa(s(T50)) → U10_gaa(minus107_in_gaa(T50))
U10_gaa(minus107_out_gaa(T51, X131)) → minus107_out_gaa(s(T51), X131)

The set Q consists of the following terms:

minus107_in_gaa(x0)
U10_gaa(x0)

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

(70) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

DIV1_IN_GAAA(s(s(s(s(s(s(s(T45)))))))) → U8_GAAA(minus107_in_gaa(T45))
U8_GAAA(minus107_out_gaa(T46, T48)) → DIV1_IN_GAAA(T48)

Strictly oriented rules of the TRS R:

minus107_in_gaa(T49) → minus107_out_gaa(0, T49)

Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(DIV1_IN_GAAA(x1)) = x1   
POL(U10_gaa(x1)) = 1 + x1   
POL(U8_GAAA(x1)) = x1   
POL(minus107_in_gaa(x1)) = 2 + x1   
POL(minus107_out_gaa(x1, x2)) = 1 + x1 + x2   
POL(s(x1)) = 1 + x1   

(71) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

minus107_in_gaa(s(T50)) → U10_gaa(minus107_in_gaa(T50))
U10_gaa(minus107_out_gaa(T51, X131)) → minus107_out_gaa(s(T51), X131)

The set Q consists of the following terms:

minus107_in_gaa(x0)
U10_gaa(x0)

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

(72) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(73) TRUE