0 Prolog
↳1 CutEliminatorProof (⇐)
↳2 Prolog
↳3 PrologToPiTRSProof (⇐)
↳4 PiTRS
↳5 DependencyPairsProof (⇔)
↳6 PiDP
↳7 DependencyGraphProof (⇔)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔)
↳11 PiDP
↳12 PiDPToQDPProof (⇐)
↳13 QDP
↳14 UsableRulesReductionPairsProof (⇔)
↳15 QDP
↳16 Narrowing (⇐)
↳17 QDP
↳18 UsableRulesProof (⇔)
↳19 QDP
↳20 QReductionProof (⇔)
↳21 QDP
↳22 Instantiation (⇔)
↳23 QDP
↳24 NonTerminationProof (⇔)
↳25 FALSE
↳26 PiDP
↳27 UsableRulesProof (⇔)
↳28 PiDP
↳29 PiDPToQDPProof (⇐)
↳30 QDP
↳31 UsableRulesReductionPairsProof (⇔)
↳32 QDP
↳33 Narrowing (⇐)
↳34 QDP
↳35 UsableRulesProof (⇔)
↳36 QDP
↳37 QReductionProof (⇔)
↳38 QDP
↳39 Instantiation (⇔)
↳40 QDP
↳41 NonTerminationProof (⇔)
↳42 FALSE
↳43 PiDP
↳44 UsableRulesProof (⇔)
↳45 PiDP
↳46 PiDPToQDPProof (⇐)
↳47 QDP
↳48 Rewriting (⇔)
↳49 QDP
↳50 UsableRulesProof (⇔)
↳51 QDP
↳52 QReductionProof (⇔)
↳53 QDP
↳54 Rewriting (⇔)
↳55 QDP
↳56 Rewriting (⇔)
↳57 QDP
↳58 UsableRulesProof (⇔)
↳59 QDP
↳60 QReductionProof (⇔)
↳61 QDP
↳62 Rewriting (⇔)
↳63 QDP
↳64 UsableRulesProof (⇔)
↳65 QDP
↳66 QReductionProof (⇔)
↳67 QDP
↳68 Rewriting (⇔)
↳69 QDP
↳70 UsableRulesProof (⇔)
↳71 QDP
↳72 QReductionProof (⇔)
↳73 QDP
↳74 NonTerminationProof (⇔)
↳75 FALSE
↳76 PiDP
↳77 UsableRulesProof (⇔)
↳78 PiDP
↳79 PiDPToQDPProof (⇐)
↳80 QDP
↳81 UsableRulesReductionPairsProof (⇔)
↳82 QDP
↳83 Narrowing (⇐)
↳84 QDP
↳85 UsableRulesProof (⇔)
↳86 QDP
↳87 QReductionProof (⇔)
↳88 QDP
↳89 Narrowing (⇐)
↳90 QDP
↳91 UsableRulesProof (⇔)
↳92 QDP
↳93 QReductionProof (⇔)
↳94 QDP
↳95 Instantiation (⇔)
↳96 QDP
↳97 NonTerminationProof (⇔)
↳98 FALSE
↳99 PrologToPiTRSProof (⇐)
↳100 PiTRS
↳101 DependencyPairsProof (⇔)
↳102 PiDP
↳103 DependencyGraphProof (⇔)
↳104 AND
↳105 PiDP
↳106 UsableRulesProof (⇔)
↳107 PiDP
↳108 PiDPToQDPProof (⇐)
↳109 QDP
↳110 Narrowing (⇐)
↳111 QDP
↳112 UsableRulesProof (⇔)
↳113 QDP
↳114 QReductionProof (⇔)
↳115 QDP
↳116 Instantiation (⇔)
↳117 QDP
↳118 DependencyGraphProof (⇔)
↳119 AND
↳120 QDP
↳121 NonTerminationProof (⇔)
↳122 FALSE
↳123 QDP
↳124 QDPSizeChangeProof (⇔)
↳125 TRUE
↳126 PiDP
↳127 UsableRulesProof (⇔)
↳128 PiDP
↳129 PiDPToQDPProof (⇐)
↳130 QDP
↳131 Narrowing (⇐)
↳132 QDP
↳133 UsableRulesProof (⇔)
↳134 QDP
↳135 QReductionProof (⇔)
↳136 QDP
↳137 Instantiation (⇔)
↳138 QDP
↳139 DependencyGraphProof (⇔)
↳140 AND
↳141 QDP
↳142 NonTerminationProof (⇔)
↳143 FALSE
↳144 QDP
↳145 QDPSizeChangeProof (⇔)
↳146 TRUE
↳147 PiDP
↳148 UsableRulesProof (⇔)
↳149 PiDP
↳150 PiDPToQDPProof (⇐)
↳151 QDP
↳152 Rewriting (⇔)
↳153 QDP
↳154 UsableRulesProof (⇔)
↳155 QDP
↳156 QReductionProof (⇔)
↳157 QDP
↳158 Rewriting (⇔)
↳159 QDP
↳160 Rewriting (⇔)
↳161 QDP
↳162 UsableRulesProof (⇔)
↳163 QDP
↳164 QReductionProof (⇔)
↳165 QDP
↳166 Rewriting (⇔)
↳167 QDP
↳168 UsableRulesProof (⇔)
↳169 QDP
↳170 QReductionProof (⇔)
↳171 QDP
↳172 Rewriting (⇔)
↳173 QDP
↳174 UsableRulesProof (⇔)
↳175 QDP
↳176 QReductionProof (⇔)
↳177 QDP
↳178 NonTerminationProof (⇔)
↳179 FALSE
↳180 PiDP
↳181 UsableRulesProof (⇔)
↳182 PiDP
↳183 PiDPToQDPProof (⇐)
↳184 QDP
↳185 Narrowing (⇐)
↳186 QDP
↳187 UsableRulesProof (⇔)
↳188 QDP
↳189 QReductionProof (⇔)
↳190 QDP
↳191 Narrowing (⇐)
↳192 QDP
↳193 UsableRulesProof (⇔)
↳194 QDP
↳195 QReductionProof (⇔)
↳196 QDP
↳197 Instantiation (⇔)
↳198 QDP
↳199 Instantiation (⇔)
↳200 QDP
↳201 DependencyGraphProof (⇔)
↳202 AND
↳203 QDP
↳204 NonTerminationProof (⇔)
↳205 FALSE
↳206 QDP
↳207 QDPSizeChangeProof (⇔)
↳208 TRUE
convert_in_gga([], X1, Z) → U1_gga(X1, Z, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U1_gga(X1, Z, eq_out_ag(Z, 0)) → convert_out_gga([], X1, Z)
convert_in_gga(X, Y, Z) → U2_gga(X, Y, Z, head_in_gg(X, 0))
head_in_gg([], X2) → head_out_gg([], X2)
head_in_gg(.(H, X3), H) → head_out_gg(.(H, X3), H)
U2_gga(X, Y, Z, head_out_gg(X, 0)) → U3_gga(X, Y, Z, tail_in_ga(X, T))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X4, Xs), Xs) → tail_out_ga(.(X4, Xs), Xs)
U3_gga(X, Y, Z, tail_out_ga(X, T)) → U4_gga(X, Y, Z, T, convert_in_gga(T, Y, U))
convert_in_gga(X, Y, Z) → U6_gga(X, Y, Z, head_in_ga(X, H))
head_in_ga([], X2) → head_out_ga([], X2)
head_in_ga(.(H, X3), H) → head_out_ga(.(H, X3), H)
U6_gga(X, Y, Z, head_out_ga(X, H)) → U7_gga(X, Y, Z, H, p_in_aa(H, P))
p_in_aa(s(X), X) → p_out_aa(s(X), X)
p_in_aa(0, 0) → p_out_aa(0, 0)
U7_gga(X, Y, Z, H, p_out_aa(H, P)) → U8_gga(X, Y, Z, H, P, tail_in_ga(X, T))
U8_gga(X, Y, Z, H, P, tail_out_ga(X, T)) → U9_gga(X, Y, Z, H, P, T, convert_in_aga(.(P, T), Y, U))
convert_in_aga([], X1, Z) → U1_aga(X1, Z, eq_in_ag(Z, 0))
U1_aga(X1, Z, eq_out_ag(Z, 0)) → convert_out_aga([], X1, Z)
convert_in_aga(X, Y, Z) → U2_aga(X, Y, Z, head_in_ag(X, 0))
head_in_ag([], X2) → head_out_ag([], X2)
head_in_ag(.(H, X3), H) → head_out_ag(.(H, X3), H)
U2_aga(X, Y, Z, head_out_ag(X, 0)) → U3_aga(X, Y, Z, tail_in_aa(X, T))
tail_in_aa([], []) → tail_out_aa([], [])
tail_in_aa(.(X4, Xs), Xs) → tail_out_aa(.(X4, Xs), Xs)
U3_aga(X, Y, Z, tail_out_aa(X, T)) → U4_aga(X, Y, Z, T, convert_in_aga(T, Y, U))
convert_in_aga(X, Y, Z) → U6_aga(X, Y, Z, head_in_aa(X, H))
head_in_aa([], X2) → head_out_aa([], X2)
head_in_aa(.(H, X3), H) → head_out_aa(.(H, X3), H)
U6_aga(X, Y, Z, head_out_aa(X, H)) → U7_aga(X, Y, Z, H, p_in_aa(H, P))
U7_aga(X, Y, Z, H, p_out_aa(H, P)) → U8_aga(X, Y, Z, H, P, tail_in_aa(X, T))
U8_aga(X, Y, Z, H, P, tail_out_aa(X, T)) → U9_aga(X, Y, Z, H, P, T, convert_in_aga(.(P, T), Y, U))
U9_aga(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → U10_aga(X, Y, Z, p_in_ag(Z, U))
p_in_ag(s(X), X) → p_out_ag(s(X), X)
p_in_ag(0, 0) → p_out_ag(0, 0)
U10_aga(X, Y, Z, p_out_ag(Z, U)) → convert_out_aga(X, Y, Z)
U4_aga(X, Y, Z, T, convert_out_aga(T, Y, U)) → U5_aga(X, Y, Z, times_in_gga(U, Y, Z))
times_in_gga(0, Y, Z) → U11_gga(Y, Z, eq_in_ag(Z, 0))
U11_gga(Y, Z, eq_out_ag(Z, 0)) → times_out_gga(0, Y, Z)
times_in_gga(X, Y, Z) → U12_gga(X, Y, Z, p_in_ga(X, P))
p_in_ga(s(X), X) → p_out_ga(s(X), X)
p_in_ga(0, 0) → p_out_ga(0, 0)
U12_gga(X, Y, Z, p_out_ga(X, P)) → U13_gga(X, Y, Z, P, times_in_gga(P, Y, U))
U13_gga(X, Y, Z, P, times_out_gga(P, Y, U)) → U14_gga(X, Y, Z, plus_in_gga(Y, U, Z))
plus_in_gga(0, Y, Z) → U15_gga(Y, Z, eq_in_ga(Y, Z))
eq_in_ga(X, X) → eq_out_ga(X, X)
U15_gga(Y, Z, eq_out_ga(Y, Z)) → plus_out_gga(0, Y, Z)
plus_in_gga(X, Y, Z) → U16_gga(X, Y, Z, p_in_ga(X, P))
U16_gga(X, Y, Z, p_out_ga(X, P)) → U17_gga(X, Y, Z, P, plus_in_gga(P, Y, U))
U17_gga(X, Y, Z, P, plus_out_gga(P, Y, U)) → U18_gga(X, Y, Z, p_in_ag(Z, U))
U18_gga(X, Y, Z, p_out_ag(Z, U)) → plus_out_gga(X, Y, Z)
U14_gga(X, Y, Z, plus_out_gga(Y, U, Z)) → times_out_gga(X, Y, Z)
U5_aga(X, Y, Z, times_out_gga(U, Y, Z)) → convert_out_aga(X, Y, Z)
U9_gga(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → U10_gga(X, Y, Z, p_in_ag(Z, U))
U10_gga(X, Y, Z, p_out_ag(Z, U)) → convert_out_gga(X, Y, Z)
U4_gga(X, Y, Z, T, convert_out_gga(T, Y, U)) → U5_gga(X, Y, Z, times_in_gga(U, Y, Z))
U5_gga(X, Y, Z, times_out_gga(U, Y, Z)) → convert_out_gga(X, Y, Z)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
convert_in_gga([], X1, Z) → U1_gga(X1, Z, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U1_gga(X1, Z, eq_out_ag(Z, 0)) → convert_out_gga([], X1, Z)
convert_in_gga(X, Y, Z) → U2_gga(X, Y, Z, head_in_gg(X, 0))
head_in_gg([], X2) → head_out_gg([], X2)
head_in_gg(.(H, X3), H) → head_out_gg(.(H, X3), H)
U2_gga(X, Y, Z, head_out_gg(X, 0)) → U3_gga(X, Y, Z, tail_in_ga(X, T))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X4, Xs), Xs) → tail_out_ga(.(X4, Xs), Xs)
U3_gga(X, Y, Z, tail_out_ga(X, T)) → U4_gga(X, Y, Z, T, convert_in_gga(T, Y, U))
convert_in_gga(X, Y, Z) → U6_gga(X, Y, Z, head_in_ga(X, H))
head_in_ga([], X2) → head_out_ga([], X2)
head_in_ga(.(H, X3), H) → head_out_ga(.(H, X3), H)
U6_gga(X, Y, Z, head_out_ga(X, H)) → U7_gga(X, Y, Z, H, p_in_aa(H, P))
p_in_aa(s(X), X) → p_out_aa(s(X), X)
p_in_aa(0, 0) → p_out_aa(0, 0)
U7_gga(X, Y, Z, H, p_out_aa(H, P)) → U8_gga(X, Y, Z, H, P, tail_in_ga(X, T))
U8_gga(X, Y, Z, H, P, tail_out_ga(X, T)) → U9_gga(X, Y, Z, H, P, T, convert_in_aga(.(P, T), Y, U))
convert_in_aga([], X1, Z) → U1_aga(X1, Z, eq_in_ag(Z, 0))
U1_aga(X1, Z, eq_out_ag(Z, 0)) → convert_out_aga([], X1, Z)
convert_in_aga(X, Y, Z) → U2_aga(X, Y, Z, head_in_ag(X, 0))
head_in_ag([], X2) → head_out_ag([], X2)
head_in_ag(.(H, X3), H) → head_out_ag(.(H, X3), H)
U2_aga(X, Y, Z, head_out_ag(X, 0)) → U3_aga(X, Y, Z, tail_in_aa(X, T))
tail_in_aa([], []) → tail_out_aa([], [])
tail_in_aa(.(X4, Xs), Xs) → tail_out_aa(.(X4, Xs), Xs)
U3_aga(X, Y, Z, tail_out_aa(X, T)) → U4_aga(X, Y, Z, T, convert_in_aga(T, Y, U))
convert_in_aga(X, Y, Z) → U6_aga(X, Y, Z, head_in_aa(X, H))
head_in_aa([], X2) → head_out_aa([], X2)
head_in_aa(.(H, X3), H) → head_out_aa(.(H, X3), H)
U6_aga(X, Y, Z, head_out_aa(X, H)) → U7_aga(X, Y, Z, H, p_in_aa(H, P))
U7_aga(X, Y, Z, H, p_out_aa(H, P)) → U8_aga(X, Y, Z, H, P, tail_in_aa(X, T))
U8_aga(X, Y, Z, H, P, tail_out_aa(X, T)) → U9_aga(X, Y, Z, H, P, T, convert_in_aga(.(P, T), Y, U))
U9_aga(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → U10_aga(X, Y, Z, p_in_ag(Z, U))
p_in_ag(s(X), X) → p_out_ag(s(X), X)
p_in_ag(0, 0) → p_out_ag(0, 0)
U10_aga(X, Y, Z, p_out_ag(Z, U)) → convert_out_aga(X, Y, Z)
U4_aga(X, Y, Z, T, convert_out_aga(T, Y, U)) → U5_aga(X, Y, Z, times_in_gga(U, Y, Z))
times_in_gga(0, Y, Z) → U11_gga(Y, Z, eq_in_ag(Z, 0))
U11_gga(Y, Z, eq_out_ag(Z, 0)) → times_out_gga(0, Y, Z)
times_in_gga(X, Y, Z) → U12_gga(X, Y, Z, p_in_ga(X, P))
p_in_ga(s(X), X) → p_out_ga(s(X), X)
p_in_ga(0, 0) → p_out_ga(0, 0)
U12_gga(X, Y, Z, p_out_ga(X, P)) → U13_gga(X, Y, Z, P, times_in_gga(P, Y, U))
U13_gga(X, Y, Z, P, times_out_gga(P, Y, U)) → U14_gga(X, Y, Z, plus_in_gga(Y, U, Z))
plus_in_gga(0, Y, Z) → U15_gga(Y, Z, eq_in_ga(Y, Z))
eq_in_ga(X, X) → eq_out_ga(X, X)
U15_gga(Y, Z, eq_out_ga(Y, Z)) → plus_out_gga(0, Y, Z)
plus_in_gga(X, Y, Z) → U16_gga(X, Y, Z, p_in_ga(X, P))
U16_gga(X, Y, Z, p_out_ga(X, P)) → U17_gga(X, Y, Z, P, plus_in_gga(P, Y, U))
U17_gga(X, Y, Z, P, plus_out_gga(P, Y, U)) → U18_gga(X, Y, Z, p_in_ag(Z, U))
U18_gga(X, Y, Z, p_out_ag(Z, U)) → plus_out_gga(X, Y, Z)
U14_gga(X, Y, Z, plus_out_gga(Y, U, Z)) → times_out_gga(X, Y, Z)
U5_aga(X, Y, Z, times_out_gga(U, Y, Z)) → convert_out_aga(X, Y, Z)
U9_gga(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → U10_gga(X, Y, Z, p_in_ag(Z, U))
U10_gga(X, Y, Z, p_out_ag(Z, U)) → convert_out_gga(X, Y, Z)
U4_gga(X, Y, Z, T, convert_out_gga(T, Y, U)) → U5_gga(X, Y, Z, times_in_gga(U, Y, Z))
U5_gga(X, Y, Z, times_out_gga(U, Y, Z)) → convert_out_gga(X, Y, Z)
CONVERT_IN_GGA([], X1, Z) → U1_GGA(X1, Z, eq_in_ag(Z, 0))
CONVERT_IN_GGA([], X1, Z) → EQ_IN_AG(Z, 0)
CONVERT_IN_GGA(X, Y, Z) → U2_GGA(X, Y, Z, head_in_gg(X, 0))
CONVERT_IN_GGA(X, Y, Z) → HEAD_IN_GG(X, 0)
U2_GGA(X, Y, Z, head_out_gg(X, 0)) → U3_GGA(X, Y, Z, tail_in_ga(X, T))
U2_GGA(X, Y, Z, head_out_gg(X, 0)) → TAIL_IN_GA(X, T)
U3_GGA(X, Y, Z, tail_out_ga(X, T)) → U4_GGA(X, Y, Z, T, convert_in_gga(T, Y, U))
U3_GGA(X, Y, Z, tail_out_ga(X, T)) → CONVERT_IN_GGA(T, Y, U)
CONVERT_IN_GGA(X, Y, Z) → U6_GGA(X, Y, Z, head_in_ga(X, H))
CONVERT_IN_GGA(X, Y, Z) → HEAD_IN_GA(X, H)
U6_GGA(X, Y, Z, head_out_ga(X, H)) → U7_GGA(X, Y, Z, H, p_in_aa(H, P))
U6_GGA(X, Y, Z, head_out_ga(X, H)) → P_IN_AA(H, P)
U7_GGA(X, Y, Z, H, p_out_aa(H, P)) → U8_GGA(X, Y, Z, H, P, tail_in_ga(X, T))
U7_GGA(X, Y, Z, H, p_out_aa(H, P)) → TAIL_IN_GA(X, T)
U8_GGA(X, Y, Z, H, P, tail_out_ga(X, T)) → U9_GGA(X, Y, Z, H, P, T, convert_in_aga(.(P, T), Y, U))
U8_GGA(X, Y, Z, H, P, tail_out_ga(X, T)) → CONVERT_IN_AGA(.(P, T), Y, U)
CONVERT_IN_AGA([], X1, Z) → U1_AGA(X1, Z, eq_in_ag(Z, 0))
CONVERT_IN_AGA([], X1, Z) → EQ_IN_AG(Z, 0)
CONVERT_IN_AGA(X, Y, Z) → U2_AGA(X, Y, Z, head_in_ag(X, 0))
CONVERT_IN_AGA(X, Y, Z) → HEAD_IN_AG(X, 0)
U2_AGA(X, Y, Z, head_out_ag(X, 0)) → U3_AGA(X, Y, Z, tail_in_aa(X, T))
U2_AGA(X, Y, Z, head_out_ag(X, 0)) → TAIL_IN_AA(X, T)
U3_AGA(X, Y, Z, tail_out_aa(X, T)) → U4_AGA(X, Y, Z, T, convert_in_aga(T, Y, U))
U3_AGA(X, Y, Z, tail_out_aa(X, T)) → CONVERT_IN_AGA(T, Y, U)
CONVERT_IN_AGA(X, Y, Z) → U6_AGA(X, Y, Z, head_in_aa(X, H))
CONVERT_IN_AGA(X, Y, Z) → HEAD_IN_AA(X, H)
U6_AGA(X, Y, Z, head_out_aa(X, H)) → U7_AGA(X, Y, Z, H, p_in_aa(H, P))
U6_AGA(X, Y, Z, head_out_aa(X, H)) → P_IN_AA(H, P)
U7_AGA(X, Y, Z, H, p_out_aa(H, P)) → U8_AGA(X, Y, Z, H, P, tail_in_aa(X, T))
U7_AGA(X, Y, Z, H, p_out_aa(H, P)) → TAIL_IN_AA(X, T)
U8_AGA(X, Y, Z, H, P, tail_out_aa(X, T)) → U9_AGA(X, Y, Z, H, P, T, convert_in_aga(.(P, T), Y, U))
U8_AGA(X, Y, Z, H, P, tail_out_aa(X, T)) → CONVERT_IN_AGA(.(P, T), Y, U)
U9_AGA(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → U10_AGA(X, Y, Z, p_in_ag(Z, U))
U9_AGA(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → P_IN_AG(Z, U)
U4_AGA(X, Y, Z, T, convert_out_aga(T, Y, U)) → U5_AGA(X, Y, Z, times_in_gga(U, Y, Z))
U4_AGA(X, Y, Z, T, convert_out_aga(T, Y, U)) → TIMES_IN_GGA(U, Y, Z)
TIMES_IN_GGA(0, Y, Z) → U11_GGA(Y, Z, eq_in_ag(Z, 0))
TIMES_IN_GGA(0, Y, Z) → EQ_IN_AG(Z, 0)
TIMES_IN_GGA(X, Y, Z) → U12_GGA(X, Y, Z, p_in_ga(X, P))
TIMES_IN_GGA(X, Y, Z) → P_IN_GA(X, P)
U12_GGA(X, Y, Z, p_out_ga(X, P)) → U13_GGA(X, Y, Z, P, times_in_gga(P, Y, U))
U12_GGA(X, Y, Z, p_out_ga(X, P)) → TIMES_IN_GGA(P, Y, U)
U13_GGA(X, Y, Z, P, times_out_gga(P, Y, U)) → U14_GGA(X, Y, Z, plus_in_gga(Y, U, Z))
U13_GGA(X, Y, Z, P, times_out_gga(P, Y, U)) → PLUS_IN_GGA(Y, U, Z)
PLUS_IN_GGA(0, Y, Z) → U15_GGA(Y, Z, eq_in_ga(Y, Z))
PLUS_IN_GGA(0, Y, Z) → EQ_IN_GA(Y, Z)
PLUS_IN_GGA(X, Y, Z) → U16_GGA(X, Y, Z, p_in_ga(X, P))
PLUS_IN_GGA(X, Y, Z) → P_IN_GA(X, P)
U16_GGA(X, Y, Z, p_out_ga(X, P)) → U17_GGA(X, Y, Z, P, plus_in_gga(P, Y, U))
U16_GGA(X, Y, Z, p_out_ga(X, P)) → PLUS_IN_GGA(P, Y, U)
U17_GGA(X, Y, Z, P, plus_out_gga(P, Y, U)) → U18_GGA(X, Y, Z, p_in_ag(Z, U))
U17_GGA(X, Y, Z, P, plus_out_gga(P, Y, U)) → P_IN_AG(Z, U)
U9_GGA(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → U10_GGA(X, Y, Z, p_in_ag(Z, U))
U9_GGA(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → P_IN_AG(Z, U)
U4_GGA(X, Y, Z, T, convert_out_gga(T, Y, U)) → U5_GGA(X, Y, Z, times_in_gga(U, Y, Z))
U4_GGA(X, Y, Z, T, convert_out_gga(T, Y, U)) → TIMES_IN_GGA(U, Y, Z)
convert_in_gga([], X1, Z) → U1_gga(X1, Z, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U1_gga(X1, Z, eq_out_ag(Z, 0)) → convert_out_gga([], X1, Z)
convert_in_gga(X, Y, Z) → U2_gga(X, Y, Z, head_in_gg(X, 0))
head_in_gg([], X2) → head_out_gg([], X2)
head_in_gg(.(H, X3), H) → head_out_gg(.(H, X3), H)
U2_gga(X, Y, Z, head_out_gg(X, 0)) → U3_gga(X, Y, Z, tail_in_ga(X, T))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X4, Xs), Xs) → tail_out_ga(.(X4, Xs), Xs)
U3_gga(X, Y, Z, tail_out_ga(X, T)) → U4_gga(X, Y, Z, T, convert_in_gga(T, Y, U))
convert_in_gga(X, Y, Z) → U6_gga(X, Y, Z, head_in_ga(X, H))
head_in_ga([], X2) → head_out_ga([], X2)
head_in_ga(.(H, X3), H) → head_out_ga(.(H, X3), H)
U6_gga(X, Y, Z, head_out_ga(X, H)) → U7_gga(X, Y, Z, H, p_in_aa(H, P))
p_in_aa(s(X), X) → p_out_aa(s(X), X)
p_in_aa(0, 0) → p_out_aa(0, 0)
U7_gga(X, Y, Z, H, p_out_aa(H, P)) → U8_gga(X, Y, Z, H, P, tail_in_ga(X, T))
U8_gga(X, Y, Z, H, P, tail_out_ga(X, T)) → U9_gga(X, Y, Z, H, P, T, convert_in_aga(.(P, T), Y, U))
convert_in_aga([], X1, Z) → U1_aga(X1, Z, eq_in_ag(Z, 0))
U1_aga(X1, Z, eq_out_ag(Z, 0)) → convert_out_aga([], X1, Z)
convert_in_aga(X, Y, Z) → U2_aga(X, Y, Z, head_in_ag(X, 0))
head_in_ag([], X2) → head_out_ag([], X2)
head_in_ag(.(H, X3), H) → head_out_ag(.(H, X3), H)
U2_aga(X, Y, Z, head_out_ag(X, 0)) → U3_aga(X, Y, Z, tail_in_aa(X, T))
tail_in_aa([], []) → tail_out_aa([], [])
tail_in_aa(.(X4, Xs), Xs) → tail_out_aa(.(X4, Xs), Xs)
U3_aga(X, Y, Z, tail_out_aa(X, T)) → U4_aga(X, Y, Z, T, convert_in_aga(T, Y, U))
convert_in_aga(X, Y, Z) → U6_aga(X, Y, Z, head_in_aa(X, H))
head_in_aa([], X2) → head_out_aa([], X2)
head_in_aa(.(H, X3), H) → head_out_aa(.(H, X3), H)
U6_aga(X, Y, Z, head_out_aa(X, H)) → U7_aga(X, Y, Z, H, p_in_aa(H, P))
U7_aga(X, Y, Z, H, p_out_aa(H, P)) → U8_aga(X, Y, Z, H, P, tail_in_aa(X, T))
U8_aga(X, Y, Z, H, P, tail_out_aa(X, T)) → U9_aga(X, Y, Z, H, P, T, convert_in_aga(.(P, T), Y, U))
U9_aga(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → U10_aga(X, Y, Z, p_in_ag(Z, U))
p_in_ag(s(X), X) → p_out_ag(s(X), X)
p_in_ag(0, 0) → p_out_ag(0, 0)
U10_aga(X, Y, Z, p_out_ag(Z, U)) → convert_out_aga(X, Y, Z)
U4_aga(X, Y, Z, T, convert_out_aga(T, Y, U)) → U5_aga(X, Y, Z, times_in_gga(U, Y, Z))
times_in_gga(0, Y, Z) → U11_gga(Y, Z, eq_in_ag(Z, 0))
U11_gga(Y, Z, eq_out_ag(Z, 0)) → times_out_gga(0, Y, Z)
times_in_gga(X, Y, Z) → U12_gga(X, Y, Z, p_in_ga(X, P))
p_in_ga(s(X), X) → p_out_ga(s(X), X)
p_in_ga(0, 0) → p_out_ga(0, 0)
U12_gga(X, Y, Z, p_out_ga(X, P)) → U13_gga(X, Y, Z, P, times_in_gga(P, Y, U))
U13_gga(X, Y, Z, P, times_out_gga(P, Y, U)) → U14_gga(X, Y, Z, plus_in_gga(Y, U, Z))
plus_in_gga(0, Y, Z) → U15_gga(Y, Z, eq_in_ga(Y, Z))
eq_in_ga(X, X) → eq_out_ga(X, X)
U15_gga(Y, Z, eq_out_ga(Y, Z)) → plus_out_gga(0, Y, Z)
plus_in_gga(X, Y, Z) → U16_gga(X, Y, Z, p_in_ga(X, P))
U16_gga(X, Y, Z, p_out_ga(X, P)) → U17_gga(X, Y, Z, P, plus_in_gga(P, Y, U))
U17_gga(X, Y, Z, P, plus_out_gga(P, Y, U)) → U18_gga(X, Y, Z, p_in_ag(Z, U))
U18_gga(X, Y, Z, p_out_ag(Z, U)) → plus_out_gga(X, Y, Z)
U14_gga(X, Y, Z, plus_out_gga(Y, U, Z)) → times_out_gga(X, Y, Z)
U5_aga(X, Y, Z, times_out_gga(U, Y, Z)) → convert_out_aga(X, Y, Z)
U9_gga(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → U10_gga(X, Y, Z, p_in_ag(Z, U))
U10_gga(X, Y, Z, p_out_ag(Z, U)) → convert_out_gga(X, Y, Z)
U4_gga(X, Y, Z, T, convert_out_gga(T, Y, U)) → U5_gga(X, Y, Z, times_in_gga(U, Y, Z))
U5_gga(X, Y, Z, times_out_gga(U, Y, Z)) → convert_out_gga(X, Y, Z)
CONVERT_IN_GGA([], X1, Z) → U1_GGA(X1, Z, eq_in_ag(Z, 0))
CONVERT_IN_GGA([], X1, Z) → EQ_IN_AG(Z, 0)
CONVERT_IN_GGA(X, Y, Z) → U2_GGA(X, Y, Z, head_in_gg(X, 0))
CONVERT_IN_GGA(X, Y, Z) → HEAD_IN_GG(X, 0)
U2_GGA(X, Y, Z, head_out_gg(X, 0)) → U3_GGA(X, Y, Z, tail_in_ga(X, T))
U2_GGA(X, Y, Z, head_out_gg(X, 0)) → TAIL_IN_GA(X, T)
U3_GGA(X, Y, Z, tail_out_ga(X, T)) → U4_GGA(X, Y, Z, T, convert_in_gga(T, Y, U))
U3_GGA(X, Y, Z, tail_out_ga(X, T)) → CONVERT_IN_GGA(T, Y, U)
CONVERT_IN_GGA(X, Y, Z) → U6_GGA(X, Y, Z, head_in_ga(X, H))
CONVERT_IN_GGA(X, Y, Z) → HEAD_IN_GA(X, H)
U6_GGA(X, Y, Z, head_out_ga(X, H)) → U7_GGA(X, Y, Z, H, p_in_aa(H, P))
U6_GGA(X, Y, Z, head_out_ga(X, H)) → P_IN_AA(H, P)
U7_GGA(X, Y, Z, H, p_out_aa(H, P)) → U8_GGA(X, Y, Z, H, P, tail_in_ga(X, T))
U7_GGA(X, Y, Z, H, p_out_aa(H, P)) → TAIL_IN_GA(X, T)
U8_GGA(X, Y, Z, H, P, tail_out_ga(X, T)) → U9_GGA(X, Y, Z, H, P, T, convert_in_aga(.(P, T), Y, U))
U8_GGA(X, Y, Z, H, P, tail_out_ga(X, T)) → CONVERT_IN_AGA(.(P, T), Y, U)
CONVERT_IN_AGA([], X1, Z) → U1_AGA(X1, Z, eq_in_ag(Z, 0))
CONVERT_IN_AGA([], X1, Z) → EQ_IN_AG(Z, 0)
CONVERT_IN_AGA(X, Y, Z) → U2_AGA(X, Y, Z, head_in_ag(X, 0))
CONVERT_IN_AGA(X, Y, Z) → HEAD_IN_AG(X, 0)
U2_AGA(X, Y, Z, head_out_ag(X, 0)) → U3_AGA(X, Y, Z, tail_in_aa(X, T))
U2_AGA(X, Y, Z, head_out_ag(X, 0)) → TAIL_IN_AA(X, T)
U3_AGA(X, Y, Z, tail_out_aa(X, T)) → U4_AGA(X, Y, Z, T, convert_in_aga(T, Y, U))
U3_AGA(X, Y, Z, tail_out_aa(X, T)) → CONVERT_IN_AGA(T, Y, U)
CONVERT_IN_AGA(X, Y, Z) → U6_AGA(X, Y, Z, head_in_aa(X, H))
CONVERT_IN_AGA(X, Y, Z) → HEAD_IN_AA(X, H)
U6_AGA(X, Y, Z, head_out_aa(X, H)) → U7_AGA(X, Y, Z, H, p_in_aa(H, P))
U6_AGA(X, Y, Z, head_out_aa(X, H)) → P_IN_AA(H, P)
U7_AGA(X, Y, Z, H, p_out_aa(H, P)) → U8_AGA(X, Y, Z, H, P, tail_in_aa(X, T))
U7_AGA(X, Y, Z, H, p_out_aa(H, P)) → TAIL_IN_AA(X, T)
U8_AGA(X, Y, Z, H, P, tail_out_aa(X, T)) → U9_AGA(X, Y, Z, H, P, T, convert_in_aga(.(P, T), Y, U))
U8_AGA(X, Y, Z, H, P, tail_out_aa(X, T)) → CONVERT_IN_AGA(.(P, T), Y, U)
U9_AGA(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → U10_AGA(X, Y, Z, p_in_ag(Z, U))
U9_AGA(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → P_IN_AG(Z, U)
U4_AGA(X, Y, Z, T, convert_out_aga(T, Y, U)) → U5_AGA(X, Y, Z, times_in_gga(U, Y, Z))
U4_AGA(X, Y, Z, T, convert_out_aga(T, Y, U)) → TIMES_IN_GGA(U, Y, Z)
TIMES_IN_GGA(0, Y, Z) → U11_GGA(Y, Z, eq_in_ag(Z, 0))
TIMES_IN_GGA(0, Y, Z) → EQ_IN_AG(Z, 0)
TIMES_IN_GGA(X, Y, Z) → U12_GGA(X, Y, Z, p_in_ga(X, P))
TIMES_IN_GGA(X, Y, Z) → P_IN_GA(X, P)
U12_GGA(X, Y, Z, p_out_ga(X, P)) → U13_GGA(X, Y, Z, P, times_in_gga(P, Y, U))
U12_GGA(X, Y, Z, p_out_ga(X, P)) → TIMES_IN_GGA(P, Y, U)
U13_GGA(X, Y, Z, P, times_out_gga(P, Y, U)) → U14_GGA(X, Y, Z, plus_in_gga(Y, U, Z))
U13_GGA(X, Y, Z, P, times_out_gga(P, Y, U)) → PLUS_IN_GGA(Y, U, Z)
PLUS_IN_GGA(0, Y, Z) → U15_GGA(Y, Z, eq_in_ga(Y, Z))
PLUS_IN_GGA(0, Y, Z) → EQ_IN_GA(Y, Z)
PLUS_IN_GGA(X, Y, Z) → U16_GGA(X, Y, Z, p_in_ga(X, P))
PLUS_IN_GGA(X, Y, Z) → P_IN_GA(X, P)
U16_GGA(X, Y, Z, p_out_ga(X, P)) → U17_GGA(X, Y, Z, P, plus_in_gga(P, Y, U))
U16_GGA(X, Y, Z, p_out_ga(X, P)) → PLUS_IN_GGA(P, Y, U)
U17_GGA(X, Y, Z, P, plus_out_gga(P, Y, U)) → U18_GGA(X, Y, Z, p_in_ag(Z, U))
U17_GGA(X, Y, Z, P, plus_out_gga(P, Y, U)) → P_IN_AG(Z, U)
U9_GGA(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → U10_GGA(X, Y, Z, p_in_ag(Z, U))
U9_GGA(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → P_IN_AG(Z, U)
U4_GGA(X, Y, Z, T, convert_out_gga(T, Y, U)) → U5_GGA(X, Y, Z, times_in_gga(U, Y, Z))
U4_GGA(X, Y, Z, T, convert_out_gga(T, Y, U)) → TIMES_IN_GGA(U, Y, Z)
convert_in_gga([], X1, Z) → U1_gga(X1, Z, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U1_gga(X1, Z, eq_out_ag(Z, 0)) → convert_out_gga([], X1, Z)
convert_in_gga(X, Y, Z) → U2_gga(X, Y, Z, head_in_gg(X, 0))
head_in_gg([], X2) → head_out_gg([], X2)
head_in_gg(.(H, X3), H) → head_out_gg(.(H, X3), H)
U2_gga(X, Y, Z, head_out_gg(X, 0)) → U3_gga(X, Y, Z, tail_in_ga(X, T))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X4, Xs), Xs) → tail_out_ga(.(X4, Xs), Xs)
U3_gga(X, Y, Z, tail_out_ga(X, T)) → U4_gga(X, Y, Z, T, convert_in_gga(T, Y, U))
convert_in_gga(X, Y, Z) → U6_gga(X, Y, Z, head_in_ga(X, H))
head_in_ga([], X2) → head_out_ga([], X2)
head_in_ga(.(H, X3), H) → head_out_ga(.(H, X3), H)
U6_gga(X, Y, Z, head_out_ga(X, H)) → U7_gga(X, Y, Z, H, p_in_aa(H, P))
p_in_aa(s(X), X) → p_out_aa(s(X), X)
p_in_aa(0, 0) → p_out_aa(0, 0)
U7_gga(X, Y, Z, H, p_out_aa(H, P)) → U8_gga(X, Y, Z, H, P, tail_in_ga(X, T))
U8_gga(X, Y, Z, H, P, tail_out_ga(X, T)) → U9_gga(X, Y, Z, H, P, T, convert_in_aga(.(P, T), Y, U))
convert_in_aga([], X1, Z) → U1_aga(X1, Z, eq_in_ag(Z, 0))
U1_aga(X1, Z, eq_out_ag(Z, 0)) → convert_out_aga([], X1, Z)
convert_in_aga(X, Y, Z) → U2_aga(X, Y, Z, head_in_ag(X, 0))
head_in_ag([], X2) → head_out_ag([], X2)
head_in_ag(.(H, X3), H) → head_out_ag(.(H, X3), H)
U2_aga(X, Y, Z, head_out_ag(X, 0)) → U3_aga(X, Y, Z, tail_in_aa(X, T))
tail_in_aa([], []) → tail_out_aa([], [])
tail_in_aa(.(X4, Xs), Xs) → tail_out_aa(.(X4, Xs), Xs)
U3_aga(X, Y, Z, tail_out_aa(X, T)) → U4_aga(X, Y, Z, T, convert_in_aga(T, Y, U))
convert_in_aga(X, Y, Z) → U6_aga(X, Y, Z, head_in_aa(X, H))
head_in_aa([], X2) → head_out_aa([], X2)
head_in_aa(.(H, X3), H) → head_out_aa(.(H, X3), H)
U6_aga(X, Y, Z, head_out_aa(X, H)) → U7_aga(X, Y, Z, H, p_in_aa(H, P))
U7_aga(X, Y, Z, H, p_out_aa(H, P)) → U8_aga(X, Y, Z, H, P, tail_in_aa(X, T))
U8_aga(X, Y, Z, H, P, tail_out_aa(X, T)) → U9_aga(X, Y, Z, H, P, T, convert_in_aga(.(P, T), Y, U))
U9_aga(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → U10_aga(X, Y, Z, p_in_ag(Z, U))
p_in_ag(s(X), X) → p_out_ag(s(X), X)
p_in_ag(0, 0) → p_out_ag(0, 0)
U10_aga(X, Y, Z, p_out_ag(Z, U)) → convert_out_aga(X, Y, Z)
U4_aga(X, Y, Z, T, convert_out_aga(T, Y, U)) → U5_aga(X, Y, Z, times_in_gga(U, Y, Z))
times_in_gga(0, Y, Z) → U11_gga(Y, Z, eq_in_ag(Z, 0))
U11_gga(Y, Z, eq_out_ag(Z, 0)) → times_out_gga(0, Y, Z)
times_in_gga(X, Y, Z) → U12_gga(X, Y, Z, p_in_ga(X, P))
p_in_ga(s(X), X) → p_out_ga(s(X), X)
p_in_ga(0, 0) → p_out_ga(0, 0)
U12_gga(X, Y, Z, p_out_ga(X, P)) → U13_gga(X, Y, Z, P, times_in_gga(P, Y, U))
U13_gga(X, Y, Z, P, times_out_gga(P, Y, U)) → U14_gga(X, Y, Z, plus_in_gga(Y, U, Z))
plus_in_gga(0, Y, Z) → U15_gga(Y, Z, eq_in_ga(Y, Z))
eq_in_ga(X, X) → eq_out_ga(X, X)
U15_gga(Y, Z, eq_out_ga(Y, Z)) → plus_out_gga(0, Y, Z)
plus_in_gga(X, Y, Z) → U16_gga(X, Y, Z, p_in_ga(X, P))
U16_gga(X, Y, Z, p_out_ga(X, P)) → U17_gga(X, Y, Z, P, plus_in_gga(P, Y, U))
U17_gga(X, Y, Z, P, plus_out_gga(P, Y, U)) → U18_gga(X, Y, Z, p_in_ag(Z, U))
U18_gga(X, Y, Z, p_out_ag(Z, U)) → plus_out_gga(X, Y, Z)
U14_gga(X, Y, Z, plus_out_gga(Y, U, Z)) → times_out_gga(X, Y, Z)
U5_aga(X, Y, Z, times_out_gga(U, Y, Z)) → convert_out_aga(X, Y, Z)
U9_gga(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → U10_gga(X, Y, Z, p_in_ag(Z, U))
U10_gga(X, Y, Z, p_out_ag(Z, U)) → convert_out_gga(X, Y, Z)
U4_gga(X, Y, Z, T, convert_out_gga(T, Y, U)) → U5_gga(X, Y, Z, times_in_gga(U, Y, Z))
U5_gga(X, Y, Z, times_out_gga(U, Y, Z)) → convert_out_gga(X, Y, Z)
PLUS_IN_GGA(X, Y, Z) → U16_GGA(X, Y, Z, p_in_ga(X, P))
U16_GGA(X, Y, Z, p_out_ga(X, P)) → PLUS_IN_GGA(P, Y, U)
convert_in_gga([], X1, Z) → U1_gga(X1, Z, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U1_gga(X1, Z, eq_out_ag(Z, 0)) → convert_out_gga([], X1, Z)
convert_in_gga(X, Y, Z) → U2_gga(X, Y, Z, head_in_gg(X, 0))
head_in_gg([], X2) → head_out_gg([], X2)
head_in_gg(.(H, X3), H) → head_out_gg(.(H, X3), H)
U2_gga(X, Y, Z, head_out_gg(X, 0)) → U3_gga(X, Y, Z, tail_in_ga(X, T))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X4, Xs), Xs) → tail_out_ga(.(X4, Xs), Xs)
U3_gga(X, Y, Z, tail_out_ga(X, T)) → U4_gga(X, Y, Z, T, convert_in_gga(T, Y, U))
convert_in_gga(X, Y, Z) → U6_gga(X, Y, Z, head_in_ga(X, H))
head_in_ga([], X2) → head_out_ga([], X2)
head_in_ga(.(H, X3), H) → head_out_ga(.(H, X3), H)
U6_gga(X, Y, Z, head_out_ga(X, H)) → U7_gga(X, Y, Z, H, p_in_aa(H, P))
p_in_aa(s(X), X) → p_out_aa(s(X), X)
p_in_aa(0, 0) → p_out_aa(0, 0)
U7_gga(X, Y, Z, H, p_out_aa(H, P)) → U8_gga(X, Y, Z, H, P, tail_in_ga(X, T))
U8_gga(X, Y, Z, H, P, tail_out_ga(X, T)) → U9_gga(X, Y, Z, H, P, T, convert_in_aga(.(P, T), Y, U))
convert_in_aga([], X1, Z) → U1_aga(X1, Z, eq_in_ag(Z, 0))
U1_aga(X1, Z, eq_out_ag(Z, 0)) → convert_out_aga([], X1, Z)
convert_in_aga(X, Y, Z) → U2_aga(X, Y, Z, head_in_ag(X, 0))
head_in_ag([], X2) → head_out_ag([], X2)
head_in_ag(.(H, X3), H) → head_out_ag(.(H, X3), H)
U2_aga(X, Y, Z, head_out_ag(X, 0)) → U3_aga(X, Y, Z, tail_in_aa(X, T))
tail_in_aa([], []) → tail_out_aa([], [])
tail_in_aa(.(X4, Xs), Xs) → tail_out_aa(.(X4, Xs), Xs)
U3_aga(X, Y, Z, tail_out_aa(X, T)) → U4_aga(X, Y, Z, T, convert_in_aga(T, Y, U))
convert_in_aga(X, Y, Z) → U6_aga(X, Y, Z, head_in_aa(X, H))
head_in_aa([], X2) → head_out_aa([], X2)
head_in_aa(.(H, X3), H) → head_out_aa(.(H, X3), H)
U6_aga(X, Y, Z, head_out_aa(X, H)) → U7_aga(X, Y, Z, H, p_in_aa(H, P))
U7_aga(X, Y, Z, H, p_out_aa(H, P)) → U8_aga(X, Y, Z, H, P, tail_in_aa(X, T))
U8_aga(X, Y, Z, H, P, tail_out_aa(X, T)) → U9_aga(X, Y, Z, H, P, T, convert_in_aga(.(P, T), Y, U))
U9_aga(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → U10_aga(X, Y, Z, p_in_ag(Z, U))
p_in_ag(s(X), X) → p_out_ag(s(X), X)
p_in_ag(0, 0) → p_out_ag(0, 0)
U10_aga(X, Y, Z, p_out_ag(Z, U)) → convert_out_aga(X, Y, Z)
U4_aga(X, Y, Z, T, convert_out_aga(T, Y, U)) → U5_aga(X, Y, Z, times_in_gga(U, Y, Z))
times_in_gga(0, Y, Z) → U11_gga(Y, Z, eq_in_ag(Z, 0))
U11_gga(Y, Z, eq_out_ag(Z, 0)) → times_out_gga(0, Y, Z)
times_in_gga(X, Y, Z) → U12_gga(X, Y, Z, p_in_ga(X, P))
p_in_ga(s(X), X) → p_out_ga(s(X), X)
p_in_ga(0, 0) → p_out_ga(0, 0)
U12_gga(X, Y, Z, p_out_ga(X, P)) → U13_gga(X, Y, Z, P, times_in_gga(P, Y, U))
U13_gga(X, Y, Z, P, times_out_gga(P, Y, U)) → U14_gga(X, Y, Z, plus_in_gga(Y, U, Z))
plus_in_gga(0, Y, Z) → U15_gga(Y, Z, eq_in_ga(Y, Z))
eq_in_ga(X, X) → eq_out_ga(X, X)
U15_gga(Y, Z, eq_out_ga(Y, Z)) → plus_out_gga(0, Y, Z)
plus_in_gga(X, Y, Z) → U16_gga(X, Y, Z, p_in_ga(X, P))
U16_gga(X, Y, Z, p_out_ga(X, P)) → U17_gga(X, Y, Z, P, plus_in_gga(P, Y, U))
U17_gga(X, Y, Z, P, plus_out_gga(P, Y, U)) → U18_gga(X, Y, Z, p_in_ag(Z, U))
U18_gga(X, Y, Z, p_out_ag(Z, U)) → plus_out_gga(X, Y, Z)
U14_gga(X, Y, Z, plus_out_gga(Y, U, Z)) → times_out_gga(X, Y, Z)
U5_aga(X, Y, Z, times_out_gga(U, Y, Z)) → convert_out_aga(X, Y, Z)
U9_gga(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → U10_gga(X, Y, Z, p_in_ag(Z, U))
U10_gga(X, Y, Z, p_out_ag(Z, U)) → convert_out_gga(X, Y, Z)
U4_gga(X, Y, Z, T, convert_out_gga(T, Y, U)) → U5_gga(X, Y, Z, times_in_gga(U, Y, Z))
U5_gga(X, Y, Z, times_out_gga(U, Y, Z)) → convert_out_gga(X, Y, Z)
PLUS_IN_GGA(X, Y, Z) → U16_GGA(X, Y, Z, p_in_ga(X, P))
U16_GGA(X, Y, Z, p_out_ga(X, P)) → PLUS_IN_GGA(P, Y, U)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
p_in_ga(0, 0) → p_out_ga(0, 0)
PLUS_IN_GGA(X, Y) → U16_GGA(Y, p_in_ga(X))
U16_GGA(Y, p_out_ga(P)) → PLUS_IN_GGA(P, Y)
p_in_ga(s(X)) → p_out_ga(X)
p_in_ga(0) → p_out_ga(0)
p_in_ga(x0)
Used ordering: POLO with Polynomial interpretation [POLO]:
p_in_ga(s(X)) → p_out_ga(X)
POL(0) = 0
POL(PLUS_IN_GGA(x1, x2)) = x1 + x2
POL(U16_GGA(x1, x2)) = x1 + x2
POL(p_in_ga(x1)) = x1
POL(p_out_ga(x1)) = 2·x1
POL(s(x1)) = 2 + 2·x1
PLUS_IN_GGA(X, Y) → U16_GGA(Y, p_in_ga(X))
U16_GGA(Y, p_out_ga(P)) → PLUS_IN_GGA(P, Y)
p_in_ga(0) → p_out_ga(0)
p_in_ga(x0)
PLUS_IN_GGA(0, y1) → U16_GGA(y1, p_out_ga(0))
U16_GGA(Y, p_out_ga(P)) → PLUS_IN_GGA(P, Y)
PLUS_IN_GGA(0, y1) → U16_GGA(y1, p_out_ga(0))
p_in_ga(0) → p_out_ga(0)
p_in_ga(x0)
U16_GGA(Y, p_out_ga(P)) → PLUS_IN_GGA(P, Y)
PLUS_IN_GGA(0, y1) → U16_GGA(y1, p_out_ga(0))
p_in_ga(x0)
p_in_ga(x0)
U16_GGA(Y, p_out_ga(P)) → PLUS_IN_GGA(P, Y)
PLUS_IN_GGA(0, y1) → U16_GGA(y1, p_out_ga(0))
U16_GGA(z0, p_out_ga(0)) → PLUS_IN_GGA(0, z0)
PLUS_IN_GGA(0, y1) → U16_GGA(y1, p_out_ga(0))
U16_GGA(z0, p_out_ga(0)) → PLUS_IN_GGA(0, z0)
TIMES_IN_GGA(X, Y, Z) → U12_GGA(X, Y, Z, p_in_ga(X, P))
U12_GGA(X, Y, Z, p_out_ga(X, P)) → TIMES_IN_GGA(P, Y, U)
convert_in_gga([], X1, Z) → U1_gga(X1, Z, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U1_gga(X1, Z, eq_out_ag(Z, 0)) → convert_out_gga([], X1, Z)
convert_in_gga(X, Y, Z) → U2_gga(X, Y, Z, head_in_gg(X, 0))
head_in_gg([], X2) → head_out_gg([], X2)
head_in_gg(.(H, X3), H) → head_out_gg(.(H, X3), H)
U2_gga(X, Y, Z, head_out_gg(X, 0)) → U3_gga(X, Y, Z, tail_in_ga(X, T))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X4, Xs), Xs) → tail_out_ga(.(X4, Xs), Xs)
U3_gga(X, Y, Z, tail_out_ga(X, T)) → U4_gga(X, Y, Z, T, convert_in_gga(T, Y, U))
convert_in_gga(X, Y, Z) → U6_gga(X, Y, Z, head_in_ga(X, H))
head_in_ga([], X2) → head_out_ga([], X2)
head_in_ga(.(H, X3), H) → head_out_ga(.(H, X3), H)
U6_gga(X, Y, Z, head_out_ga(X, H)) → U7_gga(X, Y, Z, H, p_in_aa(H, P))
p_in_aa(s(X), X) → p_out_aa(s(X), X)
p_in_aa(0, 0) → p_out_aa(0, 0)
U7_gga(X, Y, Z, H, p_out_aa(H, P)) → U8_gga(X, Y, Z, H, P, tail_in_ga(X, T))
U8_gga(X, Y, Z, H, P, tail_out_ga(X, T)) → U9_gga(X, Y, Z, H, P, T, convert_in_aga(.(P, T), Y, U))
convert_in_aga([], X1, Z) → U1_aga(X1, Z, eq_in_ag(Z, 0))
U1_aga(X1, Z, eq_out_ag(Z, 0)) → convert_out_aga([], X1, Z)
convert_in_aga(X, Y, Z) → U2_aga(X, Y, Z, head_in_ag(X, 0))
head_in_ag([], X2) → head_out_ag([], X2)
head_in_ag(.(H, X3), H) → head_out_ag(.(H, X3), H)
U2_aga(X, Y, Z, head_out_ag(X, 0)) → U3_aga(X, Y, Z, tail_in_aa(X, T))
tail_in_aa([], []) → tail_out_aa([], [])
tail_in_aa(.(X4, Xs), Xs) → tail_out_aa(.(X4, Xs), Xs)
U3_aga(X, Y, Z, tail_out_aa(X, T)) → U4_aga(X, Y, Z, T, convert_in_aga(T, Y, U))
convert_in_aga(X, Y, Z) → U6_aga(X, Y, Z, head_in_aa(X, H))
head_in_aa([], X2) → head_out_aa([], X2)
head_in_aa(.(H, X3), H) → head_out_aa(.(H, X3), H)
U6_aga(X, Y, Z, head_out_aa(X, H)) → U7_aga(X, Y, Z, H, p_in_aa(H, P))
U7_aga(X, Y, Z, H, p_out_aa(H, P)) → U8_aga(X, Y, Z, H, P, tail_in_aa(X, T))
U8_aga(X, Y, Z, H, P, tail_out_aa(X, T)) → U9_aga(X, Y, Z, H, P, T, convert_in_aga(.(P, T), Y, U))
U9_aga(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → U10_aga(X, Y, Z, p_in_ag(Z, U))
p_in_ag(s(X), X) → p_out_ag(s(X), X)
p_in_ag(0, 0) → p_out_ag(0, 0)
U10_aga(X, Y, Z, p_out_ag(Z, U)) → convert_out_aga(X, Y, Z)
U4_aga(X, Y, Z, T, convert_out_aga(T, Y, U)) → U5_aga(X, Y, Z, times_in_gga(U, Y, Z))
times_in_gga(0, Y, Z) → U11_gga(Y, Z, eq_in_ag(Z, 0))
U11_gga(Y, Z, eq_out_ag(Z, 0)) → times_out_gga(0, Y, Z)
times_in_gga(X, Y, Z) → U12_gga(X, Y, Z, p_in_ga(X, P))
p_in_ga(s(X), X) → p_out_ga(s(X), X)
p_in_ga(0, 0) → p_out_ga(0, 0)
U12_gga(X, Y, Z, p_out_ga(X, P)) → U13_gga(X, Y, Z, P, times_in_gga(P, Y, U))
U13_gga(X, Y, Z, P, times_out_gga(P, Y, U)) → U14_gga(X, Y, Z, plus_in_gga(Y, U, Z))
plus_in_gga(0, Y, Z) → U15_gga(Y, Z, eq_in_ga(Y, Z))
eq_in_ga(X, X) → eq_out_ga(X, X)
U15_gga(Y, Z, eq_out_ga(Y, Z)) → plus_out_gga(0, Y, Z)
plus_in_gga(X, Y, Z) → U16_gga(X, Y, Z, p_in_ga(X, P))
U16_gga(X, Y, Z, p_out_ga(X, P)) → U17_gga(X, Y, Z, P, plus_in_gga(P, Y, U))
U17_gga(X, Y, Z, P, plus_out_gga(P, Y, U)) → U18_gga(X, Y, Z, p_in_ag(Z, U))
U18_gga(X, Y, Z, p_out_ag(Z, U)) → plus_out_gga(X, Y, Z)
U14_gga(X, Y, Z, plus_out_gga(Y, U, Z)) → times_out_gga(X, Y, Z)
U5_aga(X, Y, Z, times_out_gga(U, Y, Z)) → convert_out_aga(X, Y, Z)
U9_gga(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → U10_gga(X, Y, Z, p_in_ag(Z, U))
U10_gga(X, Y, Z, p_out_ag(Z, U)) → convert_out_gga(X, Y, Z)
U4_gga(X, Y, Z, T, convert_out_gga(T, Y, U)) → U5_gga(X, Y, Z, times_in_gga(U, Y, Z))
U5_gga(X, Y, Z, times_out_gga(U, Y, Z)) → convert_out_gga(X, Y, Z)
TIMES_IN_GGA(X, Y, Z) → U12_GGA(X, Y, Z, p_in_ga(X, P))
U12_GGA(X, Y, Z, p_out_ga(X, P)) → TIMES_IN_GGA(P, Y, U)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
p_in_ga(0, 0) → p_out_ga(0, 0)
TIMES_IN_GGA(X, Y) → U12_GGA(Y, p_in_ga(X))
U12_GGA(Y, p_out_ga(P)) → TIMES_IN_GGA(P, Y)
p_in_ga(s(X)) → p_out_ga(X)
p_in_ga(0) → p_out_ga(0)
p_in_ga(x0)
Used ordering: POLO with Polynomial interpretation [POLO]:
p_in_ga(s(X)) → p_out_ga(X)
POL(0) = 0
POL(TIMES_IN_GGA(x1, x2)) = x1 + x2
POL(U12_GGA(x1, x2)) = x1 + x2
POL(p_in_ga(x1)) = x1
POL(p_out_ga(x1)) = 2·x1
POL(s(x1)) = 2 + 2·x1
TIMES_IN_GGA(X, Y) → U12_GGA(Y, p_in_ga(X))
U12_GGA(Y, p_out_ga(P)) → TIMES_IN_GGA(P, Y)
p_in_ga(0) → p_out_ga(0)
p_in_ga(x0)
TIMES_IN_GGA(0, y1) → U12_GGA(y1, p_out_ga(0))
U12_GGA(Y, p_out_ga(P)) → TIMES_IN_GGA(P, Y)
TIMES_IN_GGA(0, y1) → U12_GGA(y1, p_out_ga(0))
p_in_ga(0) → p_out_ga(0)
p_in_ga(x0)
U12_GGA(Y, p_out_ga(P)) → TIMES_IN_GGA(P, Y)
TIMES_IN_GGA(0, y1) → U12_GGA(y1, p_out_ga(0))
p_in_ga(x0)
p_in_ga(x0)
U12_GGA(Y, p_out_ga(P)) → TIMES_IN_GGA(P, Y)
TIMES_IN_GGA(0, y1) → U12_GGA(y1, p_out_ga(0))
U12_GGA(z0, p_out_ga(0)) → TIMES_IN_GGA(0, z0)
TIMES_IN_GGA(0, y1) → U12_GGA(y1, p_out_ga(0))
U12_GGA(z0, p_out_ga(0)) → TIMES_IN_GGA(0, z0)
CONVERT_IN_AGA(X, Y, Z) → U2_AGA(X, Y, Z, head_in_ag(X, 0))
U2_AGA(X, Y, Z, head_out_ag(X, 0)) → U3_AGA(X, Y, Z, tail_in_aa(X, T))
U3_AGA(X, Y, Z, tail_out_aa(X, T)) → CONVERT_IN_AGA(T, Y, U)
CONVERT_IN_AGA(X, Y, Z) → U6_AGA(X, Y, Z, head_in_aa(X, H))
U6_AGA(X, Y, Z, head_out_aa(X, H)) → U7_AGA(X, Y, Z, H, p_in_aa(H, P))
U7_AGA(X, Y, Z, H, p_out_aa(H, P)) → U8_AGA(X, Y, Z, H, P, tail_in_aa(X, T))
U8_AGA(X, Y, Z, H, P, tail_out_aa(X, T)) → CONVERT_IN_AGA(.(P, T), Y, U)
convert_in_gga([], X1, Z) → U1_gga(X1, Z, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U1_gga(X1, Z, eq_out_ag(Z, 0)) → convert_out_gga([], X1, Z)
convert_in_gga(X, Y, Z) → U2_gga(X, Y, Z, head_in_gg(X, 0))
head_in_gg([], X2) → head_out_gg([], X2)
head_in_gg(.(H, X3), H) → head_out_gg(.(H, X3), H)
U2_gga(X, Y, Z, head_out_gg(X, 0)) → U3_gga(X, Y, Z, tail_in_ga(X, T))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X4, Xs), Xs) → tail_out_ga(.(X4, Xs), Xs)
U3_gga(X, Y, Z, tail_out_ga(X, T)) → U4_gga(X, Y, Z, T, convert_in_gga(T, Y, U))
convert_in_gga(X, Y, Z) → U6_gga(X, Y, Z, head_in_ga(X, H))
head_in_ga([], X2) → head_out_ga([], X2)
head_in_ga(.(H, X3), H) → head_out_ga(.(H, X3), H)
U6_gga(X, Y, Z, head_out_ga(X, H)) → U7_gga(X, Y, Z, H, p_in_aa(H, P))
p_in_aa(s(X), X) → p_out_aa(s(X), X)
p_in_aa(0, 0) → p_out_aa(0, 0)
U7_gga(X, Y, Z, H, p_out_aa(H, P)) → U8_gga(X, Y, Z, H, P, tail_in_ga(X, T))
U8_gga(X, Y, Z, H, P, tail_out_ga(X, T)) → U9_gga(X, Y, Z, H, P, T, convert_in_aga(.(P, T), Y, U))
convert_in_aga([], X1, Z) → U1_aga(X1, Z, eq_in_ag(Z, 0))
U1_aga(X1, Z, eq_out_ag(Z, 0)) → convert_out_aga([], X1, Z)
convert_in_aga(X, Y, Z) → U2_aga(X, Y, Z, head_in_ag(X, 0))
head_in_ag([], X2) → head_out_ag([], X2)
head_in_ag(.(H, X3), H) → head_out_ag(.(H, X3), H)
U2_aga(X, Y, Z, head_out_ag(X, 0)) → U3_aga(X, Y, Z, tail_in_aa(X, T))
tail_in_aa([], []) → tail_out_aa([], [])
tail_in_aa(.(X4, Xs), Xs) → tail_out_aa(.(X4, Xs), Xs)
U3_aga(X, Y, Z, tail_out_aa(X, T)) → U4_aga(X, Y, Z, T, convert_in_aga(T, Y, U))
convert_in_aga(X, Y, Z) → U6_aga(X, Y, Z, head_in_aa(X, H))
head_in_aa([], X2) → head_out_aa([], X2)
head_in_aa(.(H, X3), H) → head_out_aa(.(H, X3), H)
U6_aga(X, Y, Z, head_out_aa(X, H)) → U7_aga(X, Y, Z, H, p_in_aa(H, P))
U7_aga(X, Y, Z, H, p_out_aa(H, P)) → U8_aga(X, Y, Z, H, P, tail_in_aa(X, T))
U8_aga(X, Y, Z, H, P, tail_out_aa(X, T)) → U9_aga(X, Y, Z, H, P, T, convert_in_aga(.(P, T), Y, U))
U9_aga(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → U10_aga(X, Y, Z, p_in_ag(Z, U))
p_in_ag(s(X), X) → p_out_ag(s(X), X)
p_in_ag(0, 0) → p_out_ag(0, 0)
U10_aga(X, Y, Z, p_out_ag(Z, U)) → convert_out_aga(X, Y, Z)
U4_aga(X, Y, Z, T, convert_out_aga(T, Y, U)) → U5_aga(X, Y, Z, times_in_gga(U, Y, Z))
times_in_gga(0, Y, Z) → U11_gga(Y, Z, eq_in_ag(Z, 0))
U11_gga(Y, Z, eq_out_ag(Z, 0)) → times_out_gga(0, Y, Z)
times_in_gga(X, Y, Z) → U12_gga(X, Y, Z, p_in_ga(X, P))
p_in_ga(s(X), X) → p_out_ga(s(X), X)
p_in_ga(0, 0) → p_out_ga(0, 0)
U12_gga(X, Y, Z, p_out_ga(X, P)) → U13_gga(X, Y, Z, P, times_in_gga(P, Y, U))
U13_gga(X, Y, Z, P, times_out_gga(P, Y, U)) → U14_gga(X, Y, Z, plus_in_gga(Y, U, Z))
plus_in_gga(0, Y, Z) → U15_gga(Y, Z, eq_in_ga(Y, Z))
eq_in_ga(X, X) → eq_out_ga(X, X)
U15_gga(Y, Z, eq_out_ga(Y, Z)) → plus_out_gga(0, Y, Z)
plus_in_gga(X, Y, Z) → U16_gga(X, Y, Z, p_in_ga(X, P))
U16_gga(X, Y, Z, p_out_ga(X, P)) → U17_gga(X, Y, Z, P, plus_in_gga(P, Y, U))
U17_gga(X, Y, Z, P, plus_out_gga(P, Y, U)) → U18_gga(X, Y, Z, p_in_ag(Z, U))
U18_gga(X, Y, Z, p_out_ag(Z, U)) → plus_out_gga(X, Y, Z)
U14_gga(X, Y, Z, plus_out_gga(Y, U, Z)) → times_out_gga(X, Y, Z)
U5_aga(X, Y, Z, times_out_gga(U, Y, Z)) → convert_out_aga(X, Y, Z)
U9_gga(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → U10_gga(X, Y, Z, p_in_ag(Z, U))
U10_gga(X, Y, Z, p_out_ag(Z, U)) → convert_out_gga(X, Y, Z)
U4_gga(X, Y, Z, T, convert_out_gga(T, Y, U)) → U5_gga(X, Y, Z, times_in_gga(U, Y, Z))
U5_gga(X, Y, Z, times_out_gga(U, Y, Z)) → convert_out_gga(X, Y, Z)
CONVERT_IN_AGA(X, Y, Z) → U2_AGA(X, Y, Z, head_in_ag(X, 0))
U2_AGA(X, Y, Z, head_out_ag(X, 0)) → U3_AGA(X, Y, Z, tail_in_aa(X, T))
U3_AGA(X, Y, Z, tail_out_aa(X, T)) → CONVERT_IN_AGA(T, Y, U)
CONVERT_IN_AGA(X, Y, Z) → U6_AGA(X, Y, Z, head_in_aa(X, H))
U6_AGA(X, Y, Z, head_out_aa(X, H)) → U7_AGA(X, Y, Z, H, p_in_aa(H, P))
U7_AGA(X, Y, Z, H, p_out_aa(H, P)) → U8_AGA(X, Y, Z, H, P, tail_in_aa(X, T))
U8_AGA(X, Y, Z, H, P, tail_out_aa(X, T)) → CONVERT_IN_AGA(.(P, T), Y, U)
head_in_ag([], X2) → head_out_ag([], X2)
head_in_ag(.(H, X3), H) → head_out_ag(.(H, X3), H)
tail_in_aa([], []) → tail_out_aa([], [])
tail_in_aa(.(X4, Xs), Xs) → tail_out_aa(.(X4, Xs), Xs)
head_in_aa([], X2) → head_out_aa([], X2)
head_in_aa(.(H, X3), H) → head_out_aa(.(H, X3), H)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
p_in_aa(0, 0) → p_out_aa(0, 0)
CONVERT_IN_AGA(Y) → U2_AGA(Y, head_in_ag(0))
U2_AGA(Y, head_out_ag) → U3_AGA(Y, tail_in_aa)
U3_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
CONVERT_IN_AGA(Y) → U6_AGA(Y, head_in_aa)
U6_AGA(Y, head_out_aa) → U7_AGA(Y, p_in_aa)
U7_AGA(Y, p_out_aa) → U8_AGA(Y, tail_in_aa)
U8_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
head_in_ag(X2) → head_out_ag
tail_in_aa → tail_out_aa
head_in_aa → head_out_aa
p_in_aa → p_out_aa
head_in_ag(x0)
tail_in_aa
head_in_aa
p_in_aa
CONVERT_IN_AGA(Y) → U2_AGA(Y, head_out_ag)
U2_AGA(Y, head_out_ag) → U3_AGA(Y, tail_in_aa)
U3_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
CONVERT_IN_AGA(Y) → U6_AGA(Y, head_in_aa)
U6_AGA(Y, head_out_aa) → U7_AGA(Y, p_in_aa)
U7_AGA(Y, p_out_aa) → U8_AGA(Y, tail_in_aa)
U8_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
CONVERT_IN_AGA(Y) → U2_AGA(Y, head_out_ag)
head_in_ag(X2) → head_out_ag
tail_in_aa → tail_out_aa
head_in_aa → head_out_aa
p_in_aa → p_out_aa
head_in_ag(x0)
tail_in_aa
head_in_aa
p_in_aa
U2_AGA(Y, head_out_ag) → U3_AGA(Y, tail_in_aa)
U3_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
CONVERT_IN_AGA(Y) → U6_AGA(Y, head_in_aa)
U6_AGA(Y, head_out_aa) → U7_AGA(Y, p_in_aa)
U7_AGA(Y, p_out_aa) → U8_AGA(Y, tail_in_aa)
U8_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
CONVERT_IN_AGA(Y) → U2_AGA(Y, head_out_ag)
tail_in_aa → tail_out_aa
p_in_aa → p_out_aa
head_in_aa → head_out_aa
head_in_ag(x0)
tail_in_aa
head_in_aa
p_in_aa
head_in_ag(x0)
U2_AGA(Y, head_out_ag) → U3_AGA(Y, tail_in_aa)
U3_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
CONVERT_IN_AGA(Y) → U6_AGA(Y, head_in_aa)
U6_AGA(Y, head_out_aa) → U7_AGA(Y, p_in_aa)
U7_AGA(Y, p_out_aa) → U8_AGA(Y, tail_in_aa)
U8_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
CONVERT_IN_AGA(Y) → U2_AGA(Y, head_out_ag)
tail_in_aa → tail_out_aa
p_in_aa → p_out_aa
head_in_aa → head_out_aa
tail_in_aa
head_in_aa
p_in_aa
U2_AGA(Y, head_out_ag) → U3_AGA(Y, tail_out_aa)
U3_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
CONVERT_IN_AGA(Y) → U6_AGA(Y, head_in_aa)
U6_AGA(Y, head_out_aa) → U7_AGA(Y, p_in_aa)
U7_AGA(Y, p_out_aa) → U8_AGA(Y, tail_in_aa)
U8_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
CONVERT_IN_AGA(Y) → U2_AGA(Y, head_out_ag)
U2_AGA(Y, head_out_ag) → U3_AGA(Y, tail_out_aa)
tail_in_aa → tail_out_aa
p_in_aa → p_out_aa
head_in_aa → head_out_aa
tail_in_aa
head_in_aa
p_in_aa
CONVERT_IN_AGA(Y) → U6_AGA(Y, head_out_aa)
U3_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
U6_AGA(Y, head_out_aa) → U7_AGA(Y, p_in_aa)
U7_AGA(Y, p_out_aa) → U8_AGA(Y, tail_in_aa)
U8_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
CONVERT_IN_AGA(Y) → U2_AGA(Y, head_out_ag)
U2_AGA(Y, head_out_ag) → U3_AGA(Y, tail_out_aa)
CONVERT_IN_AGA(Y) → U6_AGA(Y, head_out_aa)
tail_in_aa → tail_out_aa
p_in_aa → p_out_aa
head_in_aa → head_out_aa
tail_in_aa
head_in_aa
p_in_aa
U3_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
U6_AGA(Y, head_out_aa) → U7_AGA(Y, p_in_aa)
U7_AGA(Y, p_out_aa) → U8_AGA(Y, tail_in_aa)
U8_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
CONVERT_IN_AGA(Y) → U2_AGA(Y, head_out_ag)
U2_AGA(Y, head_out_ag) → U3_AGA(Y, tail_out_aa)
CONVERT_IN_AGA(Y) → U6_AGA(Y, head_out_aa)
tail_in_aa → tail_out_aa
p_in_aa → p_out_aa
tail_in_aa
head_in_aa
p_in_aa
head_in_aa
U3_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
U6_AGA(Y, head_out_aa) → U7_AGA(Y, p_in_aa)
U7_AGA(Y, p_out_aa) → U8_AGA(Y, tail_in_aa)
U8_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
CONVERT_IN_AGA(Y) → U2_AGA(Y, head_out_ag)
U2_AGA(Y, head_out_ag) → U3_AGA(Y, tail_out_aa)
CONVERT_IN_AGA(Y) → U6_AGA(Y, head_out_aa)
tail_in_aa → tail_out_aa
p_in_aa → p_out_aa
tail_in_aa
p_in_aa
U6_AGA(Y, head_out_aa) → U7_AGA(Y, p_out_aa)
U3_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
U7_AGA(Y, p_out_aa) → U8_AGA(Y, tail_in_aa)
U8_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
CONVERT_IN_AGA(Y) → U2_AGA(Y, head_out_ag)
U2_AGA(Y, head_out_ag) → U3_AGA(Y, tail_out_aa)
CONVERT_IN_AGA(Y) → U6_AGA(Y, head_out_aa)
U6_AGA(Y, head_out_aa) → U7_AGA(Y, p_out_aa)
tail_in_aa → tail_out_aa
p_in_aa → p_out_aa
tail_in_aa
p_in_aa
U3_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
U7_AGA(Y, p_out_aa) → U8_AGA(Y, tail_in_aa)
U8_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
CONVERT_IN_AGA(Y) → U2_AGA(Y, head_out_ag)
U2_AGA(Y, head_out_ag) → U3_AGA(Y, tail_out_aa)
CONVERT_IN_AGA(Y) → U6_AGA(Y, head_out_aa)
U6_AGA(Y, head_out_aa) → U7_AGA(Y, p_out_aa)
tail_in_aa → tail_out_aa
tail_in_aa
p_in_aa
p_in_aa
U3_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
U7_AGA(Y, p_out_aa) → U8_AGA(Y, tail_in_aa)
U8_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
CONVERT_IN_AGA(Y) → U2_AGA(Y, head_out_ag)
U2_AGA(Y, head_out_ag) → U3_AGA(Y, tail_out_aa)
CONVERT_IN_AGA(Y) → U6_AGA(Y, head_out_aa)
U6_AGA(Y, head_out_aa) → U7_AGA(Y, p_out_aa)
tail_in_aa → tail_out_aa
tail_in_aa
U7_AGA(Y, p_out_aa) → U8_AGA(Y, tail_out_aa)
U3_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
U8_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
CONVERT_IN_AGA(Y) → U2_AGA(Y, head_out_ag)
U2_AGA(Y, head_out_ag) → U3_AGA(Y, tail_out_aa)
CONVERT_IN_AGA(Y) → U6_AGA(Y, head_out_aa)
U6_AGA(Y, head_out_aa) → U7_AGA(Y, p_out_aa)
U7_AGA(Y, p_out_aa) → U8_AGA(Y, tail_out_aa)
tail_in_aa → tail_out_aa
tail_in_aa
U3_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
U8_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
CONVERT_IN_AGA(Y) → U2_AGA(Y, head_out_ag)
U2_AGA(Y, head_out_ag) → U3_AGA(Y, tail_out_aa)
CONVERT_IN_AGA(Y) → U6_AGA(Y, head_out_aa)
U6_AGA(Y, head_out_aa) → U7_AGA(Y, p_out_aa)
U7_AGA(Y, p_out_aa) → U8_AGA(Y, tail_out_aa)
tail_in_aa
tail_in_aa
U3_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
U8_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
CONVERT_IN_AGA(Y) → U2_AGA(Y, head_out_ag)
U2_AGA(Y, head_out_ag) → U3_AGA(Y, tail_out_aa)
CONVERT_IN_AGA(Y) → U6_AGA(Y, head_out_aa)
U6_AGA(Y, head_out_aa) → U7_AGA(Y, p_out_aa)
U7_AGA(Y, p_out_aa) → U8_AGA(Y, tail_out_aa)
CONVERT_IN_GGA(X, Y, Z) → U2_GGA(X, Y, Z, head_in_gg(X, 0))
U2_GGA(X, Y, Z, head_out_gg(X, 0)) → U3_GGA(X, Y, Z, tail_in_ga(X, T))
U3_GGA(X, Y, Z, tail_out_ga(X, T)) → CONVERT_IN_GGA(T, Y, U)
convert_in_gga([], X1, Z) → U1_gga(X1, Z, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U1_gga(X1, Z, eq_out_ag(Z, 0)) → convert_out_gga([], X1, Z)
convert_in_gga(X, Y, Z) → U2_gga(X, Y, Z, head_in_gg(X, 0))
head_in_gg([], X2) → head_out_gg([], X2)
head_in_gg(.(H, X3), H) → head_out_gg(.(H, X3), H)
U2_gga(X, Y, Z, head_out_gg(X, 0)) → U3_gga(X, Y, Z, tail_in_ga(X, T))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X4, Xs), Xs) → tail_out_ga(.(X4, Xs), Xs)
U3_gga(X, Y, Z, tail_out_ga(X, T)) → U4_gga(X, Y, Z, T, convert_in_gga(T, Y, U))
convert_in_gga(X, Y, Z) → U6_gga(X, Y, Z, head_in_ga(X, H))
head_in_ga([], X2) → head_out_ga([], X2)
head_in_ga(.(H, X3), H) → head_out_ga(.(H, X3), H)
U6_gga(X, Y, Z, head_out_ga(X, H)) → U7_gga(X, Y, Z, H, p_in_aa(H, P))
p_in_aa(s(X), X) → p_out_aa(s(X), X)
p_in_aa(0, 0) → p_out_aa(0, 0)
U7_gga(X, Y, Z, H, p_out_aa(H, P)) → U8_gga(X, Y, Z, H, P, tail_in_ga(X, T))
U8_gga(X, Y, Z, H, P, tail_out_ga(X, T)) → U9_gga(X, Y, Z, H, P, T, convert_in_aga(.(P, T), Y, U))
convert_in_aga([], X1, Z) → U1_aga(X1, Z, eq_in_ag(Z, 0))
U1_aga(X1, Z, eq_out_ag(Z, 0)) → convert_out_aga([], X1, Z)
convert_in_aga(X, Y, Z) → U2_aga(X, Y, Z, head_in_ag(X, 0))
head_in_ag([], X2) → head_out_ag([], X2)
head_in_ag(.(H, X3), H) → head_out_ag(.(H, X3), H)
U2_aga(X, Y, Z, head_out_ag(X, 0)) → U3_aga(X, Y, Z, tail_in_aa(X, T))
tail_in_aa([], []) → tail_out_aa([], [])
tail_in_aa(.(X4, Xs), Xs) → tail_out_aa(.(X4, Xs), Xs)
U3_aga(X, Y, Z, tail_out_aa(X, T)) → U4_aga(X, Y, Z, T, convert_in_aga(T, Y, U))
convert_in_aga(X, Y, Z) → U6_aga(X, Y, Z, head_in_aa(X, H))
head_in_aa([], X2) → head_out_aa([], X2)
head_in_aa(.(H, X3), H) → head_out_aa(.(H, X3), H)
U6_aga(X, Y, Z, head_out_aa(X, H)) → U7_aga(X, Y, Z, H, p_in_aa(H, P))
U7_aga(X, Y, Z, H, p_out_aa(H, P)) → U8_aga(X, Y, Z, H, P, tail_in_aa(X, T))
U8_aga(X, Y, Z, H, P, tail_out_aa(X, T)) → U9_aga(X, Y, Z, H, P, T, convert_in_aga(.(P, T), Y, U))
U9_aga(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → U10_aga(X, Y, Z, p_in_ag(Z, U))
p_in_ag(s(X), X) → p_out_ag(s(X), X)
p_in_ag(0, 0) → p_out_ag(0, 0)
U10_aga(X, Y, Z, p_out_ag(Z, U)) → convert_out_aga(X, Y, Z)
U4_aga(X, Y, Z, T, convert_out_aga(T, Y, U)) → U5_aga(X, Y, Z, times_in_gga(U, Y, Z))
times_in_gga(0, Y, Z) → U11_gga(Y, Z, eq_in_ag(Z, 0))
U11_gga(Y, Z, eq_out_ag(Z, 0)) → times_out_gga(0, Y, Z)
times_in_gga(X, Y, Z) → U12_gga(X, Y, Z, p_in_ga(X, P))
p_in_ga(s(X), X) → p_out_ga(s(X), X)
p_in_ga(0, 0) → p_out_ga(0, 0)
U12_gga(X, Y, Z, p_out_ga(X, P)) → U13_gga(X, Y, Z, P, times_in_gga(P, Y, U))
U13_gga(X, Y, Z, P, times_out_gga(P, Y, U)) → U14_gga(X, Y, Z, plus_in_gga(Y, U, Z))
plus_in_gga(0, Y, Z) → U15_gga(Y, Z, eq_in_ga(Y, Z))
eq_in_ga(X, X) → eq_out_ga(X, X)
U15_gga(Y, Z, eq_out_ga(Y, Z)) → plus_out_gga(0, Y, Z)
plus_in_gga(X, Y, Z) → U16_gga(X, Y, Z, p_in_ga(X, P))
U16_gga(X, Y, Z, p_out_ga(X, P)) → U17_gga(X, Y, Z, P, plus_in_gga(P, Y, U))
U17_gga(X, Y, Z, P, plus_out_gga(P, Y, U)) → U18_gga(X, Y, Z, p_in_ag(Z, U))
U18_gga(X, Y, Z, p_out_ag(Z, U)) → plus_out_gga(X, Y, Z)
U14_gga(X, Y, Z, plus_out_gga(Y, U, Z)) → times_out_gga(X, Y, Z)
U5_aga(X, Y, Z, times_out_gga(U, Y, Z)) → convert_out_aga(X, Y, Z)
U9_gga(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → U10_gga(X, Y, Z, p_in_ag(Z, U))
U10_gga(X, Y, Z, p_out_ag(Z, U)) → convert_out_gga(X, Y, Z)
U4_gga(X, Y, Z, T, convert_out_gga(T, Y, U)) → U5_gga(X, Y, Z, times_in_gga(U, Y, Z))
U5_gga(X, Y, Z, times_out_gga(U, Y, Z)) → convert_out_gga(X, Y, Z)
CONVERT_IN_GGA(X, Y, Z) → U2_GGA(X, Y, Z, head_in_gg(X, 0))
U2_GGA(X, Y, Z, head_out_gg(X, 0)) → U3_GGA(X, Y, Z, tail_in_ga(X, T))
U3_GGA(X, Y, Z, tail_out_ga(X, T)) → CONVERT_IN_GGA(T, Y, U)
head_in_gg([], X2) → head_out_gg([], X2)
head_in_gg(.(H, X3), H) → head_out_gg(.(H, X3), H)
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X4, Xs), Xs) → tail_out_ga(.(X4, Xs), Xs)
CONVERT_IN_GGA(X, Y) → U2_GGA(X, Y, head_in_gg(X, 0))
U2_GGA(X, Y, head_out_gg) → U3_GGA(Y, tail_in_ga(X))
U3_GGA(Y, tail_out_ga(T)) → CONVERT_IN_GGA(T, Y)
head_in_gg([], X2) → head_out_gg
head_in_gg(.(H, X3), H) → head_out_gg
tail_in_ga([]) → tail_out_ga([])
tail_in_ga(.(X4, Xs)) → tail_out_ga(Xs)
head_in_gg(x0, x1)
tail_in_ga(x0)
Used ordering: POLO with Polynomial interpretation [POLO]:
tail_in_ga(.(X4, Xs)) → tail_out_ga(Xs)
head_in_gg(.(H, X3), H) → head_out_gg
POL(.(x1, x2)) = x1 + 2·x2
POL(0) = 0
POL(CONVERT_IN_GGA(x1, x2)) = 2·x1 + x2
POL(U2_GGA(x1, x2, x3)) = x1 + x2 + x3
POL(U3_GGA(x1, x2)) = x1 + x2
POL([]) = 0
POL(head_in_gg(x1, x2)) = x1 + 2·x2
POL(head_out_gg) = 0
POL(tail_in_ga(x1)) = x1
POL(tail_out_ga(x1)) = 2·x1
CONVERT_IN_GGA(X, Y) → U2_GGA(X, Y, head_in_gg(X, 0))
U2_GGA(X, Y, head_out_gg) → U3_GGA(Y, tail_in_ga(X))
U3_GGA(Y, tail_out_ga(T)) → CONVERT_IN_GGA(T, Y)
tail_in_ga([]) → tail_out_ga([])
head_in_gg([], X2) → head_out_gg
head_in_gg(x0, x1)
tail_in_ga(x0)
CONVERT_IN_GGA([], y1) → U2_GGA([], y1, head_out_gg)
U2_GGA(X, Y, head_out_gg) → U3_GGA(Y, tail_in_ga(X))
U3_GGA(Y, tail_out_ga(T)) → CONVERT_IN_GGA(T, Y)
CONVERT_IN_GGA([], y1) → U2_GGA([], y1, head_out_gg)
tail_in_ga([]) → tail_out_ga([])
head_in_gg([], X2) → head_out_gg
head_in_gg(x0, x1)
tail_in_ga(x0)
U2_GGA(X, Y, head_out_gg) → U3_GGA(Y, tail_in_ga(X))
U3_GGA(Y, tail_out_ga(T)) → CONVERT_IN_GGA(T, Y)
CONVERT_IN_GGA([], y1) → U2_GGA([], y1, head_out_gg)
tail_in_ga([]) → tail_out_ga([])
head_in_gg(x0, x1)
tail_in_ga(x0)
head_in_gg(x0, x1)
U2_GGA(X, Y, head_out_gg) → U3_GGA(Y, tail_in_ga(X))
U3_GGA(Y, tail_out_ga(T)) → CONVERT_IN_GGA(T, Y)
CONVERT_IN_GGA([], y1) → U2_GGA([], y1, head_out_gg)
tail_in_ga([]) → tail_out_ga([])
tail_in_ga(x0)
U2_GGA([], y1, head_out_gg) → U3_GGA(y1, tail_out_ga([]))
U3_GGA(Y, tail_out_ga(T)) → CONVERT_IN_GGA(T, Y)
CONVERT_IN_GGA([], y1) → U2_GGA([], y1, head_out_gg)
U2_GGA([], y1, head_out_gg) → U3_GGA(y1, tail_out_ga([]))
tail_in_ga([]) → tail_out_ga([])
tail_in_ga(x0)
U3_GGA(Y, tail_out_ga(T)) → CONVERT_IN_GGA(T, Y)
CONVERT_IN_GGA([], y1) → U2_GGA([], y1, head_out_gg)
U2_GGA([], y1, head_out_gg) → U3_GGA(y1, tail_out_ga([]))
tail_in_ga(x0)
tail_in_ga(x0)
U3_GGA(Y, tail_out_ga(T)) → CONVERT_IN_GGA(T, Y)
CONVERT_IN_GGA([], y1) → U2_GGA([], y1, head_out_gg)
U2_GGA([], y1, head_out_gg) → U3_GGA(y1, tail_out_ga([]))
U3_GGA(z0, tail_out_ga([])) → CONVERT_IN_GGA([], z0)
CONVERT_IN_GGA([], y1) → U2_GGA([], y1, head_out_gg)
U2_GGA([], y1, head_out_gg) → U3_GGA(y1, tail_out_ga([]))
U3_GGA(z0, tail_out_ga([])) → CONVERT_IN_GGA([], z0)
convert_in_gga([], X1, Z) → U1_gga(X1, Z, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U1_gga(X1, Z, eq_out_ag(Z, 0)) → convert_out_gga([], X1, Z)
convert_in_gga(X, Y, Z) → U2_gga(X, Y, Z, head_in_gg(X, 0))
head_in_gg([], X2) → head_out_gg([], X2)
head_in_gg(.(H, X3), H) → head_out_gg(.(H, X3), H)
U2_gga(X, Y, Z, head_out_gg(X, 0)) → U3_gga(X, Y, Z, tail_in_ga(X, T))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X4, Xs), Xs) → tail_out_ga(.(X4, Xs), Xs)
U3_gga(X, Y, Z, tail_out_ga(X, T)) → U4_gga(X, Y, Z, T, convert_in_gga(T, Y, U))
convert_in_gga(X, Y, Z) → U6_gga(X, Y, Z, head_in_ga(X, H))
head_in_ga([], X2) → head_out_ga([], X2)
head_in_ga(.(H, X3), H) → head_out_ga(.(H, X3), H)
U6_gga(X, Y, Z, head_out_ga(X, H)) → U7_gga(X, Y, Z, H, p_in_aa(H, P))
p_in_aa(s(X), X) → p_out_aa(s(X), X)
p_in_aa(0, 0) → p_out_aa(0, 0)
U7_gga(X, Y, Z, H, p_out_aa(H, P)) → U8_gga(X, Y, Z, H, P, tail_in_ga(X, T))
U8_gga(X, Y, Z, H, P, tail_out_ga(X, T)) → U9_gga(X, Y, Z, H, P, T, convert_in_aga(.(P, T), Y, U))
convert_in_aga([], X1, Z) → U1_aga(X1, Z, eq_in_ag(Z, 0))
U1_aga(X1, Z, eq_out_ag(Z, 0)) → convert_out_aga([], X1, Z)
convert_in_aga(X, Y, Z) → U2_aga(X, Y, Z, head_in_ag(X, 0))
head_in_ag([], X2) → head_out_ag([], X2)
head_in_ag(.(H, X3), H) → head_out_ag(.(H, X3), H)
U2_aga(X, Y, Z, head_out_ag(X, 0)) → U3_aga(X, Y, Z, tail_in_aa(X, T))
tail_in_aa([], []) → tail_out_aa([], [])
tail_in_aa(.(X4, Xs), Xs) → tail_out_aa(.(X4, Xs), Xs)
U3_aga(X, Y, Z, tail_out_aa(X, T)) → U4_aga(X, Y, Z, T, convert_in_aga(T, Y, U))
convert_in_aga(X, Y, Z) → U6_aga(X, Y, Z, head_in_aa(X, H))
head_in_aa([], X2) → head_out_aa([], X2)
head_in_aa(.(H, X3), H) → head_out_aa(.(H, X3), H)
U6_aga(X, Y, Z, head_out_aa(X, H)) → U7_aga(X, Y, Z, H, p_in_aa(H, P))
U7_aga(X, Y, Z, H, p_out_aa(H, P)) → U8_aga(X, Y, Z, H, P, tail_in_aa(X, T))
U8_aga(X, Y, Z, H, P, tail_out_aa(X, T)) → U9_aga(X, Y, Z, H, P, T, convert_in_aga(.(P, T), Y, U))
U9_aga(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → U10_aga(X, Y, Z, p_in_ag(Z, U))
p_in_ag(s(X), X) → p_out_ag(s(X), X)
p_in_ag(0, 0) → p_out_ag(0, 0)
U10_aga(X, Y, Z, p_out_ag(Z, U)) → convert_out_aga(X, Y, Z)
U4_aga(X, Y, Z, T, convert_out_aga(T, Y, U)) → U5_aga(X, Y, Z, times_in_gga(U, Y, Z))
times_in_gga(0, Y, Z) → U11_gga(Y, Z, eq_in_ag(Z, 0))
U11_gga(Y, Z, eq_out_ag(Z, 0)) → times_out_gga(0, Y, Z)
times_in_gga(X, Y, Z) → U12_gga(X, Y, Z, p_in_ga(X, P))
p_in_ga(s(X), X) → p_out_ga(s(X), X)
p_in_ga(0, 0) → p_out_ga(0, 0)
U12_gga(X, Y, Z, p_out_ga(X, P)) → U13_gga(X, Y, Z, P, times_in_gga(P, Y, U))
U13_gga(X, Y, Z, P, times_out_gga(P, Y, U)) → U14_gga(X, Y, Z, plus_in_gga(Y, U, Z))
plus_in_gga(0, Y, Z) → U15_gga(Y, Z, eq_in_ga(Y, Z))
eq_in_ga(X, X) → eq_out_ga(X, X)
U15_gga(Y, Z, eq_out_ga(Y, Z)) → plus_out_gga(0, Y, Z)
plus_in_gga(X, Y, Z) → U16_gga(X, Y, Z, p_in_ga(X, P))
U16_gga(X, Y, Z, p_out_ga(X, P)) → U17_gga(X, Y, Z, P, plus_in_gga(P, Y, U))
U17_gga(X, Y, Z, P, plus_out_gga(P, Y, U)) → U18_gga(X, Y, Z, p_in_ag(Z, U))
U18_gga(X, Y, Z, p_out_ag(Z, U)) → plus_out_gga(X, Y, Z)
U14_gga(X, Y, Z, plus_out_gga(Y, U, Z)) → times_out_gga(X, Y, Z)
U5_aga(X, Y, Z, times_out_gga(U, Y, Z)) → convert_out_aga(X, Y, Z)
U9_gga(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → U10_gga(X, Y, Z, p_in_ag(Z, U))
U10_gga(X, Y, Z, p_out_ag(Z, U)) → convert_out_gga(X, Y, Z)
U4_gga(X, Y, Z, T, convert_out_gga(T, Y, U)) → U5_gga(X, Y, Z, times_in_gga(U, Y, Z))
U5_gga(X, Y, Z, times_out_gga(U, Y, Z)) → convert_out_gga(X, Y, Z)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
convert_in_gga([], X1, Z) → U1_gga(X1, Z, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U1_gga(X1, Z, eq_out_ag(Z, 0)) → convert_out_gga([], X1, Z)
convert_in_gga(X, Y, Z) → U2_gga(X, Y, Z, head_in_gg(X, 0))
head_in_gg([], X2) → head_out_gg([], X2)
head_in_gg(.(H, X3), H) → head_out_gg(.(H, X3), H)
U2_gga(X, Y, Z, head_out_gg(X, 0)) → U3_gga(X, Y, Z, tail_in_ga(X, T))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X4, Xs), Xs) → tail_out_ga(.(X4, Xs), Xs)
U3_gga(X, Y, Z, tail_out_ga(X, T)) → U4_gga(X, Y, Z, T, convert_in_gga(T, Y, U))
convert_in_gga(X, Y, Z) → U6_gga(X, Y, Z, head_in_ga(X, H))
head_in_ga([], X2) → head_out_ga([], X2)
head_in_ga(.(H, X3), H) → head_out_ga(.(H, X3), H)
U6_gga(X, Y, Z, head_out_ga(X, H)) → U7_gga(X, Y, Z, H, p_in_aa(H, P))
p_in_aa(s(X), X) → p_out_aa(s(X), X)
p_in_aa(0, 0) → p_out_aa(0, 0)
U7_gga(X, Y, Z, H, p_out_aa(H, P)) → U8_gga(X, Y, Z, H, P, tail_in_ga(X, T))
U8_gga(X, Y, Z, H, P, tail_out_ga(X, T)) → U9_gga(X, Y, Z, H, P, T, convert_in_aga(.(P, T), Y, U))
convert_in_aga([], X1, Z) → U1_aga(X1, Z, eq_in_ag(Z, 0))
U1_aga(X1, Z, eq_out_ag(Z, 0)) → convert_out_aga([], X1, Z)
convert_in_aga(X, Y, Z) → U2_aga(X, Y, Z, head_in_ag(X, 0))
head_in_ag([], X2) → head_out_ag([], X2)
head_in_ag(.(H, X3), H) → head_out_ag(.(H, X3), H)
U2_aga(X, Y, Z, head_out_ag(X, 0)) → U3_aga(X, Y, Z, tail_in_aa(X, T))
tail_in_aa([], []) → tail_out_aa([], [])
tail_in_aa(.(X4, Xs), Xs) → tail_out_aa(.(X4, Xs), Xs)
U3_aga(X, Y, Z, tail_out_aa(X, T)) → U4_aga(X, Y, Z, T, convert_in_aga(T, Y, U))
convert_in_aga(X, Y, Z) → U6_aga(X, Y, Z, head_in_aa(X, H))
head_in_aa([], X2) → head_out_aa([], X2)
head_in_aa(.(H, X3), H) → head_out_aa(.(H, X3), H)
U6_aga(X, Y, Z, head_out_aa(X, H)) → U7_aga(X, Y, Z, H, p_in_aa(H, P))
U7_aga(X, Y, Z, H, p_out_aa(H, P)) → U8_aga(X, Y, Z, H, P, tail_in_aa(X, T))
U8_aga(X, Y, Z, H, P, tail_out_aa(X, T)) → U9_aga(X, Y, Z, H, P, T, convert_in_aga(.(P, T), Y, U))
U9_aga(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → U10_aga(X, Y, Z, p_in_ag(Z, U))
p_in_ag(s(X), X) → p_out_ag(s(X), X)
p_in_ag(0, 0) → p_out_ag(0, 0)
U10_aga(X, Y, Z, p_out_ag(Z, U)) → convert_out_aga(X, Y, Z)
U4_aga(X, Y, Z, T, convert_out_aga(T, Y, U)) → U5_aga(X, Y, Z, times_in_gga(U, Y, Z))
times_in_gga(0, Y, Z) → U11_gga(Y, Z, eq_in_ag(Z, 0))
U11_gga(Y, Z, eq_out_ag(Z, 0)) → times_out_gga(0, Y, Z)
times_in_gga(X, Y, Z) → U12_gga(X, Y, Z, p_in_ga(X, P))
p_in_ga(s(X), X) → p_out_ga(s(X), X)
p_in_ga(0, 0) → p_out_ga(0, 0)
U12_gga(X, Y, Z, p_out_ga(X, P)) → U13_gga(X, Y, Z, P, times_in_gga(P, Y, U))
U13_gga(X, Y, Z, P, times_out_gga(P, Y, U)) → U14_gga(X, Y, Z, plus_in_gga(Y, U, Z))
plus_in_gga(0, Y, Z) → U15_gga(Y, Z, eq_in_ga(Y, Z))
eq_in_ga(X, X) → eq_out_ga(X, X)
U15_gga(Y, Z, eq_out_ga(Y, Z)) → plus_out_gga(0, Y, Z)
plus_in_gga(X, Y, Z) → U16_gga(X, Y, Z, p_in_ga(X, P))
U16_gga(X, Y, Z, p_out_ga(X, P)) → U17_gga(X, Y, Z, P, plus_in_gga(P, Y, U))
U17_gga(X, Y, Z, P, plus_out_gga(P, Y, U)) → U18_gga(X, Y, Z, p_in_ag(Z, U))
U18_gga(X, Y, Z, p_out_ag(Z, U)) → plus_out_gga(X, Y, Z)
U14_gga(X, Y, Z, plus_out_gga(Y, U, Z)) → times_out_gga(X, Y, Z)
U5_aga(X, Y, Z, times_out_gga(U, Y, Z)) → convert_out_aga(X, Y, Z)
U9_gga(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → U10_gga(X, Y, Z, p_in_ag(Z, U))
U10_gga(X, Y, Z, p_out_ag(Z, U)) → convert_out_gga(X, Y, Z)
U4_gga(X, Y, Z, T, convert_out_gga(T, Y, U)) → U5_gga(X, Y, Z, times_in_gga(U, Y, Z))
U5_gga(X, Y, Z, times_out_gga(U, Y, Z)) → convert_out_gga(X, Y, Z)
CONVERT_IN_GGA([], X1, Z) → U1_GGA(X1, Z, eq_in_ag(Z, 0))
CONVERT_IN_GGA([], X1, Z) → EQ_IN_AG(Z, 0)
CONVERT_IN_GGA(X, Y, Z) → U2_GGA(X, Y, Z, head_in_gg(X, 0))
CONVERT_IN_GGA(X, Y, Z) → HEAD_IN_GG(X, 0)
U2_GGA(X, Y, Z, head_out_gg(X, 0)) → U3_GGA(X, Y, Z, tail_in_ga(X, T))
U2_GGA(X, Y, Z, head_out_gg(X, 0)) → TAIL_IN_GA(X, T)
U3_GGA(X, Y, Z, tail_out_ga(X, T)) → U4_GGA(X, Y, Z, T, convert_in_gga(T, Y, U))
U3_GGA(X, Y, Z, tail_out_ga(X, T)) → CONVERT_IN_GGA(T, Y, U)
CONVERT_IN_GGA(X, Y, Z) → U6_GGA(X, Y, Z, head_in_ga(X, H))
CONVERT_IN_GGA(X, Y, Z) → HEAD_IN_GA(X, H)
U6_GGA(X, Y, Z, head_out_ga(X, H)) → U7_GGA(X, Y, Z, H, p_in_aa(H, P))
U6_GGA(X, Y, Z, head_out_ga(X, H)) → P_IN_AA(H, P)
U7_GGA(X, Y, Z, H, p_out_aa(H, P)) → U8_GGA(X, Y, Z, H, P, tail_in_ga(X, T))
U7_GGA(X, Y, Z, H, p_out_aa(H, P)) → TAIL_IN_GA(X, T)
U8_GGA(X, Y, Z, H, P, tail_out_ga(X, T)) → U9_GGA(X, Y, Z, H, P, T, convert_in_aga(.(P, T), Y, U))
U8_GGA(X, Y, Z, H, P, tail_out_ga(X, T)) → CONVERT_IN_AGA(.(P, T), Y, U)
CONVERT_IN_AGA([], X1, Z) → U1_AGA(X1, Z, eq_in_ag(Z, 0))
CONVERT_IN_AGA([], X1, Z) → EQ_IN_AG(Z, 0)
CONVERT_IN_AGA(X, Y, Z) → U2_AGA(X, Y, Z, head_in_ag(X, 0))
CONVERT_IN_AGA(X, Y, Z) → HEAD_IN_AG(X, 0)
U2_AGA(X, Y, Z, head_out_ag(X, 0)) → U3_AGA(X, Y, Z, tail_in_aa(X, T))
U2_AGA(X, Y, Z, head_out_ag(X, 0)) → TAIL_IN_AA(X, T)
U3_AGA(X, Y, Z, tail_out_aa(X, T)) → U4_AGA(X, Y, Z, T, convert_in_aga(T, Y, U))
U3_AGA(X, Y, Z, tail_out_aa(X, T)) → CONVERT_IN_AGA(T, Y, U)
CONVERT_IN_AGA(X, Y, Z) → U6_AGA(X, Y, Z, head_in_aa(X, H))
CONVERT_IN_AGA(X, Y, Z) → HEAD_IN_AA(X, H)
U6_AGA(X, Y, Z, head_out_aa(X, H)) → U7_AGA(X, Y, Z, H, p_in_aa(H, P))
U6_AGA(X, Y, Z, head_out_aa(X, H)) → P_IN_AA(H, P)
U7_AGA(X, Y, Z, H, p_out_aa(H, P)) → U8_AGA(X, Y, Z, H, P, tail_in_aa(X, T))
U7_AGA(X, Y, Z, H, p_out_aa(H, P)) → TAIL_IN_AA(X, T)
U8_AGA(X, Y, Z, H, P, tail_out_aa(X, T)) → U9_AGA(X, Y, Z, H, P, T, convert_in_aga(.(P, T), Y, U))
U8_AGA(X, Y, Z, H, P, tail_out_aa(X, T)) → CONVERT_IN_AGA(.(P, T), Y, U)
U9_AGA(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → U10_AGA(X, Y, Z, p_in_ag(Z, U))
U9_AGA(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → P_IN_AG(Z, U)
U4_AGA(X, Y, Z, T, convert_out_aga(T, Y, U)) → U5_AGA(X, Y, Z, times_in_gga(U, Y, Z))
U4_AGA(X, Y, Z, T, convert_out_aga(T, Y, U)) → TIMES_IN_GGA(U, Y, Z)
TIMES_IN_GGA(0, Y, Z) → U11_GGA(Y, Z, eq_in_ag(Z, 0))
TIMES_IN_GGA(0, Y, Z) → EQ_IN_AG(Z, 0)
TIMES_IN_GGA(X, Y, Z) → U12_GGA(X, Y, Z, p_in_ga(X, P))
TIMES_IN_GGA(X, Y, Z) → P_IN_GA(X, P)
U12_GGA(X, Y, Z, p_out_ga(X, P)) → U13_GGA(X, Y, Z, P, times_in_gga(P, Y, U))
U12_GGA(X, Y, Z, p_out_ga(X, P)) → TIMES_IN_GGA(P, Y, U)
U13_GGA(X, Y, Z, P, times_out_gga(P, Y, U)) → U14_GGA(X, Y, Z, plus_in_gga(Y, U, Z))
U13_GGA(X, Y, Z, P, times_out_gga(P, Y, U)) → PLUS_IN_GGA(Y, U, Z)
PLUS_IN_GGA(0, Y, Z) → U15_GGA(Y, Z, eq_in_ga(Y, Z))
PLUS_IN_GGA(0, Y, Z) → EQ_IN_GA(Y, Z)
PLUS_IN_GGA(X, Y, Z) → U16_GGA(X, Y, Z, p_in_ga(X, P))
PLUS_IN_GGA(X, Y, Z) → P_IN_GA(X, P)
U16_GGA(X, Y, Z, p_out_ga(X, P)) → U17_GGA(X, Y, Z, P, plus_in_gga(P, Y, U))
U16_GGA(X, Y, Z, p_out_ga(X, P)) → PLUS_IN_GGA(P, Y, U)
U17_GGA(X, Y, Z, P, plus_out_gga(P, Y, U)) → U18_GGA(X, Y, Z, p_in_ag(Z, U))
U17_GGA(X, Y, Z, P, plus_out_gga(P, Y, U)) → P_IN_AG(Z, U)
U9_GGA(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → U10_GGA(X, Y, Z, p_in_ag(Z, U))
U9_GGA(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → P_IN_AG(Z, U)
U4_GGA(X, Y, Z, T, convert_out_gga(T, Y, U)) → U5_GGA(X, Y, Z, times_in_gga(U, Y, Z))
U4_GGA(X, Y, Z, T, convert_out_gga(T, Y, U)) → TIMES_IN_GGA(U, Y, Z)
convert_in_gga([], X1, Z) → U1_gga(X1, Z, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U1_gga(X1, Z, eq_out_ag(Z, 0)) → convert_out_gga([], X1, Z)
convert_in_gga(X, Y, Z) → U2_gga(X, Y, Z, head_in_gg(X, 0))
head_in_gg([], X2) → head_out_gg([], X2)
head_in_gg(.(H, X3), H) → head_out_gg(.(H, X3), H)
U2_gga(X, Y, Z, head_out_gg(X, 0)) → U3_gga(X, Y, Z, tail_in_ga(X, T))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X4, Xs), Xs) → tail_out_ga(.(X4, Xs), Xs)
U3_gga(X, Y, Z, tail_out_ga(X, T)) → U4_gga(X, Y, Z, T, convert_in_gga(T, Y, U))
convert_in_gga(X, Y, Z) → U6_gga(X, Y, Z, head_in_ga(X, H))
head_in_ga([], X2) → head_out_ga([], X2)
head_in_ga(.(H, X3), H) → head_out_ga(.(H, X3), H)
U6_gga(X, Y, Z, head_out_ga(X, H)) → U7_gga(X, Y, Z, H, p_in_aa(H, P))
p_in_aa(s(X), X) → p_out_aa(s(X), X)
p_in_aa(0, 0) → p_out_aa(0, 0)
U7_gga(X, Y, Z, H, p_out_aa(H, P)) → U8_gga(X, Y, Z, H, P, tail_in_ga(X, T))
U8_gga(X, Y, Z, H, P, tail_out_ga(X, T)) → U9_gga(X, Y, Z, H, P, T, convert_in_aga(.(P, T), Y, U))
convert_in_aga([], X1, Z) → U1_aga(X1, Z, eq_in_ag(Z, 0))
U1_aga(X1, Z, eq_out_ag(Z, 0)) → convert_out_aga([], X1, Z)
convert_in_aga(X, Y, Z) → U2_aga(X, Y, Z, head_in_ag(X, 0))
head_in_ag([], X2) → head_out_ag([], X2)
head_in_ag(.(H, X3), H) → head_out_ag(.(H, X3), H)
U2_aga(X, Y, Z, head_out_ag(X, 0)) → U3_aga(X, Y, Z, tail_in_aa(X, T))
tail_in_aa([], []) → tail_out_aa([], [])
tail_in_aa(.(X4, Xs), Xs) → tail_out_aa(.(X4, Xs), Xs)
U3_aga(X, Y, Z, tail_out_aa(X, T)) → U4_aga(X, Y, Z, T, convert_in_aga(T, Y, U))
convert_in_aga(X, Y, Z) → U6_aga(X, Y, Z, head_in_aa(X, H))
head_in_aa([], X2) → head_out_aa([], X2)
head_in_aa(.(H, X3), H) → head_out_aa(.(H, X3), H)
U6_aga(X, Y, Z, head_out_aa(X, H)) → U7_aga(X, Y, Z, H, p_in_aa(H, P))
U7_aga(X, Y, Z, H, p_out_aa(H, P)) → U8_aga(X, Y, Z, H, P, tail_in_aa(X, T))
U8_aga(X, Y, Z, H, P, tail_out_aa(X, T)) → U9_aga(X, Y, Z, H, P, T, convert_in_aga(.(P, T), Y, U))
U9_aga(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → U10_aga(X, Y, Z, p_in_ag(Z, U))
p_in_ag(s(X), X) → p_out_ag(s(X), X)
p_in_ag(0, 0) → p_out_ag(0, 0)
U10_aga(X, Y, Z, p_out_ag(Z, U)) → convert_out_aga(X, Y, Z)
U4_aga(X, Y, Z, T, convert_out_aga(T, Y, U)) → U5_aga(X, Y, Z, times_in_gga(U, Y, Z))
times_in_gga(0, Y, Z) → U11_gga(Y, Z, eq_in_ag(Z, 0))
U11_gga(Y, Z, eq_out_ag(Z, 0)) → times_out_gga(0, Y, Z)
times_in_gga(X, Y, Z) → U12_gga(X, Y, Z, p_in_ga(X, P))
p_in_ga(s(X), X) → p_out_ga(s(X), X)
p_in_ga(0, 0) → p_out_ga(0, 0)
U12_gga(X, Y, Z, p_out_ga(X, P)) → U13_gga(X, Y, Z, P, times_in_gga(P, Y, U))
U13_gga(X, Y, Z, P, times_out_gga(P, Y, U)) → U14_gga(X, Y, Z, plus_in_gga(Y, U, Z))
plus_in_gga(0, Y, Z) → U15_gga(Y, Z, eq_in_ga(Y, Z))
eq_in_ga(X, X) → eq_out_ga(X, X)
U15_gga(Y, Z, eq_out_ga(Y, Z)) → plus_out_gga(0, Y, Z)
plus_in_gga(X, Y, Z) → U16_gga(X, Y, Z, p_in_ga(X, P))
U16_gga(X, Y, Z, p_out_ga(X, P)) → U17_gga(X, Y, Z, P, plus_in_gga(P, Y, U))
U17_gga(X, Y, Z, P, plus_out_gga(P, Y, U)) → U18_gga(X, Y, Z, p_in_ag(Z, U))
U18_gga(X, Y, Z, p_out_ag(Z, U)) → plus_out_gga(X, Y, Z)
U14_gga(X, Y, Z, plus_out_gga(Y, U, Z)) → times_out_gga(X, Y, Z)
U5_aga(X, Y, Z, times_out_gga(U, Y, Z)) → convert_out_aga(X, Y, Z)
U9_gga(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → U10_gga(X, Y, Z, p_in_ag(Z, U))
U10_gga(X, Y, Z, p_out_ag(Z, U)) → convert_out_gga(X, Y, Z)
U4_gga(X, Y, Z, T, convert_out_gga(T, Y, U)) → U5_gga(X, Y, Z, times_in_gga(U, Y, Z))
U5_gga(X, Y, Z, times_out_gga(U, Y, Z)) → convert_out_gga(X, Y, Z)
CONVERT_IN_GGA([], X1, Z) → U1_GGA(X1, Z, eq_in_ag(Z, 0))
CONVERT_IN_GGA([], X1, Z) → EQ_IN_AG(Z, 0)
CONVERT_IN_GGA(X, Y, Z) → U2_GGA(X, Y, Z, head_in_gg(X, 0))
CONVERT_IN_GGA(X, Y, Z) → HEAD_IN_GG(X, 0)
U2_GGA(X, Y, Z, head_out_gg(X, 0)) → U3_GGA(X, Y, Z, tail_in_ga(X, T))
U2_GGA(X, Y, Z, head_out_gg(X, 0)) → TAIL_IN_GA(X, T)
U3_GGA(X, Y, Z, tail_out_ga(X, T)) → U4_GGA(X, Y, Z, T, convert_in_gga(T, Y, U))
U3_GGA(X, Y, Z, tail_out_ga(X, T)) → CONVERT_IN_GGA(T, Y, U)
CONVERT_IN_GGA(X, Y, Z) → U6_GGA(X, Y, Z, head_in_ga(X, H))
CONVERT_IN_GGA(X, Y, Z) → HEAD_IN_GA(X, H)
U6_GGA(X, Y, Z, head_out_ga(X, H)) → U7_GGA(X, Y, Z, H, p_in_aa(H, P))
U6_GGA(X, Y, Z, head_out_ga(X, H)) → P_IN_AA(H, P)
U7_GGA(X, Y, Z, H, p_out_aa(H, P)) → U8_GGA(X, Y, Z, H, P, tail_in_ga(X, T))
U7_GGA(X, Y, Z, H, p_out_aa(H, P)) → TAIL_IN_GA(X, T)
U8_GGA(X, Y, Z, H, P, tail_out_ga(X, T)) → U9_GGA(X, Y, Z, H, P, T, convert_in_aga(.(P, T), Y, U))
U8_GGA(X, Y, Z, H, P, tail_out_ga(X, T)) → CONVERT_IN_AGA(.(P, T), Y, U)
CONVERT_IN_AGA([], X1, Z) → U1_AGA(X1, Z, eq_in_ag(Z, 0))
CONVERT_IN_AGA([], X1, Z) → EQ_IN_AG(Z, 0)
CONVERT_IN_AGA(X, Y, Z) → U2_AGA(X, Y, Z, head_in_ag(X, 0))
CONVERT_IN_AGA(X, Y, Z) → HEAD_IN_AG(X, 0)
U2_AGA(X, Y, Z, head_out_ag(X, 0)) → U3_AGA(X, Y, Z, tail_in_aa(X, T))
U2_AGA(X, Y, Z, head_out_ag(X, 0)) → TAIL_IN_AA(X, T)
U3_AGA(X, Y, Z, tail_out_aa(X, T)) → U4_AGA(X, Y, Z, T, convert_in_aga(T, Y, U))
U3_AGA(X, Y, Z, tail_out_aa(X, T)) → CONVERT_IN_AGA(T, Y, U)
CONVERT_IN_AGA(X, Y, Z) → U6_AGA(X, Y, Z, head_in_aa(X, H))
CONVERT_IN_AGA(X, Y, Z) → HEAD_IN_AA(X, H)
U6_AGA(X, Y, Z, head_out_aa(X, H)) → U7_AGA(X, Y, Z, H, p_in_aa(H, P))
U6_AGA(X, Y, Z, head_out_aa(X, H)) → P_IN_AA(H, P)
U7_AGA(X, Y, Z, H, p_out_aa(H, P)) → U8_AGA(X, Y, Z, H, P, tail_in_aa(X, T))
U7_AGA(X, Y, Z, H, p_out_aa(H, P)) → TAIL_IN_AA(X, T)
U8_AGA(X, Y, Z, H, P, tail_out_aa(X, T)) → U9_AGA(X, Y, Z, H, P, T, convert_in_aga(.(P, T), Y, U))
U8_AGA(X, Y, Z, H, P, tail_out_aa(X, T)) → CONVERT_IN_AGA(.(P, T), Y, U)
U9_AGA(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → U10_AGA(X, Y, Z, p_in_ag(Z, U))
U9_AGA(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → P_IN_AG(Z, U)
U4_AGA(X, Y, Z, T, convert_out_aga(T, Y, U)) → U5_AGA(X, Y, Z, times_in_gga(U, Y, Z))
U4_AGA(X, Y, Z, T, convert_out_aga(T, Y, U)) → TIMES_IN_GGA(U, Y, Z)
TIMES_IN_GGA(0, Y, Z) → U11_GGA(Y, Z, eq_in_ag(Z, 0))
TIMES_IN_GGA(0, Y, Z) → EQ_IN_AG(Z, 0)
TIMES_IN_GGA(X, Y, Z) → U12_GGA(X, Y, Z, p_in_ga(X, P))
TIMES_IN_GGA(X, Y, Z) → P_IN_GA(X, P)
U12_GGA(X, Y, Z, p_out_ga(X, P)) → U13_GGA(X, Y, Z, P, times_in_gga(P, Y, U))
U12_GGA(X, Y, Z, p_out_ga(X, P)) → TIMES_IN_GGA(P, Y, U)
U13_GGA(X, Y, Z, P, times_out_gga(P, Y, U)) → U14_GGA(X, Y, Z, plus_in_gga(Y, U, Z))
U13_GGA(X, Y, Z, P, times_out_gga(P, Y, U)) → PLUS_IN_GGA(Y, U, Z)
PLUS_IN_GGA(0, Y, Z) → U15_GGA(Y, Z, eq_in_ga(Y, Z))
PLUS_IN_GGA(0, Y, Z) → EQ_IN_GA(Y, Z)
PLUS_IN_GGA(X, Y, Z) → U16_GGA(X, Y, Z, p_in_ga(X, P))
PLUS_IN_GGA(X, Y, Z) → P_IN_GA(X, P)
U16_GGA(X, Y, Z, p_out_ga(X, P)) → U17_GGA(X, Y, Z, P, plus_in_gga(P, Y, U))
U16_GGA(X, Y, Z, p_out_ga(X, P)) → PLUS_IN_GGA(P, Y, U)
U17_GGA(X, Y, Z, P, plus_out_gga(P, Y, U)) → U18_GGA(X, Y, Z, p_in_ag(Z, U))
U17_GGA(X, Y, Z, P, plus_out_gga(P, Y, U)) → P_IN_AG(Z, U)
U9_GGA(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → U10_GGA(X, Y, Z, p_in_ag(Z, U))
U9_GGA(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → P_IN_AG(Z, U)
U4_GGA(X, Y, Z, T, convert_out_gga(T, Y, U)) → U5_GGA(X, Y, Z, times_in_gga(U, Y, Z))
U4_GGA(X, Y, Z, T, convert_out_gga(T, Y, U)) → TIMES_IN_GGA(U, Y, Z)
convert_in_gga([], X1, Z) → U1_gga(X1, Z, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U1_gga(X1, Z, eq_out_ag(Z, 0)) → convert_out_gga([], X1, Z)
convert_in_gga(X, Y, Z) → U2_gga(X, Y, Z, head_in_gg(X, 0))
head_in_gg([], X2) → head_out_gg([], X2)
head_in_gg(.(H, X3), H) → head_out_gg(.(H, X3), H)
U2_gga(X, Y, Z, head_out_gg(X, 0)) → U3_gga(X, Y, Z, tail_in_ga(X, T))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X4, Xs), Xs) → tail_out_ga(.(X4, Xs), Xs)
U3_gga(X, Y, Z, tail_out_ga(X, T)) → U4_gga(X, Y, Z, T, convert_in_gga(T, Y, U))
convert_in_gga(X, Y, Z) → U6_gga(X, Y, Z, head_in_ga(X, H))
head_in_ga([], X2) → head_out_ga([], X2)
head_in_ga(.(H, X3), H) → head_out_ga(.(H, X3), H)
U6_gga(X, Y, Z, head_out_ga(X, H)) → U7_gga(X, Y, Z, H, p_in_aa(H, P))
p_in_aa(s(X), X) → p_out_aa(s(X), X)
p_in_aa(0, 0) → p_out_aa(0, 0)
U7_gga(X, Y, Z, H, p_out_aa(H, P)) → U8_gga(X, Y, Z, H, P, tail_in_ga(X, T))
U8_gga(X, Y, Z, H, P, tail_out_ga(X, T)) → U9_gga(X, Y, Z, H, P, T, convert_in_aga(.(P, T), Y, U))
convert_in_aga([], X1, Z) → U1_aga(X1, Z, eq_in_ag(Z, 0))
U1_aga(X1, Z, eq_out_ag(Z, 0)) → convert_out_aga([], X1, Z)
convert_in_aga(X, Y, Z) → U2_aga(X, Y, Z, head_in_ag(X, 0))
head_in_ag([], X2) → head_out_ag([], X2)
head_in_ag(.(H, X3), H) → head_out_ag(.(H, X3), H)
U2_aga(X, Y, Z, head_out_ag(X, 0)) → U3_aga(X, Y, Z, tail_in_aa(X, T))
tail_in_aa([], []) → tail_out_aa([], [])
tail_in_aa(.(X4, Xs), Xs) → tail_out_aa(.(X4, Xs), Xs)
U3_aga(X, Y, Z, tail_out_aa(X, T)) → U4_aga(X, Y, Z, T, convert_in_aga(T, Y, U))
convert_in_aga(X, Y, Z) → U6_aga(X, Y, Z, head_in_aa(X, H))
head_in_aa([], X2) → head_out_aa([], X2)
head_in_aa(.(H, X3), H) → head_out_aa(.(H, X3), H)
U6_aga(X, Y, Z, head_out_aa(X, H)) → U7_aga(X, Y, Z, H, p_in_aa(H, P))
U7_aga(X, Y, Z, H, p_out_aa(H, P)) → U8_aga(X, Y, Z, H, P, tail_in_aa(X, T))
U8_aga(X, Y, Z, H, P, tail_out_aa(X, T)) → U9_aga(X, Y, Z, H, P, T, convert_in_aga(.(P, T), Y, U))
U9_aga(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → U10_aga(X, Y, Z, p_in_ag(Z, U))
p_in_ag(s(X), X) → p_out_ag(s(X), X)
p_in_ag(0, 0) → p_out_ag(0, 0)
U10_aga(X, Y, Z, p_out_ag(Z, U)) → convert_out_aga(X, Y, Z)
U4_aga(X, Y, Z, T, convert_out_aga(T, Y, U)) → U5_aga(X, Y, Z, times_in_gga(U, Y, Z))
times_in_gga(0, Y, Z) → U11_gga(Y, Z, eq_in_ag(Z, 0))
U11_gga(Y, Z, eq_out_ag(Z, 0)) → times_out_gga(0, Y, Z)
times_in_gga(X, Y, Z) → U12_gga(X, Y, Z, p_in_ga(X, P))
p_in_ga(s(X), X) → p_out_ga(s(X), X)
p_in_ga(0, 0) → p_out_ga(0, 0)
U12_gga(X, Y, Z, p_out_ga(X, P)) → U13_gga(X, Y, Z, P, times_in_gga(P, Y, U))
U13_gga(X, Y, Z, P, times_out_gga(P, Y, U)) → U14_gga(X, Y, Z, plus_in_gga(Y, U, Z))
plus_in_gga(0, Y, Z) → U15_gga(Y, Z, eq_in_ga(Y, Z))
eq_in_ga(X, X) → eq_out_ga(X, X)
U15_gga(Y, Z, eq_out_ga(Y, Z)) → plus_out_gga(0, Y, Z)
plus_in_gga(X, Y, Z) → U16_gga(X, Y, Z, p_in_ga(X, P))
U16_gga(X, Y, Z, p_out_ga(X, P)) → U17_gga(X, Y, Z, P, plus_in_gga(P, Y, U))
U17_gga(X, Y, Z, P, plus_out_gga(P, Y, U)) → U18_gga(X, Y, Z, p_in_ag(Z, U))
U18_gga(X, Y, Z, p_out_ag(Z, U)) → plus_out_gga(X, Y, Z)
U14_gga(X, Y, Z, plus_out_gga(Y, U, Z)) → times_out_gga(X, Y, Z)
U5_aga(X, Y, Z, times_out_gga(U, Y, Z)) → convert_out_aga(X, Y, Z)
U9_gga(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → U10_gga(X, Y, Z, p_in_ag(Z, U))
U10_gga(X, Y, Z, p_out_ag(Z, U)) → convert_out_gga(X, Y, Z)
U4_gga(X, Y, Z, T, convert_out_gga(T, Y, U)) → U5_gga(X, Y, Z, times_in_gga(U, Y, Z))
U5_gga(X, Y, Z, times_out_gga(U, Y, Z)) → convert_out_gga(X, Y, Z)
PLUS_IN_GGA(X, Y, Z) → U16_GGA(X, Y, Z, p_in_ga(X, P))
U16_GGA(X, Y, Z, p_out_ga(X, P)) → PLUS_IN_GGA(P, Y, U)
convert_in_gga([], X1, Z) → U1_gga(X1, Z, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U1_gga(X1, Z, eq_out_ag(Z, 0)) → convert_out_gga([], X1, Z)
convert_in_gga(X, Y, Z) → U2_gga(X, Y, Z, head_in_gg(X, 0))
head_in_gg([], X2) → head_out_gg([], X2)
head_in_gg(.(H, X3), H) → head_out_gg(.(H, X3), H)
U2_gga(X, Y, Z, head_out_gg(X, 0)) → U3_gga(X, Y, Z, tail_in_ga(X, T))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X4, Xs), Xs) → tail_out_ga(.(X4, Xs), Xs)
U3_gga(X, Y, Z, tail_out_ga(X, T)) → U4_gga(X, Y, Z, T, convert_in_gga(T, Y, U))
convert_in_gga(X, Y, Z) → U6_gga(X, Y, Z, head_in_ga(X, H))
head_in_ga([], X2) → head_out_ga([], X2)
head_in_ga(.(H, X3), H) → head_out_ga(.(H, X3), H)
U6_gga(X, Y, Z, head_out_ga(X, H)) → U7_gga(X, Y, Z, H, p_in_aa(H, P))
p_in_aa(s(X), X) → p_out_aa(s(X), X)
p_in_aa(0, 0) → p_out_aa(0, 0)
U7_gga(X, Y, Z, H, p_out_aa(H, P)) → U8_gga(X, Y, Z, H, P, tail_in_ga(X, T))
U8_gga(X, Y, Z, H, P, tail_out_ga(X, T)) → U9_gga(X, Y, Z, H, P, T, convert_in_aga(.(P, T), Y, U))
convert_in_aga([], X1, Z) → U1_aga(X1, Z, eq_in_ag(Z, 0))
U1_aga(X1, Z, eq_out_ag(Z, 0)) → convert_out_aga([], X1, Z)
convert_in_aga(X, Y, Z) → U2_aga(X, Y, Z, head_in_ag(X, 0))
head_in_ag([], X2) → head_out_ag([], X2)
head_in_ag(.(H, X3), H) → head_out_ag(.(H, X3), H)
U2_aga(X, Y, Z, head_out_ag(X, 0)) → U3_aga(X, Y, Z, tail_in_aa(X, T))
tail_in_aa([], []) → tail_out_aa([], [])
tail_in_aa(.(X4, Xs), Xs) → tail_out_aa(.(X4, Xs), Xs)
U3_aga(X, Y, Z, tail_out_aa(X, T)) → U4_aga(X, Y, Z, T, convert_in_aga(T, Y, U))
convert_in_aga(X, Y, Z) → U6_aga(X, Y, Z, head_in_aa(X, H))
head_in_aa([], X2) → head_out_aa([], X2)
head_in_aa(.(H, X3), H) → head_out_aa(.(H, X3), H)
U6_aga(X, Y, Z, head_out_aa(X, H)) → U7_aga(X, Y, Z, H, p_in_aa(H, P))
U7_aga(X, Y, Z, H, p_out_aa(H, P)) → U8_aga(X, Y, Z, H, P, tail_in_aa(X, T))
U8_aga(X, Y, Z, H, P, tail_out_aa(X, T)) → U9_aga(X, Y, Z, H, P, T, convert_in_aga(.(P, T), Y, U))
U9_aga(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → U10_aga(X, Y, Z, p_in_ag(Z, U))
p_in_ag(s(X), X) → p_out_ag(s(X), X)
p_in_ag(0, 0) → p_out_ag(0, 0)
U10_aga(X, Y, Z, p_out_ag(Z, U)) → convert_out_aga(X, Y, Z)
U4_aga(X, Y, Z, T, convert_out_aga(T, Y, U)) → U5_aga(X, Y, Z, times_in_gga(U, Y, Z))
times_in_gga(0, Y, Z) → U11_gga(Y, Z, eq_in_ag(Z, 0))
U11_gga(Y, Z, eq_out_ag(Z, 0)) → times_out_gga(0, Y, Z)
times_in_gga(X, Y, Z) → U12_gga(X, Y, Z, p_in_ga(X, P))
p_in_ga(s(X), X) → p_out_ga(s(X), X)
p_in_ga(0, 0) → p_out_ga(0, 0)
U12_gga(X, Y, Z, p_out_ga(X, P)) → U13_gga(X, Y, Z, P, times_in_gga(P, Y, U))
U13_gga(X, Y, Z, P, times_out_gga(P, Y, U)) → U14_gga(X, Y, Z, plus_in_gga(Y, U, Z))
plus_in_gga(0, Y, Z) → U15_gga(Y, Z, eq_in_ga(Y, Z))
eq_in_ga(X, X) → eq_out_ga(X, X)
U15_gga(Y, Z, eq_out_ga(Y, Z)) → plus_out_gga(0, Y, Z)
plus_in_gga(X, Y, Z) → U16_gga(X, Y, Z, p_in_ga(X, P))
U16_gga(X, Y, Z, p_out_ga(X, P)) → U17_gga(X, Y, Z, P, plus_in_gga(P, Y, U))
U17_gga(X, Y, Z, P, plus_out_gga(P, Y, U)) → U18_gga(X, Y, Z, p_in_ag(Z, U))
U18_gga(X, Y, Z, p_out_ag(Z, U)) → plus_out_gga(X, Y, Z)
U14_gga(X, Y, Z, plus_out_gga(Y, U, Z)) → times_out_gga(X, Y, Z)
U5_aga(X, Y, Z, times_out_gga(U, Y, Z)) → convert_out_aga(X, Y, Z)
U9_gga(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → U10_gga(X, Y, Z, p_in_ag(Z, U))
U10_gga(X, Y, Z, p_out_ag(Z, U)) → convert_out_gga(X, Y, Z)
U4_gga(X, Y, Z, T, convert_out_gga(T, Y, U)) → U5_gga(X, Y, Z, times_in_gga(U, Y, Z))
U5_gga(X, Y, Z, times_out_gga(U, Y, Z)) → convert_out_gga(X, Y, Z)
PLUS_IN_GGA(X, Y, Z) → U16_GGA(X, Y, Z, p_in_ga(X, P))
U16_GGA(X, Y, Z, p_out_ga(X, P)) → PLUS_IN_GGA(P, Y, U)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
p_in_ga(0, 0) → p_out_ga(0, 0)
PLUS_IN_GGA(X, Y) → U16_GGA(X, Y, p_in_ga(X))
U16_GGA(X, Y, p_out_ga(X, P)) → PLUS_IN_GGA(P, Y)
p_in_ga(s(X)) → p_out_ga(s(X), X)
p_in_ga(0) → p_out_ga(0, 0)
p_in_ga(x0)
PLUS_IN_GGA(s(x0), y1) → U16_GGA(s(x0), y1, p_out_ga(s(x0), x0))
PLUS_IN_GGA(0, y1) → U16_GGA(0, y1, p_out_ga(0, 0))
U16_GGA(X, Y, p_out_ga(X, P)) → PLUS_IN_GGA(P, Y)
PLUS_IN_GGA(s(x0), y1) → U16_GGA(s(x0), y1, p_out_ga(s(x0), x0))
PLUS_IN_GGA(0, y1) → U16_GGA(0, y1, p_out_ga(0, 0))
p_in_ga(s(X)) → p_out_ga(s(X), X)
p_in_ga(0) → p_out_ga(0, 0)
p_in_ga(x0)
U16_GGA(X, Y, p_out_ga(X, P)) → PLUS_IN_GGA(P, Y)
PLUS_IN_GGA(s(x0), y1) → U16_GGA(s(x0), y1, p_out_ga(s(x0), x0))
PLUS_IN_GGA(0, y1) → U16_GGA(0, y1, p_out_ga(0, 0))
p_in_ga(x0)
p_in_ga(x0)
U16_GGA(X, Y, p_out_ga(X, P)) → PLUS_IN_GGA(P, Y)
PLUS_IN_GGA(s(x0), y1) → U16_GGA(s(x0), y1, p_out_ga(s(x0), x0))
PLUS_IN_GGA(0, y1) → U16_GGA(0, y1, p_out_ga(0, 0))
U16_GGA(s(z0), z1, p_out_ga(s(z0), z0)) → PLUS_IN_GGA(z0, z1)
U16_GGA(0, z0, p_out_ga(0, 0)) → PLUS_IN_GGA(0, z0)
PLUS_IN_GGA(s(x0), y1) → U16_GGA(s(x0), y1, p_out_ga(s(x0), x0))
PLUS_IN_GGA(0, y1) → U16_GGA(0, y1, p_out_ga(0, 0))
U16_GGA(s(z0), z1, p_out_ga(s(z0), z0)) → PLUS_IN_GGA(z0, z1)
U16_GGA(0, z0, p_out_ga(0, 0)) → PLUS_IN_GGA(0, z0)
U16_GGA(0, z0, p_out_ga(0, 0)) → PLUS_IN_GGA(0, z0)
PLUS_IN_GGA(0, y1) → U16_GGA(0, y1, p_out_ga(0, 0))
U16_GGA(s(z0), z1, p_out_ga(s(z0), z0)) → PLUS_IN_GGA(z0, z1)
PLUS_IN_GGA(s(x0), y1) → U16_GGA(s(x0), y1, p_out_ga(s(x0), x0))
From the DPs we obtained the following set of size-change graphs:
TIMES_IN_GGA(X, Y, Z) → U12_GGA(X, Y, Z, p_in_ga(X, P))
U12_GGA(X, Y, Z, p_out_ga(X, P)) → TIMES_IN_GGA(P, Y, U)
convert_in_gga([], X1, Z) → U1_gga(X1, Z, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U1_gga(X1, Z, eq_out_ag(Z, 0)) → convert_out_gga([], X1, Z)
convert_in_gga(X, Y, Z) → U2_gga(X, Y, Z, head_in_gg(X, 0))
head_in_gg([], X2) → head_out_gg([], X2)
head_in_gg(.(H, X3), H) → head_out_gg(.(H, X3), H)
U2_gga(X, Y, Z, head_out_gg(X, 0)) → U3_gga(X, Y, Z, tail_in_ga(X, T))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X4, Xs), Xs) → tail_out_ga(.(X4, Xs), Xs)
U3_gga(X, Y, Z, tail_out_ga(X, T)) → U4_gga(X, Y, Z, T, convert_in_gga(T, Y, U))
convert_in_gga(X, Y, Z) → U6_gga(X, Y, Z, head_in_ga(X, H))
head_in_ga([], X2) → head_out_ga([], X2)
head_in_ga(.(H, X3), H) → head_out_ga(.(H, X3), H)
U6_gga(X, Y, Z, head_out_ga(X, H)) → U7_gga(X, Y, Z, H, p_in_aa(H, P))
p_in_aa(s(X), X) → p_out_aa(s(X), X)
p_in_aa(0, 0) → p_out_aa(0, 0)
U7_gga(X, Y, Z, H, p_out_aa(H, P)) → U8_gga(X, Y, Z, H, P, tail_in_ga(X, T))
U8_gga(X, Y, Z, H, P, tail_out_ga(X, T)) → U9_gga(X, Y, Z, H, P, T, convert_in_aga(.(P, T), Y, U))
convert_in_aga([], X1, Z) → U1_aga(X1, Z, eq_in_ag(Z, 0))
U1_aga(X1, Z, eq_out_ag(Z, 0)) → convert_out_aga([], X1, Z)
convert_in_aga(X, Y, Z) → U2_aga(X, Y, Z, head_in_ag(X, 0))
head_in_ag([], X2) → head_out_ag([], X2)
head_in_ag(.(H, X3), H) → head_out_ag(.(H, X3), H)
U2_aga(X, Y, Z, head_out_ag(X, 0)) → U3_aga(X, Y, Z, tail_in_aa(X, T))
tail_in_aa([], []) → tail_out_aa([], [])
tail_in_aa(.(X4, Xs), Xs) → tail_out_aa(.(X4, Xs), Xs)
U3_aga(X, Y, Z, tail_out_aa(X, T)) → U4_aga(X, Y, Z, T, convert_in_aga(T, Y, U))
convert_in_aga(X, Y, Z) → U6_aga(X, Y, Z, head_in_aa(X, H))
head_in_aa([], X2) → head_out_aa([], X2)
head_in_aa(.(H, X3), H) → head_out_aa(.(H, X3), H)
U6_aga(X, Y, Z, head_out_aa(X, H)) → U7_aga(X, Y, Z, H, p_in_aa(H, P))
U7_aga(X, Y, Z, H, p_out_aa(H, P)) → U8_aga(X, Y, Z, H, P, tail_in_aa(X, T))
U8_aga(X, Y, Z, H, P, tail_out_aa(X, T)) → U9_aga(X, Y, Z, H, P, T, convert_in_aga(.(P, T), Y, U))
U9_aga(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → U10_aga(X, Y, Z, p_in_ag(Z, U))
p_in_ag(s(X), X) → p_out_ag(s(X), X)
p_in_ag(0, 0) → p_out_ag(0, 0)
U10_aga(X, Y, Z, p_out_ag(Z, U)) → convert_out_aga(X, Y, Z)
U4_aga(X, Y, Z, T, convert_out_aga(T, Y, U)) → U5_aga(X, Y, Z, times_in_gga(U, Y, Z))
times_in_gga(0, Y, Z) → U11_gga(Y, Z, eq_in_ag(Z, 0))
U11_gga(Y, Z, eq_out_ag(Z, 0)) → times_out_gga(0, Y, Z)
times_in_gga(X, Y, Z) → U12_gga(X, Y, Z, p_in_ga(X, P))
p_in_ga(s(X), X) → p_out_ga(s(X), X)
p_in_ga(0, 0) → p_out_ga(0, 0)
U12_gga(X, Y, Z, p_out_ga(X, P)) → U13_gga(X, Y, Z, P, times_in_gga(P, Y, U))
U13_gga(X, Y, Z, P, times_out_gga(P, Y, U)) → U14_gga(X, Y, Z, plus_in_gga(Y, U, Z))
plus_in_gga(0, Y, Z) → U15_gga(Y, Z, eq_in_ga(Y, Z))
eq_in_ga(X, X) → eq_out_ga(X, X)
U15_gga(Y, Z, eq_out_ga(Y, Z)) → plus_out_gga(0, Y, Z)
plus_in_gga(X, Y, Z) → U16_gga(X, Y, Z, p_in_ga(X, P))
U16_gga(X, Y, Z, p_out_ga(X, P)) → U17_gga(X, Y, Z, P, plus_in_gga(P, Y, U))
U17_gga(X, Y, Z, P, plus_out_gga(P, Y, U)) → U18_gga(X, Y, Z, p_in_ag(Z, U))
U18_gga(X, Y, Z, p_out_ag(Z, U)) → plus_out_gga(X, Y, Z)
U14_gga(X, Y, Z, plus_out_gga(Y, U, Z)) → times_out_gga(X, Y, Z)
U5_aga(X, Y, Z, times_out_gga(U, Y, Z)) → convert_out_aga(X, Y, Z)
U9_gga(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → U10_gga(X, Y, Z, p_in_ag(Z, U))
U10_gga(X, Y, Z, p_out_ag(Z, U)) → convert_out_gga(X, Y, Z)
U4_gga(X, Y, Z, T, convert_out_gga(T, Y, U)) → U5_gga(X, Y, Z, times_in_gga(U, Y, Z))
U5_gga(X, Y, Z, times_out_gga(U, Y, Z)) → convert_out_gga(X, Y, Z)
TIMES_IN_GGA(X, Y, Z) → U12_GGA(X, Y, Z, p_in_ga(X, P))
U12_GGA(X, Y, Z, p_out_ga(X, P)) → TIMES_IN_GGA(P, Y, U)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
p_in_ga(0, 0) → p_out_ga(0, 0)
TIMES_IN_GGA(X, Y) → U12_GGA(X, Y, p_in_ga(X))
U12_GGA(X, Y, p_out_ga(X, P)) → TIMES_IN_GGA(P, Y)
p_in_ga(s(X)) → p_out_ga(s(X), X)
p_in_ga(0) → p_out_ga(0, 0)
p_in_ga(x0)
TIMES_IN_GGA(s(x0), y1) → U12_GGA(s(x0), y1, p_out_ga(s(x0), x0))
TIMES_IN_GGA(0, y1) → U12_GGA(0, y1, p_out_ga(0, 0))
U12_GGA(X, Y, p_out_ga(X, P)) → TIMES_IN_GGA(P, Y)
TIMES_IN_GGA(s(x0), y1) → U12_GGA(s(x0), y1, p_out_ga(s(x0), x0))
TIMES_IN_GGA(0, y1) → U12_GGA(0, y1, p_out_ga(0, 0))
p_in_ga(s(X)) → p_out_ga(s(X), X)
p_in_ga(0) → p_out_ga(0, 0)
p_in_ga(x0)
U12_GGA(X, Y, p_out_ga(X, P)) → TIMES_IN_GGA(P, Y)
TIMES_IN_GGA(s(x0), y1) → U12_GGA(s(x0), y1, p_out_ga(s(x0), x0))
TIMES_IN_GGA(0, y1) → U12_GGA(0, y1, p_out_ga(0, 0))
p_in_ga(x0)
p_in_ga(x0)
U12_GGA(X, Y, p_out_ga(X, P)) → TIMES_IN_GGA(P, Y)
TIMES_IN_GGA(s(x0), y1) → U12_GGA(s(x0), y1, p_out_ga(s(x0), x0))
TIMES_IN_GGA(0, y1) → U12_GGA(0, y1, p_out_ga(0, 0))
U12_GGA(s(z0), z1, p_out_ga(s(z0), z0)) → TIMES_IN_GGA(z0, z1)
U12_GGA(0, z0, p_out_ga(0, 0)) → TIMES_IN_GGA(0, z0)
TIMES_IN_GGA(s(x0), y1) → U12_GGA(s(x0), y1, p_out_ga(s(x0), x0))
TIMES_IN_GGA(0, y1) → U12_GGA(0, y1, p_out_ga(0, 0))
U12_GGA(s(z0), z1, p_out_ga(s(z0), z0)) → TIMES_IN_GGA(z0, z1)
U12_GGA(0, z0, p_out_ga(0, 0)) → TIMES_IN_GGA(0, z0)
U12_GGA(0, z0, p_out_ga(0, 0)) → TIMES_IN_GGA(0, z0)
TIMES_IN_GGA(0, y1) → U12_GGA(0, y1, p_out_ga(0, 0))
U12_GGA(s(z0), z1, p_out_ga(s(z0), z0)) → TIMES_IN_GGA(z0, z1)
TIMES_IN_GGA(s(x0), y1) → U12_GGA(s(x0), y1, p_out_ga(s(x0), x0))
From the DPs we obtained the following set of size-change graphs:
CONVERT_IN_AGA(X, Y, Z) → U2_AGA(X, Y, Z, head_in_ag(X, 0))
U2_AGA(X, Y, Z, head_out_ag(X, 0)) → U3_AGA(X, Y, Z, tail_in_aa(X, T))
U3_AGA(X, Y, Z, tail_out_aa(X, T)) → CONVERT_IN_AGA(T, Y, U)
CONVERT_IN_AGA(X, Y, Z) → U6_AGA(X, Y, Z, head_in_aa(X, H))
U6_AGA(X, Y, Z, head_out_aa(X, H)) → U7_AGA(X, Y, Z, H, p_in_aa(H, P))
U7_AGA(X, Y, Z, H, p_out_aa(H, P)) → U8_AGA(X, Y, Z, H, P, tail_in_aa(X, T))
U8_AGA(X, Y, Z, H, P, tail_out_aa(X, T)) → CONVERT_IN_AGA(.(P, T), Y, U)
convert_in_gga([], X1, Z) → U1_gga(X1, Z, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U1_gga(X1, Z, eq_out_ag(Z, 0)) → convert_out_gga([], X1, Z)
convert_in_gga(X, Y, Z) → U2_gga(X, Y, Z, head_in_gg(X, 0))
head_in_gg([], X2) → head_out_gg([], X2)
head_in_gg(.(H, X3), H) → head_out_gg(.(H, X3), H)
U2_gga(X, Y, Z, head_out_gg(X, 0)) → U3_gga(X, Y, Z, tail_in_ga(X, T))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X4, Xs), Xs) → tail_out_ga(.(X4, Xs), Xs)
U3_gga(X, Y, Z, tail_out_ga(X, T)) → U4_gga(X, Y, Z, T, convert_in_gga(T, Y, U))
convert_in_gga(X, Y, Z) → U6_gga(X, Y, Z, head_in_ga(X, H))
head_in_ga([], X2) → head_out_ga([], X2)
head_in_ga(.(H, X3), H) → head_out_ga(.(H, X3), H)
U6_gga(X, Y, Z, head_out_ga(X, H)) → U7_gga(X, Y, Z, H, p_in_aa(H, P))
p_in_aa(s(X), X) → p_out_aa(s(X), X)
p_in_aa(0, 0) → p_out_aa(0, 0)
U7_gga(X, Y, Z, H, p_out_aa(H, P)) → U8_gga(X, Y, Z, H, P, tail_in_ga(X, T))
U8_gga(X, Y, Z, H, P, tail_out_ga(X, T)) → U9_gga(X, Y, Z, H, P, T, convert_in_aga(.(P, T), Y, U))
convert_in_aga([], X1, Z) → U1_aga(X1, Z, eq_in_ag(Z, 0))
U1_aga(X1, Z, eq_out_ag(Z, 0)) → convert_out_aga([], X1, Z)
convert_in_aga(X, Y, Z) → U2_aga(X, Y, Z, head_in_ag(X, 0))
head_in_ag([], X2) → head_out_ag([], X2)
head_in_ag(.(H, X3), H) → head_out_ag(.(H, X3), H)
U2_aga(X, Y, Z, head_out_ag(X, 0)) → U3_aga(X, Y, Z, tail_in_aa(X, T))
tail_in_aa([], []) → tail_out_aa([], [])
tail_in_aa(.(X4, Xs), Xs) → tail_out_aa(.(X4, Xs), Xs)
U3_aga(X, Y, Z, tail_out_aa(X, T)) → U4_aga(X, Y, Z, T, convert_in_aga(T, Y, U))
convert_in_aga(X, Y, Z) → U6_aga(X, Y, Z, head_in_aa(X, H))
head_in_aa([], X2) → head_out_aa([], X2)
head_in_aa(.(H, X3), H) → head_out_aa(.(H, X3), H)
U6_aga(X, Y, Z, head_out_aa(X, H)) → U7_aga(X, Y, Z, H, p_in_aa(H, P))
U7_aga(X, Y, Z, H, p_out_aa(H, P)) → U8_aga(X, Y, Z, H, P, tail_in_aa(X, T))
U8_aga(X, Y, Z, H, P, tail_out_aa(X, T)) → U9_aga(X, Y, Z, H, P, T, convert_in_aga(.(P, T), Y, U))
U9_aga(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → U10_aga(X, Y, Z, p_in_ag(Z, U))
p_in_ag(s(X), X) → p_out_ag(s(X), X)
p_in_ag(0, 0) → p_out_ag(0, 0)
U10_aga(X, Y, Z, p_out_ag(Z, U)) → convert_out_aga(X, Y, Z)
U4_aga(X, Y, Z, T, convert_out_aga(T, Y, U)) → U5_aga(X, Y, Z, times_in_gga(U, Y, Z))
times_in_gga(0, Y, Z) → U11_gga(Y, Z, eq_in_ag(Z, 0))
U11_gga(Y, Z, eq_out_ag(Z, 0)) → times_out_gga(0, Y, Z)
times_in_gga(X, Y, Z) → U12_gga(X, Y, Z, p_in_ga(X, P))
p_in_ga(s(X), X) → p_out_ga(s(X), X)
p_in_ga(0, 0) → p_out_ga(0, 0)
U12_gga(X, Y, Z, p_out_ga(X, P)) → U13_gga(X, Y, Z, P, times_in_gga(P, Y, U))
U13_gga(X, Y, Z, P, times_out_gga(P, Y, U)) → U14_gga(X, Y, Z, plus_in_gga(Y, U, Z))
plus_in_gga(0, Y, Z) → U15_gga(Y, Z, eq_in_ga(Y, Z))
eq_in_ga(X, X) → eq_out_ga(X, X)
U15_gga(Y, Z, eq_out_ga(Y, Z)) → plus_out_gga(0, Y, Z)
plus_in_gga(X, Y, Z) → U16_gga(X, Y, Z, p_in_ga(X, P))
U16_gga(X, Y, Z, p_out_ga(X, P)) → U17_gga(X, Y, Z, P, plus_in_gga(P, Y, U))
U17_gga(X, Y, Z, P, plus_out_gga(P, Y, U)) → U18_gga(X, Y, Z, p_in_ag(Z, U))
U18_gga(X, Y, Z, p_out_ag(Z, U)) → plus_out_gga(X, Y, Z)
U14_gga(X, Y, Z, plus_out_gga(Y, U, Z)) → times_out_gga(X, Y, Z)
U5_aga(X, Y, Z, times_out_gga(U, Y, Z)) → convert_out_aga(X, Y, Z)
U9_gga(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → U10_gga(X, Y, Z, p_in_ag(Z, U))
U10_gga(X, Y, Z, p_out_ag(Z, U)) → convert_out_gga(X, Y, Z)
U4_gga(X, Y, Z, T, convert_out_gga(T, Y, U)) → U5_gga(X, Y, Z, times_in_gga(U, Y, Z))
U5_gga(X, Y, Z, times_out_gga(U, Y, Z)) → convert_out_gga(X, Y, Z)
CONVERT_IN_AGA(X, Y, Z) → U2_AGA(X, Y, Z, head_in_ag(X, 0))
U2_AGA(X, Y, Z, head_out_ag(X, 0)) → U3_AGA(X, Y, Z, tail_in_aa(X, T))
U3_AGA(X, Y, Z, tail_out_aa(X, T)) → CONVERT_IN_AGA(T, Y, U)
CONVERT_IN_AGA(X, Y, Z) → U6_AGA(X, Y, Z, head_in_aa(X, H))
U6_AGA(X, Y, Z, head_out_aa(X, H)) → U7_AGA(X, Y, Z, H, p_in_aa(H, P))
U7_AGA(X, Y, Z, H, p_out_aa(H, P)) → U8_AGA(X, Y, Z, H, P, tail_in_aa(X, T))
U8_AGA(X, Y, Z, H, P, tail_out_aa(X, T)) → CONVERT_IN_AGA(.(P, T), Y, U)
head_in_ag([], X2) → head_out_ag([], X2)
head_in_ag(.(H, X3), H) → head_out_ag(.(H, X3), H)
tail_in_aa([], []) → tail_out_aa([], [])
tail_in_aa(.(X4, Xs), Xs) → tail_out_aa(.(X4, Xs), Xs)
head_in_aa([], X2) → head_out_aa([], X2)
head_in_aa(.(H, X3), H) → head_out_aa(.(H, X3), H)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
p_in_aa(0, 0) → p_out_aa(0, 0)
CONVERT_IN_AGA(Y) → U2_AGA(Y, head_in_ag(0))
U2_AGA(Y, head_out_ag(0)) → U3_AGA(Y, tail_in_aa)
U3_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
CONVERT_IN_AGA(Y) → U6_AGA(Y, head_in_aa)
U6_AGA(Y, head_out_aa) → U7_AGA(Y, p_in_aa)
U7_AGA(Y, p_out_aa) → U8_AGA(Y, tail_in_aa)
U8_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
head_in_ag(X2) → head_out_ag(X2)
tail_in_aa → tail_out_aa
head_in_aa → head_out_aa
p_in_aa → p_out_aa
head_in_ag(x0)
tail_in_aa
head_in_aa
p_in_aa
CONVERT_IN_AGA(Y) → U2_AGA(Y, head_out_ag(0))
U2_AGA(Y, head_out_ag(0)) → U3_AGA(Y, tail_in_aa)
U3_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
CONVERT_IN_AGA(Y) → U6_AGA(Y, head_in_aa)
U6_AGA(Y, head_out_aa) → U7_AGA(Y, p_in_aa)
U7_AGA(Y, p_out_aa) → U8_AGA(Y, tail_in_aa)
U8_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
CONVERT_IN_AGA(Y) → U2_AGA(Y, head_out_ag(0))
head_in_ag(X2) → head_out_ag(X2)
tail_in_aa → tail_out_aa
head_in_aa → head_out_aa
p_in_aa → p_out_aa
head_in_ag(x0)
tail_in_aa
head_in_aa
p_in_aa
U2_AGA(Y, head_out_ag(0)) → U3_AGA(Y, tail_in_aa)
U3_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
CONVERT_IN_AGA(Y) → U6_AGA(Y, head_in_aa)
U6_AGA(Y, head_out_aa) → U7_AGA(Y, p_in_aa)
U7_AGA(Y, p_out_aa) → U8_AGA(Y, tail_in_aa)
U8_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
CONVERT_IN_AGA(Y) → U2_AGA(Y, head_out_ag(0))
tail_in_aa → tail_out_aa
p_in_aa → p_out_aa
head_in_aa → head_out_aa
head_in_ag(x0)
tail_in_aa
head_in_aa
p_in_aa
head_in_ag(x0)
U2_AGA(Y, head_out_ag(0)) → U3_AGA(Y, tail_in_aa)
U3_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
CONVERT_IN_AGA(Y) → U6_AGA(Y, head_in_aa)
U6_AGA(Y, head_out_aa) → U7_AGA(Y, p_in_aa)
U7_AGA(Y, p_out_aa) → U8_AGA(Y, tail_in_aa)
U8_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
CONVERT_IN_AGA(Y) → U2_AGA(Y, head_out_ag(0))
tail_in_aa → tail_out_aa
p_in_aa → p_out_aa
head_in_aa → head_out_aa
tail_in_aa
head_in_aa
p_in_aa
U2_AGA(Y, head_out_ag(0)) → U3_AGA(Y, tail_out_aa)
U3_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
CONVERT_IN_AGA(Y) → U6_AGA(Y, head_in_aa)
U6_AGA(Y, head_out_aa) → U7_AGA(Y, p_in_aa)
U7_AGA(Y, p_out_aa) → U8_AGA(Y, tail_in_aa)
U8_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
CONVERT_IN_AGA(Y) → U2_AGA(Y, head_out_ag(0))
U2_AGA(Y, head_out_ag(0)) → U3_AGA(Y, tail_out_aa)
tail_in_aa → tail_out_aa
p_in_aa → p_out_aa
head_in_aa → head_out_aa
tail_in_aa
head_in_aa
p_in_aa
CONVERT_IN_AGA(Y) → U6_AGA(Y, head_out_aa)
U3_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
U6_AGA(Y, head_out_aa) → U7_AGA(Y, p_in_aa)
U7_AGA(Y, p_out_aa) → U8_AGA(Y, tail_in_aa)
U8_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
CONVERT_IN_AGA(Y) → U2_AGA(Y, head_out_ag(0))
U2_AGA(Y, head_out_ag(0)) → U3_AGA(Y, tail_out_aa)
CONVERT_IN_AGA(Y) → U6_AGA(Y, head_out_aa)
tail_in_aa → tail_out_aa
p_in_aa → p_out_aa
head_in_aa → head_out_aa
tail_in_aa
head_in_aa
p_in_aa
U3_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
U6_AGA(Y, head_out_aa) → U7_AGA(Y, p_in_aa)
U7_AGA(Y, p_out_aa) → U8_AGA(Y, tail_in_aa)
U8_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
CONVERT_IN_AGA(Y) → U2_AGA(Y, head_out_ag(0))
U2_AGA(Y, head_out_ag(0)) → U3_AGA(Y, tail_out_aa)
CONVERT_IN_AGA(Y) → U6_AGA(Y, head_out_aa)
tail_in_aa → tail_out_aa
p_in_aa → p_out_aa
tail_in_aa
head_in_aa
p_in_aa
head_in_aa
U3_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
U6_AGA(Y, head_out_aa) → U7_AGA(Y, p_in_aa)
U7_AGA(Y, p_out_aa) → U8_AGA(Y, tail_in_aa)
U8_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
CONVERT_IN_AGA(Y) → U2_AGA(Y, head_out_ag(0))
U2_AGA(Y, head_out_ag(0)) → U3_AGA(Y, tail_out_aa)
CONVERT_IN_AGA(Y) → U6_AGA(Y, head_out_aa)
tail_in_aa → tail_out_aa
p_in_aa → p_out_aa
tail_in_aa
p_in_aa
U6_AGA(Y, head_out_aa) → U7_AGA(Y, p_out_aa)
U3_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
U7_AGA(Y, p_out_aa) → U8_AGA(Y, tail_in_aa)
U8_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
CONVERT_IN_AGA(Y) → U2_AGA(Y, head_out_ag(0))
U2_AGA(Y, head_out_ag(0)) → U3_AGA(Y, tail_out_aa)
CONVERT_IN_AGA(Y) → U6_AGA(Y, head_out_aa)
U6_AGA(Y, head_out_aa) → U7_AGA(Y, p_out_aa)
tail_in_aa → tail_out_aa
p_in_aa → p_out_aa
tail_in_aa
p_in_aa
U3_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
U7_AGA(Y, p_out_aa) → U8_AGA(Y, tail_in_aa)
U8_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
CONVERT_IN_AGA(Y) → U2_AGA(Y, head_out_ag(0))
U2_AGA(Y, head_out_ag(0)) → U3_AGA(Y, tail_out_aa)
CONVERT_IN_AGA(Y) → U6_AGA(Y, head_out_aa)
U6_AGA(Y, head_out_aa) → U7_AGA(Y, p_out_aa)
tail_in_aa → tail_out_aa
tail_in_aa
p_in_aa
p_in_aa
U3_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
U7_AGA(Y, p_out_aa) → U8_AGA(Y, tail_in_aa)
U8_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
CONVERT_IN_AGA(Y) → U2_AGA(Y, head_out_ag(0))
U2_AGA(Y, head_out_ag(0)) → U3_AGA(Y, tail_out_aa)
CONVERT_IN_AGA(Y) → U6_AGA(Y, head_out_aa)
U6_AGA(Y, head_out_aa) → U7_AGA(Y, p_out_aa)
tail_in_aa → tail_out_aa
tail_in_aa
U7_AGA(Y, p_out_aa) → U8_AGA(Y, tail_out_aa)
U3_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
U8_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
CONVERT_IN_AGA(Y) → U2_AGA(Y, head_out_ag(0))
U2_AGA(Y, head_out_ag(0)) → U3_AGA(Y, tail_out_aa)
CONVERT_IN_AGA(Y) → U6_AGA(Y, head_out_aa)
U6_AGA(Y, head_out_aa) → U7_AGA(Y, p_out_aa)
U7_AGA(Y, p_out_aa) → U8_AGA(Y, tail_out_aa)
tail_in_aa → tail_out_aa
tail_in_aa
U3_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
U8_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
CONVERT_IN_AGA(Y) → U2_AGA(Y, head_out_ag(0))
U2_AGA(Y, head_out_ag(0)) → U3_AGA(Y, tail_out_aa)
CONVERT_IN_AGA(Y) → U6_AGA(Y, head_out_aa)
U6_AGA(Y, head_out_aa) → U7_AGA(Y, p_out_aa)
U7_AGA(Y, p_out_aa) → U8_AGA(Y, tail_out_aa)
tail_in_aa
tail_in_aa
U3_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
U8_AGA(Y, tail_out_aa) → CONVERT_IN_AGA(Y)
CONVERT_IN_AGA(Y) → U2_AGA(Y, head_out_ag(0))
U2_AGA(Y, head_out_ag(0)) → U3_AGA(Y, tail_out_aa)
CONVERT_IN_AGA(Y) → U6_AGA(Y, head_out_aa)
U6_AGA(Y, head_out_aa) → U7_AGA(Y, p_out_aa)
U7_AGA(Y, p_out_aa) → U8_AGA(Y, tail_out_aa)
CONVERT_IN_GGA(X, Y, Z) → U2_GGA(X, Y, Z, head_in_gg(X, 0))
U2_GGA(X, Y, Z, head_out_gg(X, 0)) → U3_GGA(X, Y, Z, tail_in_ga(X, T))
U3_GGA(X, Y, Z, tail_out_ga(X, T)) → CONVERT_IN_GGA(T, Y, U)
convert_in_gga([], X1, Z) → U1_gga(X1, Z, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U1_gga(X1, Z, eq_out_ag(Z, 0)) → convert_out_gga([], X1, Z)
convert_in_gga(X, Y, Z) → U2_gga(X, Y, Z, head_in_gg(X, 0))
head_in_gg([], X2) → head_out_gg([], X2)
head_in_gg(.(H, X3), H) → head_out_gg(.(H, X3), H)
U2_gga(X, Y, Z, head_out_gg(X, 0)) → U3_gga(X, Y, Z, tail_in_ga(X, T))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X4, Xs), Xs) → tail_out_ga(.(X4, Xs), Xs)
U3_gga(X, Y, Z, tail_out_ga(X, T)) → U4_gga(X, Y, Z, T, convert_in_gga(T, Y, U))
convert_in_gga(X, Y, Z) → U6_gga(X, Y, Z, head_in_ga(X, H))
head_in_ga([], X2) → head_out_ga([], X2)
head_in_ga(.(H, X3), H) → head_out_ga(.(H, X3), H)
U6_gga(X, Y, Z, head_out_ga(X, H)) → U7_gga(X, Y, Z, H, p_in_aa(H, P))
p_in_aa(s(X), X) → p_out_aa(s(X), X)
p_in_aa(0, 0) → p_out_aa(0, 0)
U7_gga(X, Y, Z, H, p_out_aa(H, P)) → U8_gga(X, Y, Z, H, P, tail_in_ga(X, T))
U8_gga(X, Y, Z, H, P, tail_out_ga(X, T)) → U9_gga(X, Y, Z, H, P, T, convert_in_aga(.(P, T), Y, U))
convert_in_aga([], X1, Z) → U1_aga(X1, Z, eq_in_ag(Z, 0))
U1_aga(X1, Z, eq_out_ag(Z, 0)) → convert_out_aga([], X1, Z)
convert_in_aga(X, Y, Z) → U2_aga(X, Y, Z, head_in_ag(X, 0))
head_in_ag([], X2) → head_out_ag([], X2)
head_in_ag(.(H, X3), H) → head_out_ag(.(H, X3), H)
U2_aga(X, Y, Z, head_out_ag(X, 0)) → U3_aga(X, Y, Z, tail_in_aa(X, T))
tail_in_aa([], []) → tail_out_aa([], [])
tail_in_aa(.(X4, Xs), Xs) → tail_out_aa(.(X4, Xs), Xs)
U3_aga(X, Y, Z, tail_out_aa(X, T)) → U4_aga(X, Y, Z, T, convert_in_aga(T, Y, U))
convert_in_aga(X, Y, Z) → U6_aga(X, Y, Z, head_in_aa(X, H))
head_in_aa([], X2) → head_out_aa([], X2)
head_in_aa(.(H, X3), H) → head_out_aa(.(H, X3), H)
U6_aga(X, Y, Z, head_out_aa(X, H)) → U7_aga(X, Y, Z, H, p_in_aa(H, P))
U7_aga(X, Y, Z, H, p_out_aa(H, P)) → U8_aga(X, Y, Z, H, P, tail_in_aa(X, T))
U8_aga(X, Y, Z, H, P, tail_out_aa(X, T)) → U9_aga(X, Y, Z, H, P, T, convert_in_aga(.(P, T), Y, U))
U9_aga(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → U10_aga(X, Y, Z, p_in_ag(Z, U))
p_in_ag(s(X), X) → p_out_ag(s(X), X)
p_in_ag(0, 0) → p_out_ag(0, 0)
U10_aga(X, Y, Z, p_out_ag(Z, U)) → convert_out_aga(X, Y, Z)
U4_aga(X, Y, Z, T, convert_out_aga(T, Y, U)) → U5_aga(X, Y, Z, times_in_gga(U, Y, Z))
times_in_gga(0, Y, Z) → U11_gga(Y, Z, eq_in_ag(Z, 0))
U11_gga(Y, Z, eq_out_ag(Z, 0)) → times_out_gga(0, Y, Z)
times_in_gga(X, Y, Z) → U12_gga(X, Y, Z, p_in_ga(X, P))
p_in_ga(s(X), X) → p_out_ga(s(X), X)
p_in_ga(0, 0) → p_out_ga(0, 0)
U12_gga(X, Y, Z, p_out_ga(X, P)) → U13_gga(X, Y, Z, P, times_in_gga(P, Y, U))
U13_gga(X, Y, Z, P, times_out_gga(P, Y, U)) → U14_gga(X, Y, Z, plus_in_gga(Y, U, Z))
plus_in_gga(0, Y, Z) → U15_gga(Y, Z, eq_in_ga(Y, Z))
eq_in_ga(X, X) → eq_out_ga(X, X)
U15_gga(Y, Z, eq_out_ga(Y, Z)) → plus_out_gga(0, Y, Z)
plus_in_gga(X, Y, Z) → U16_gga(X, Y, Z, p_in_ga(X, P))
U16_gga(X, Y, Z, p_out_ga(X, P)) → U17_gga(X, Y, Z, P, plus_in_gga(P, Y, U))
U17_gga(X, Y, Z, P, plus_out_gga(P, Y, U)) → U18_gga(X, Y, Z, p_in_ag(Z, U))
U18_gga(X, Y, Z, p_out_ag(Z, U)) → plus_out_gga(X, Y, Z)
U14_gga(X, Y, Z, plus_out_gga(Y, U, Z)) → times_out_gga(X, Y, Z)
U5_aga(X, Y, Z, times_out_gga(U, Y, Z)) → convert_out_aga(X, Y, Z)
U9_gga(X, Y, Z, H, P, T, convert_out_aga(.(P, T), Y, U)) → U10_gga(X, Y, Z, p_in_ag(Z, U))
U10_gga(X, Y, Z, p_out_ag(Z, U)) → convert_out_gga(X, Y, Z)
U4_gga(X, Y, Z, T, convert_out_gga(T, Y, U)) → U5_gga(X, Y, Z, times_in_gga(U, Y, Z))
U5_gga(X, Y, Z, times_out_gga(U, Y, Z)) → convert_out_gga(X, Y, Z)
CONVERT_IN_GGA(X, Y, Z) → U2_GGA(X, Y, Z, head_in_gg(X, 0))
U2_GGA(X, Y, Z, head_out_gg(X, 0)) → U3_GGA(X, Y, Z, tail_in_ga(X, T))
U3_GGA(X, Y, Z, tail_out_ga(X, T)) → CONVERT_IN_GGA(T, Y, U)
head_in_gg([], X2) → head_out_gg([], X2)
head_in_gg(.(H, X3), H) → head_out_gg(.(H, X3), H)
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X4, Xs), Xs) → tail_out_ga(.(X4, Xs), Xs)
CONVERT_IN_GGA(X, Y) → U2_GGA(X, Y, head_in_gg(X, 0))
U2_GGA(X, Y, head_out_gg(X, 0)) → U3_GGA(X, Y, tail_in_ga(X))
U3_GGA(X, Y, tail_out_ga(X, T)) → CONVERT_IN_GGA(T, Y)
head_in_gg([], X2) → head_out_gg([], X2)
head_in_gg(.(H, X3), H) → head_out_gg(.(H, X3), H)
tail_in_ga([]) → tail_out_ga([], [])
tail_in_ga(.(X4, Xs)) → tail_out_ga(.(X4, Xs), Xs)
head_in_gg(x0, x1)
tail_in_ga(x0)
CONVERT_IN_GGA([], y1) → U2_GGA([], y1, head_out_gg([], 0))
CONVERT_IN_GGA(.(0, x1), y1) → U2_GGA(.(0, x1), y1, head_out_gg(.(0, x1), 0))
U2_GGA(X, Y, head_out_gg(X, 0)) → U3_GGA(X, Y, tail_in_ga(X))
U3_GGA(X, Y, tail_out_ga(X, T)) → CONVERT_IN_GGA(T, Y)
CONVERT_IN_GGA([], y1) → U2_GGA([], y1, head_out_gg([], 0))
CONVERT_IN_GGA(.(0, x1), y1) → U2_GGA(.(0, x1), y1, head_out_gg(.(0, x1), 0))
head_in_gg([], X2) → head_out_gg([], X2)
head_in_gg(.(H, X3), H) → head_out_gg(.(H, X3), H)
tail_in_ga([]) → tail_out_ga([], [])
tail_in_ga(.(X4, Xs)) → tail_out_ga(.(X4, Xs), Xs)
head_in_gg(x0, x1)
tail_in_ga(x0)
U2_GGA(X, Y, head_out_gg(X, 0)) → U3_GGA(X, Y, tail_in_ga(X))
U3_GGA(X, Y, tail_out_ga(X, T)) → CONVERT_IN_GGA(T, Y)
CONVERT_IN_GGA([], y1) → U2_GGA([], y1, head_out_gg([], 0))
CONVERT_IN_GGA(.(0, x1), y1) → U2_GGA(.(0, x1), y1, head_out_gg(.(0, x1), 0))
tail_in_ga([]) → tail_out_ga([], [])
tail_in_ga(.(X4, Xs)) → tail_out_ga(.(X4, Xs), Xs)
head_in_gg(x0, x1)
tail_in_ga(x0)
head_in_gg(x0, x1)
U2_GGA(X, Y, head_out_gg(X, 0)) → U3_GGA(X, Y, tail_in_ga(X))
U3_GGA(X, Y, tail_out_ga(X, T)) → CONVERT_IN_GGA(T, Y)
CONVERT_IN_GGA([], y1) → U2_GGA([], y1, head_out_gg([], 0))
CONVERT_IN_GGA(.(0, x1), y1) → U2_GGA(.(0, x1), y1, head_out_gg(.(0, x1), 0))
tail_in_ga([]) → tail_out_ga([], [])
tail_in_ga(.(X4, Xs)) → tail_out_ga(.(X4, Xs), Xs)
tail_in_ga(x0)
U2_GGA([], y1, head_out_gg([], 0)) → U3_GGA([], y1, tail_out_ga([], []))
U2_GGA(.(x0, x1), y1, head_out_gg(.(x0, x1), 0)) → U3_GGA(.(x0, x1), y1, tail_out_ga(.(x0, x1), x1))
U3_GGA(X, Y, tail_out_ga(X, T)) → CONVERT_IN_GGA(T, Y)
CONVERT_IN_GGA([], y1) → U2_GGA([], y1, head_out_gg([], 0))
CONVERT_IN_GGA(.(0, x1), y1) → U2_GGA(.(0, x1), y1, head_out_gg(.(0, x1), 0))
U2_GGA([], y1, head_out_gg([], 0)) → U3_GGA([], y1, tail_out_ga([], []))
U2_GGA(.(x0, x1), y1, head_out_gg(.(x0, x1), 0)) → U3_GGA(.(x0, x1), y1, tail_out_ga(.(x0, x1), x1))
tail_in_ga([]) → tail_out_ga([], [])
tail_in_ga(.(X4, Xs)) → tail_out_ga(.(X4, Xs), Xs)
tail_in_ga(x0)
U3_GGA(X, Y, tail_out_ga(X, T)) → CONVERT_IN_GGA(T, Y)
CONVERT_IN_GGA([], y1) → U2_GGA([], y1, head_out_gg([], 0))
CONVERT_IN_GGA(.(0, x1), y1) → U2_GGA(.(0, x1), y1, head_out_gg(.(0, x1), 0))
U2_GGA([], y1, head_out_gg([], 0)) → U3_GGA([], y1, tail_out_ga([], []))
U2_GGA(.(x0, x1), y1, head_out_gg(.(x0, x1), 0)) → U3_GGA(.(x0, x1), y1, tail_out_ga(.(x0, x1), x1))
tail_in_ga(x0)
tail_in_ga(x0)
U3_GGA(X, Y, tail_out_ga(X, T)) → CONVERT_IN_GGA(T, Y)
CONVERT_IN_GGA([], y1) → U2_GGA([], y1, head_out_gg([], 0))
CONVERT_IN_GGA(.(0, x1), y1) → U2_GGA(.(0, x1), y1, head_out_gg(.(0, x1), 0))
U2_GGA([], y1, head_out_gg([], 0)) → U3_GGA([], y1, tail_out_ga([], []))
U2_GGA(.(x0, x1), y1, head_out_gg(.(x0, x1), 0)) → U3_GGA(.(x0, x1), y1, tail_out_ga(.(x0, x1), x1))
U2_GGA(.(0, z0), z1, head_out_gg(.(0, z0), 0)) → U3_GGA(.(0, z0), z1, tail_out_ga(.(0, z0), z0))
U3_GGA(X, Y, tail_out_ga(X, T)) → CONVERT_IN_GGA(T, Y)
CONVERT_IN_GGA([], y1) → U2_GGA([], y1, head_out_gg([], 0))
CONVERT_IN_GGA(.(0, x1), y1) → U2_GGA(.(0, x1), y1, head_out_gg(.(0, x1), 0))
U2_GGA([], y1, head_out_gg([], 0)) → U3_GGA([], y1, tail_out_ga([], []))
U2_GGA(.(0, z0), z1, head_out_gg(.(0, z0), 0)) → U3_GGA(.(0, z0), z1, tail_out_ga(.(0, z0), z0))
U3_GGA([], z0, tail_out_ga([], [])) → CONVERT_IN_GGA([], z0)
U3_GGA(.(0, z0), z1, tail_out_ga(.(0, z0), z0)) → CONVERT_IN_GGA(z0, z1)
CONVERT_IN_GGA([], y1) → U2_GGA([], y1, head_out_gg([], 0))
CONVERT_IN_GGA(.(0, x1), y1) → U2_GGA(.(0, x1), y1, head_out_gg(.(0, x1), 0))
U2_GGA([], y1, head_out_gg([], 0)) → U3_GGA([], y1, tail_out_ga([], []))
U2_GGA(.(0, z0), z1, head_out_gg(.(0, z0), 0)) → U3_GGA(.(0, z0), z1, tail_out_ga(.(0, z0), z0))
U3_GGA([], z0, tail_out_ga([], [])) → CONVERT_IN_GGA([], z0)
U3_GGA(.(0, z0), z1, tail_out_ga(.(0, z0), z0)) → CONVERT_IN_GGA(z0, z1)
U2_GGA([], y1, head_out_gg([], 0)) → U3_GGA([], y1, tail_out_ga([], []))
U3_GGA([], z0, tail_out_ga([], [])) → CONVERT_IN_GGA([], z0)
CONVERT_IN_GGA([], y1) → U2_GGA([], y1, head_out_gg([], 0))
CONVERT_IN_GGA(.(0, x1), y1) → U2_GGA(.(0, x1), y1, head_out_gg(.(0, x1), 0))
U2_GGA(.(0, z0), z1, head_out_gg(.(0, z0), 0)) → U3_GGA(.(0, z0), z1, tail_out_ga(.(0, z0), z0))
U3_GGA(.(0, z0), z1, tail_out_ga(.(0, z0), z0)) → CONVERT_IN_GGA(z0, z1)
From the DPs we obtained the following set of size-change graphs: