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 NonTerminationProof (⇔)
↳15 FALSE
↳16 PiDP
↳17 UsableRulesProof (⇔)
↳18 PiDP
↳19 PiDPToQDPProof (⇐)
↳20 QDP
↳21 Rewriting (⇔)
↳22 QDP
↳23 Rewriting (⇔)
↳24 QDP
↳25 Rewriting (⇔)
↳26 QDP
↳27 Rewriting (⇔)
↳28 QDP
↳29 UsableRulesProof (⇔)
↳30 QDP
↳31 QReductionProof (⇔)
↳32 QDP
↳33 Rewriting (⇔)
↳34 QDP
↳35 UsableRulesProof (⇔)
↳36 QDP
↳37 QReductionProof (⇔)
↳38 QDP
↳39 Rewriting (⇔)
↳40 QDP
↳41 UsableRulesProof (⇔)
↳42 QDP
↳43 QReductionProof (⇔)
↳44 QDP
↳45 NonTerminationProof (⇔)
↳46 FALSE
↳47 PiDP
↳48 UsableRulesProof (⇔)
↳49 PiDP
↳50 PiDPToQDPProof (⇐)
↳51 QDP
↳52 UsableRulesReductionPairsProof (⇔)
↳53 QDP
↳54 Narrowing (⇐)
↳55 QDP
↳56 Narrowing (⇐)
↳57 QDP
↳58 Narrowing (⇐)
↳59 QDP
↳60 UsableRulesProof (⇔)
↳61 QDP
↳62 QReductionProof (⇔)
↳63 QDP
↳64 Instantiation (⇔)
↳65 QDP
↳66 Instantiation (⇔)
↳67 QDP
↳68 Instantiation (⇔)
↳69 QDP
↳70 NonTerminationProof (⇔)
↳71 FALSE
↳72 PrologToPiTRSProof (⇐)
↳73 PiTRS
↳74 DependencyPairsProof (⇔)
↳75 PiDP
↳76 DependencyGraphProof (⇔)
↳77 AND
↳78 PiDP
↳79 UsableRulesProof (⇔)
↳80 PiDP
↳81 PiDPToQDPProof (⇐)
↳82 QDP
↳83 NonTerminationProof (⇔)
↳84 FALSE
↳85 PiDP
↳86 UsableRulesProof (⇔)
↳87 PiDP
↳88 PiDPToQDPProof (⇐)
↳89 QDP
↳90 Rewriting (⇔)
↳91 QDP
↳92 Rewriting (⇔)
↳93 QDP
↳94 Rewriting (⇔)
↳95 QDP
↳96 Rewriting (⇔)
↳97 QDP
↳98 UsableRulesProof (⇔)
↳99 QDP
↳100 QReductionProof (⇔)
↳101 QDP
↳102 Rewriting (⇔)
↳103 QDP
↳104 UsableRulesProof (⇔)
↳105 QDP
↳106 QReductionProof (⇔)
↳107 QDP
↳108 Rewriting (⇔)
↳109 QDP
↳110 UsableRulesProof (⇔)
↳111 QDP
↳112 QReductionProof (⇔)
↳113 QDP
↳114 NonTerminationProof (⇔)
↳115 FALSE
↳116 PiDP
↳117 UsableRulesProof (⇔)
↳118 PiDP
↳119 PiDPToQDPProof (⇐)
↳120 QDP
↳121 Narrowing (⇐)
↳122 QDP
↳123 Narrowing (⇐)
↳124 QDP
↳125 Narrowing (⇐)
↳126 QDP
↳127 UsableRulesProof (⇔)
↳128 QDP
↳129 QReductionProof (⇔)
↳130 QDP
↳131 Instantiation (⇔)
↳132 QDP
↳133 Instantiation (⇔)
↳134 QDP
↳135 Instantiation (⇔)
↳136 QDP
↳137 DependencyGraphProof (⇔)
↳138 AND
↳139 QDP
↳140 NonTerminationProof (⇔)
↳141 FALSE
↳142 QDP
↳143 QDPSizeChangeProof (⇔)
↳144 TRUE
goal_in_gaa(A, B, C) → U1_gaa(A, B, C, s2t_in_ga(A, T))
s2t_in_ga(0, L) → U22_ga(L, eq_in_ag(L, nil))
eq_in_ag(X, X) → eq_out_ag(X, X)
U22_ga(L, eq_out_ag(L, nil)) → s2t_out_ga(0, L)
s2t_in_ga(X, node(T, X5, T)) → U23_ga(X, T, X5, p_in_ga(X, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U23_ga(X, T, X5, p_out_ga(X, P)) → U24_ga(X, T, X5, s2t_in_ga(P, T))
s2t_in_ga(X, node(nil, X6, T)) → U25_ga(X, X6, T, p_in_ga(X, P))
U25_ga(X, X6, T, p_out_ga(X, P)) → U26_ga(X, X6, T, s2t_in_ga(P, T))
s2t_in_ga(X, node(T, X7, nil)) → U27_ga(X, T, X7, p_in_ga(X, P))
U27_ga(X, T, X7, p_out_ga(X, P)) → U28_ga(X, T, X7, s2t_in_ga(P, T))
s2t_in_ga(X, node(nil, X8, nil)) → s2t_out_ga(X, node(nil, X8, nil))
U28_ga(X, T, X7, s2t_out_ga(P, T)) → s2t_out_ga(X, node(T, X7, nil))
U26_ga(X, X6, T, s2t_out_ga(P, T)) → s2t_out_ga(X, node(nil, X6, T))
U24_ga(X, T, X5, s2t_out_ga(P, T)) → s2t_out_ga(X, node(T, X5, T))
U1_gaa(A, B, C, s2t_out_ga(A, T)) → U2_gaa(A, B, C, tapplast_in_aaa(T, B, C))
tapplast_in_aaa(L, X, Last) → U3_aaa(L, X, Last, tappend_in_aaa(L, node(nil, X, nil), LX))
tappend_in_aaa(nil, Y, Z) → U7_aaa(Y, Z, eq_in_aa(Y, Z))
eq_in_aa(X, X) → eq_out_aa(X, X)
U7_aaa(Y, Z, eq_out_aa(Y, Z)) → tappend_out_aaa(nil, Y, Z)
tappend_in_aaa(T, T1, node(T1, X, T2)) → U8_aaa(T, T1, X, T2, left_in_ag(T, nil))
left_in_ag(nil, nil) → left_out_ag(nil, nil)
left_in_ag(node(L, X9, X10), L) → left_out_ag(node(L, X9, X10), L)
U8_aaa(T, T1, X, T2, left_out_ag(T, nil)) → U9_aaa(T, T1, X, T2, right_in_aa(T, T2))
right_in_aa(nil, nil) → right_out_aa(nil, nil)
right_in_aa(node(X11, X12, R), R) → right_out_aa(node(X11, X12, R), R)
U9_aaa(T, T1, X, T2, right_out_aa(T, T2)) → U10_aaa(T, T1, X, T2, value_in_aa(T, X))
value_in_aa(nil, nil) → value_out_aa(nil, nil)
value_in_aa(node(X13, X, X14), X) → value_out_aa(node(X13, X, X14), X)
U10_aaa(T, T1, X, T2, value_out_aa(T, X)) → tappend_out_aaa(T, T1, node(T1, X, T2))
tappend_in_aaa(T, T2, node(T1, X, T2)) → U11_aaa(T, T2, T1, X, left_in_aa(T, T1))
left_in_aa(nil, nil) → left_out_aa(nil, nil)
left_in_aa(node(L, X9, X10), L) → left_out_aa(node(L, X9, X10), L)
U11_aaa(T, T2, T1, X, left_out_aa(T, T1)) → U12_aaa(T, T2, T1, X, right_in_ag(T, nil))
right_in_ag(nil, nil) → right_out_ag(nil, nil)
right_in_ag(node(X11, X12, R), R) → right_out_ag(node(X11, X12, R), R)
U12_aaa(T, T2, T1, X, right_out_ag(T, nil)) → U13_aaa(T, T2, T1, X, value_in_aa(T, X))
U13_aaa(T, T2, T1, X, value_out_aa(T, X)) → tappend_out_aaa(T, T2, node(T1, X, T2))
tappend_in_aaa(T, T3, node(U, X, T2)) → U14_aaa(T, T3, U, X, T2, left_in_aa(T, T1))
U14_aaa(T, T3, U, X, T2, left_out_aa(T, T1)) → U15_aaa(T, T3, U, X, T2, T1, right_in_aa(T, T2))
U15_aaa(T, T3, U, X, T2, T1, right_out_aa(T, T2)) → U16_aaa(T, T3, U, X, T2, T1, value_in_aa(T, X))
U16_aaa(T, T3, U, X, T2, T1, value_out_aa(T, X)) → U17_aaa(T, T3, U, X, T2, tappend_in_aaa(T1, T3, U))
tappend_in_aaa(T, T1, node(T1, X, U)) → U18_aaa(T, T1, X, U, left_in_aa(T, T1))
U18_aaa(T, T1, X, U, left_out_aa(T, T1)) → U19_aaa(T, T1, X, U, right_in_aa(T, T2))
U19_aaa(T, T1, X, U, right_out_aa(T, T2)) → U20_aaa(T, T1, X, U, T2, value_in_aa(T, X))
U20_aaa(T, T1, X, U, T2, value_out_aa(T, X)) → U21_aaa(T, T1, X, U, tappend_in_aaa(T2, T3, U))
U21_aaa(T, T1, X, U, tappend_out_aaa(T2, T3, U)) → tappend_out_aaa(T, T1, node(T1, X, U))
U17_aaa(T, T3, U, X, T2, tappend_out_aaa(T1, T3, U)) → tappend_out_aaa(T, T3, node(U, X, T2))
U3_aaa(L, X, Last, tappend_out_aaa(L, node(nil, X, nil), LX)) → U4_aaa(L, X, Last, tlast_in_aa(Last, LX))
tlast_in_aa(X, node(nil, X, nil)) → tlast_out_aa(X, node(nil, X, nil))
tlast_in_aa(X, node(L, X1, X2)) → U5_aa(X, L, X1, X2, tlast_in_aa(X, L))
tlast_in_aa(X, node(X3, X4, R)) → U6_aa(X, X3, X4, R, tlast_in_aa(X, R))
U6_aa(X, X3, X4, R, tlast_out_aa(X, R)) → tlast_out_aa(X, node(X3, X4, R))
U5_aa(X, L, X1, X2, tlast_out_aa(X, L)) → tlast_out_aa(X, node(L, X1, X2))
U4_aaa(L, X, Last, tlast_out_aa(Last, LX)) → tapplast_out_aaa(L, X, Last)
U2_gaa(A, B, C, tapplast_out_aaa(T, B, C)) → goal_out_gaa(A, B, C)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
goal_in_gaa(A, B, C) → U1_gaa(A, B, C, s2t_in_ga(A, T))
s2t_in_ga(0, L) → U22_ga(L, eq_in_ag(L, nil))
eq_in_ag(X, X) → eq_out_ag(X, X)
U22_ga(L, eq_out_ag(L, nil)) → s2t_out_ga(0, L)
s2t_in_ga(X, node(T, X5, T)) → U23_ga(X, T, X5, p_in_ga(X, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U23_ga(X, T, X5, p_out_ga(X, P)) → U24_ga(X, T, X5, s2t_in_ga(P, T))
s2t_in_ga(X, node(nil, X6, T)) → U25_ga(X, X6, T, p_in_ga(X, P))
U25_ga(X, X6, T, p_out_ga(X, P)) → U26_ga(X, X6, T, s2t_in_ga(P, T))
s2t_in_ga(X, node(T, X7, nil)) → U27_ga(X, T, X7, p_in_ga(X, P))
U27_ga(X, T, X7, p_out_ga(X, P)) → U28_ga(X, T, X7, s2t_in_ga(P, T))
s2t_in_ga(X, node(nil, X8, nil)) → s2t_out_ga(X, node(nil, X8, nil))
U28_ga(X, T, X7, s2t_out_ga(P, T)) → s2t_out_ga(X, node(T, X7, nil))
U26_ga(X, X6, T, s2t_out_ga(P, T)) → s2t_out_ga(X, node(nil, X6, T))
U24_ga(X, T, X5, s2t_out_ga(P, T)) → s2t_out_ga(X, node(T, X5, T))
U1_gaa(A, B, C, s2t_out_ga(A, T)) → U2_gaa(A, B, C, tapplast_in_aaa(T, B, C))
tapplast_in_aaa(L, X, Last) → U3_aaa(L, X, Last, tappend_in_aaa(L, node(nil, X, nil), LX))
tappend_in_aaa(nil, Y, Z) → U7_aaa(Y, Z, eq_in_aa(Y, Z))
eq_in_aa(X, X) → eq_out_aa(X, X)
U7_aaa(Y, Z, eq_out_aa(Y, Z)) → tappend_out_aaa(nil, Y, Z)
tappend_in_aaa(T, T1, node(T1, X, T2)) → U8_aaa(T, T1, X, T2, left_in_ag(T, nil))
left_in_ag(nil, nil) → left_out_ag(nil, nil)
left_in_ag(node(L, X9, X10), L) → left_out_ag(node(L, X9, X10), L)
U8_aaa(T, T1, X, T2, left_out_ag(T, nil)) → U9_aaa(T, T1, X, T2, right_in_aa(T, T2))
right_in_aa(nil, nil) → right_out_aa(nil, nil)
right_in_aa(node(X11, X12, R), R) → right_out_aa(node(X11, X12, R), R)
U9_aaa(T, T1, X, T2, right_out_aa(T, T2)) → U10_aaa(T, T1, X, T2, value_in_aa(T, X))
value_in_aa(nil, nil) → value_out_aa(nil, nil)
value_in_aa(node(X13, X, X14), X) → value_out_aa(node(X13, X, X14), X)
U10_aaa(T, T1, X, T2, value_out_aa(T, X)) → tappend_out_aaa(T, T1, node(T1, X, T2))
tappend_in_aaa(T, T2, node(T1, X, T2)) → U11_aaa(T, T2, T1, X, left_in_aa(T, T1))
left_in_aa(nil, nil) → left_out_aa(nil, nil)
left_in_aa(node(L, X9, X10), L) → left_out_aa(node(L, X9, X10), L)
U11_aaa(T, T2, T1, X, left_out_aa(T, T1)) → U12_aaa(T, T2, T1, X, right_in_ag(T, nil))
right_in_ag(nil, nil) → right_out_ag(nil, nil)
right_in_ag(node(X11, X12, R), R) → right_out_ag(node(X11, X12, R), R)
U12_aaa(T, T2, T1, X, right_out_ag(T, nil)) → U13_aaa(T, T2, T1, X, value_in_aa(T, X))
U13_aaa(T, T2, T1, X, value_out_aa(T, X)) → tappend_out_aaa(T, T2, node(T1, X, T2))
tappend_in_aaa(T, T3, node(U, X, T2)) → U14_aaa(T, T3, U, X, T2, left_in_aa(T, T1))
U14_aaa(T, T3, U, X, T2, left_out_aa(T, T1)) → U15_aaa(T, T3, U, X, T2, T1, right_in_aa(T, T2))
U15_aaa(T, T3, U, X, T2, T1, right_out_aa(T, T2)) → U16_aaa(T, T3, U, X, T2, T1, value_in_aa(T, X))
U16_aaa(T, T3, U, X, T2, T1, value_out_aa(T, X)) → U17_aaa(T, T3, U, X, T2, tappend_in_aaa(T1, T3, U))
tappend_in_aaa(T, T1, node(T1, X, U)) → U18_aaa(T, T1, X, U, left_in_aa(T, T1))
U18_aaa(T, T1, X, U, left_out_aa(T, T1)) → U19_aaa(T, T1, X, U, right_in_aa(T, T2))
U19_aaa(T, T1, X, U, right_out_aa(T, T2)) → U20_aaa(T, T1, X, U, T2, value_in_aa(T, X))
U20_aaa(T, T1, X, U, T2, value_out_aa(T, X)) → U21_aaa(T, T1, X, U, tappend_in_aaa(T2, T3, U))
U21_aaa(T, T1, X, U, tappend_out_aaa(T2, T3, U)) → tappend_out_aaa(T, T1, node(T1, X, U))
U17_aaa(T, T3, U, X, T2, tappend_out_aaa(T1, T3, U)) → tappend_out_aaa(T, T3, node(U, X, T2))
U3_aaa(L, X, Last, tappend_out_aaa(L, node(nil, X, nil), LX)) → U4_aaa(L, X, Last, tlast_in_aa(Last, LX))
tlast_in_aa(X, node(nil, X, nil)) → tlast_out_aa(X, node(nil, X, nil))
tlast_in_aa(X, node(L, X1, X2)) → U5_aa(X, L, X1, X2, tlast_in_aa(X, L))
tlast_in_aa(X, node(X3, X4, R)) → U6_aa(X, X3, X4, R, tlast_in_aa(X, R))
U6_aa(X, X3, X4, R, tlast_out_aa(X, R)) → tlast_out_aa(X, node(X3, X4, R))
U5_aa(X, L, X1, X2, tlast_out_aa(X, L)) → tlast_out_aa(X, node(L, X1, X2))
U4_aaa(L, X, Last, tlast_out_aa(Last, LX)) → tapplast_out_aaa(L, X, Last)
U2_gaa(A, B, C, tapplast_out_aaa(T, B, C)) → goal_out_gaa(A, B, C)
GOAL_IN_GAA(A, B, C) → U1_GAA(A, B, C, s2t_in_ga(A, T))
GOAL_IN_GAA(A, B, C) → S2T_IN_GA(A, T)
S2T_IN_GA(0, L) → U22_GA(L, eq_in_ag(L, nil))
S2T_IN_GA(0, L) → EQ_IN_AG(L, nil)
S2T_IN_GA(X, node(T, X5, T)) → U23_GA(X, T, X5, p_in_ga(X, P))
S2T_IN_GA(X, node(T, X5, T)) → P_IN_GA(X, P)
U23_GA(X, T, X5, p_out_ga(X, P)) → U24_GA(X, T, X5, s2t_in_ga(P, T))
U23_GA(X, T, X5, p_out_ga(X, P)) → S2T_IN_GA(P, T)
S2T_IN_GA(X, node(nil, X6, T)) → U25_GA(X, X6, T, p_in_ga(X, P))
S2T_IN_GA(X, node(nil, X6, T)) → P_IN_GA(X, P)
U25_GA(X, X6, T, p_out_ga(X, P)) → U26_GA(X, X6, T, s2t_in_ga(P, T))
U25_GA(X, X6, T, p_out_ga(X, P)) → S2T_IN_GA(P, T)
S2T_IN_GA(X, node(T, X7, nil)) → U27_GA(X, T, X7, p_in_ga(X, P))
S2T_IN_GA(X, node(T, X7, nil)) → P_IN_GA(X, P)
U27_GA(X, T, X7, p_out_ga(X, P)) → U28_GA(X, T, X7, s2t_in_ga(P, T))
U27_GA(X, T, X7, p_out_ga(X, P)) → S2T_IN_GA(P, T)
U1_GAA(A, B, C, s2t_out_ga(A, T)) → U2_GAA(A, B, C, tapplast_in_aaa(T, B, C))
U1_GAA(A, B, C, s2t_out_ga(A, T)) → TAPPLAST_IN_AAA(T, B, C)
TAPPLAST_IN_AAA(L, X, Last) → U3_AAA(L, X, Last, tappend_in_aaa(L, node(nil, X, nil), LX))
TAPPLAST_IN_AAA(L, X, Last) → TAPPEND_IN_AAA(L, node(nil, X, nil), LX)
TAPPEND_IN_AAA(nil, Y, Z) → U7_AAA(Y, Z, eq_in_aa(Y, Z))
TAPPEND_IN_AAA(nil, Y, Z) → EQ_IN_AA(Y, Z)
TAPPEND_IN_AAA(T, T1, node(T1, X, T2)) → U8_AAA(T, T1, X, T2, left_in_ag(T, nil))
TAPPEND_IN_AAA(T, T1, node(T1, X, T2)) → LEFT_IN_AG(T, nil)
U8_AAA(T, T1, X, T2, left_out_ag(T, nil)) → U9_AAA(T, T1, X, T2, right_in_aa(T, T2))
U8_AAA(T, T1, X, T2, left_out_ag(T, nil)) → RIGHT_IN_AA(T, T2)
U9_AAA(T, T1, X, T2, right_out_aa(T, T2)) → U10_AAA(T, T1, X, T2, value_in_aa(T, X))
U9_AAA(T, T1, X, T2, right_out_aa(T, T2)) → VALUE_IN_AA(T, X)
TAPPEND_IN_AAA(T, T2, node(T1, X, T2)) → U11_AAA(T, T2, T1, X, left_in_aa(T, T1))
TAPPEND_IN_AAA(T, T2, node(T1, X, T2)) → LEFT_IN_AA(T, T1)
U11_AAA(T, T2, T1, X, left_out_aa(T, T1)) → U12_AAA(T, T2, T1, X, right_in_ag(T, nil))
U11_AAA(T, T2, T1, X, left_out_aa(T, T1)) → RIGHT_IN_AG(T, nil)
U12_AAA(T, T2, T1, X, right_out_ag(T, nil)) → U13_AAA(T, T2, T1, X, value_in_aa(T, X))
U12_AAA(T, T2, T1, X, right_out_ag(T, nil)) → VALUE_IN_AA(T, X)
TAPPEND_IN_AAA(T, T3, node(U, X, T2)) → U14_AAA(T, T3, U, X, T2, left_in_aa(T, T1))
TAPPEND_IN_AAA(T, T3, node(U, X, T2)) → LEFT_IN_AA(T, T1)
U14_AAA(T, T3, U, X, T2, left_out_aa(T, T1)) → U15_AAA(T, T3, U, X, T2, T1, right_in_aa(T, T2))
U14_AAA(T, T3, U, X, T2, left_out_aa(T, T1)) → RIGHT_IN_AA(T, T2)
U15_AAA(T, T3, U, X, T2, T1, right_out_aa(T, T2)) → U16_AAA(T, T3, U, X, T2, T1, value_in_aa(T, X))
U15_AAA(T, T3, U, X, T2, T1, right_out_aa(T, T2)) → VALUE_IN_AA(T, X)
U16_AAA(T, T3, U, X, T2, T1, value_out_aa(T, X)) → U17_AAA(T, T3, U, X, T2, tappend_in_aaa(T1, T3, U))
U16_AAA(T, T3, U, X, T2, T1, value_out_aa(T, X)) → TAPPEND_IN_AAA(T1, T3, U)
TAPPEND_IN_AAA(T, T1, node(T1, X, U)) → U18_AAA(T, T1, X, U, left_in_aa(T, T1))
TAPPEND_IN_AAA(T, T1, node(T1, X, U)) → LEFT_IN_AA(T, T1)
U18_AAA(T, T1, X, U, left_out_aa(T, T1)) → U19_AAA(T, T1, X, U, right_in_aa(T, T2))
U18_AAA(T, T1, X, U, left_out_aa(T, T1)) → RIGHT_IN_AA(T, T2)
U19_AAA(T, T1, X, U, right_out_aa(T, T2)) → U20_AAA(T, T1, X, U, T2, value_in_aa(T, X))
U19_AAA(T, T1, X, U, right_out_aa(T, T2)) → VALUE_IN_AA(T, X)
U20_AAA(T, T1, X, U, T2, value_out_aa(T, X)) → U21_AAA(T, T1, X, U, tappend_in_aaa(T2, T3, U))
U20_AAA(T, T1, X, U, T2, value_out_aa(T, X)) → TAPPEND_IN_AAA(T2, T3, U)
U3_AAA(L, X, Last, tappend_out_aaa(L, node(nil, X, nil), LX)) → U4_AAA(L, X, Last, tlast_in_aa(Last, LX))
U3_AAA(L, X, Last, tappend_out_aaa(L, node(nil, X, nil), LX)) → TLAST_IN_AA(Last, LX)
TLAST_IN_AA(X, node(L, X1, X2)) → U5_AA(X, L, X1, X2, tlast_in_aa(X, L))
TLAST_IN_AA(X, node(L, X1, X2)) → TLAST_IN_AA(X, L)
TLAST_IN_AA(X, node(X3, X4, R)) → U6_AA(X, X3, X4, R, tlast_in_aa(X, R))
TLAST_IN_AA(X, node(X3, X4, R)) → TLAST_IN_AA(X, R)
goal_in_gaa(A, B, C) → U1_gaa(A, B, C, s2t_in_ga(A, T))
s2t_in_ga(0, L) → U22_ga(L, eq_in_ag(L, nil))
eq_in_ag(X, X) → eq_out_ag(X, X)
U22_ga(L, eq_out_ag(L, nil)) → s2t_out_ga(0, L)
s2t_in_ga(X, node(T, X5, T)) → U23_ga(X, T, X5, p_in_ga(X, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U23_ga(X, T, X5, p_out_ga(X, P)) → U24_ga(X, T, X5, s2t_in_ga(P, T))
s2t_in_ga(X, node(nil, X6, T)) → U25_ga(X, X6, T, p_in_ga(X, P))
U25_ga(X, X6, T, p_out_ga(X, P)) → U26_ga(X, X6, T, s2t_in_ga(P, T))
s2t_in_ga(X, node(T, X7, nil)) → U27_ga(X, T, X7, p_in_ga(X, P))
U27_ga(X, T, X7, p_out_ga(X, P)) → U28_ga(X, T, X7, s2t_in_ga(P, T))
s2t_in_ga(X, node(nil, X8, nil)) → s2t_out_ga(X, node(nil, X8, nil))
U28_ga(X, T, X7, s2t_out_ga(P, T)) → s2t_out_ga(X, node(T, X7, nil))
U26_ga(X, X6, T, s2t_out_ga(P, T)) → s2t_out_ga(X, node(nil, X6, T))
U24_ga(X, T, X5, s2t_out_ga(P, T)) → s2t_out_ga(X, node(T, X5, T))
U1_gaa(A, B, C, s2t_out_ga(A, T)) → U2_gaa(A, B, C, tapplast_in_aaa(T, B, C))
tapplast_in_aaa(L, X, Last) → U3_aaa(L, X, Last, tappend_in_aaa(L, node(nil, X, nil), LX))
tappend_in_aaa(nil, Y, Z) → U7_aaa(Y, Z, eq_in_aa(Y, Z))
eq_in_aa(X, X) → eq_out_aa(X, X)
U7_aaa(Y, Z, eq_out_aa(Y, Z)) → tappend_out_aaa(nil, Y, Z)
tappend_in_aaa(T, T1, node(T1, X, T2)) → U8_aaa(T, T1, X, T2, left_in_ag(T, nil))
left_in_ag(nil, nil) → left_out_ag(nil, nil)
left_in_ag(node(L, X9, X10), L) → left_out_ag(node(L, X9, X10), L)
U8_aaa(T, T1, X, T2, left_out_ag(T, nil)) → U9_aaa(T, T1, X, T2, right_in_aa(T, T2))
right_in_aa(nil, nil) → right_out_aa(nil, nil)
right_in_aa(node(X11, X12, R), R) → right_out_aa(node(X11, X12, R), R)
U9_aaa(T, T1, X, T2, right_out_aa(T, T2)) → U10_aaa(T, T1, X, T2, value_in_aa(T, X))
value_in_aa(nil, nil) → value_out_aa(nil, nil)
value_in_aa(node(X13, X, X14), X) → value_out_aa(node(X13, X, X14), X)
U10_aaa(T, T1, X, T2, value_out_aa(T, X)) → tappend_out_aaa(T, T1, node(T1, X, T2))
tappend_in_aaa(T, T2, node(T1, X, T2)) → U11_aaa(T, T2, T1, X, left_in_aa(T, T1))
left_in_aa(nil, nil) → left_out_aa(nil, nil)
left_in_aa(node(L, X9, X10), L) → left_out_aa(node(L, X9, X10), L)
U11_aaa(T, T2, T1, X, left_out_aa(T, T1)) → U12_aaa(T, T2, T1, X, right_in_ag(T, nil))
right_in_ag(nil, nil) → right_out_ag(nil, nil)
right_in_ag(node(X11, X12, R), R) → right_out_ag(node(X11, X12, R), R)
U12_aaa(T, T2, T1, X, right_out_ag(T, nil)) → U13_aaa(T, T2, T1, X, value_in_aa(T, X))
U13_aaa(T, T2, T1, X, value_out_aa(T, X)) → tappend_out_aaa(T, T2, node(T1, X, T2))
tappend_in_aaa(T, T3, node(U, X, T2)) → U14_aaa(T, T3, U, X, T2, left_in_aa(T, T1))
U14_aaa(T, T3, U, X, T2, left_out_aa(T, T1)) → U15_aaa(T, T3, U, X, T2, T1, right_in_aa(T, T2))
U15_aaa(T, T3, U, X, T2, T1, right_out_aa(T, T2)) → U16_aaa(T, T3, U, X, T2, T1, value_in_aa(T, X))
U16_aaa(T, T3, U, X, T2, T1, value_out_aa(T, X)) → U17_aaa(T, T3, U, X, T2, tappend_in_aaa(T1, T3, U))
tappend_in_aaa(T, T1, node(T1, X, U)) → U18_aaa(T, T1, X, U, left_in_aa(T, T1))
U18_aaa(T, T1, X, U, left_out_aa(T, T1)) → U19_aaa(T, T1, X, U, right_in_aa(T, T2))
U19_aaa(T, T1, X, U, right_out_aa(T, T2)) → U20_aaa(T, T1, X, U, T2, value_in_aa(T, X))
U20_aaa(T, T1, X, U, T2, value_out_aa(T, X)) → U21_aaa(T, T1, X, U, tappend_in_aaa(T2, T3, U))
U21_aaa(T, T1, X, U, tappend_out_aaa(T2, T3, U)) → tappend_out_aaa(T, T1, node(T1, X, U))
U17_aaa(T, T3, U, X, T2, tappend_out_aaa(T1, T3, U)) → tappend_out_aaa(T, T3, node(U, X, T2))
U3_aaa(L, X, Last, tappend_out_aaa(L, node(nil, X, nil), LX)) → U4_aaa(L, X, Last, tlast_in_aa(Last, LX))
tlast_in_aa(X, node(nil, X, nil)) → tlast_out_aa(X, node(nil, X, nil))
tlast_in_aa(X, node(L, X1, X2)) → U5_aa(X, L, X1, X2, tlast_in_aa(X, L))
tlast_in_aa(X, node(X3, X4, R)) → U6_aa(X, X3, X4, R, tlast_in_aa(X, R))
U6_aa(X, X3, X4, R, tlast_out_aa(X, R)) → tlast_out_aa(X, node(X3, X4, R))
U5_aa(X, L, X1, X2, tlast_out_aa(X, L)) → tlast_out_aa(X, node(L, X1, X2))
U4_aaa(L, X, Last, tlast_out_aa(Last, LX)) → tapplast_out_aaa(L, X, Last)
U2_gaa(A, B, C, tapplast_out_aaa(T, B, C)) → goal_out_gaa(A, B, C)
GOAL_IN_GAA(A, B, C) → U1_GAA(A, B, C, s2t_in_ga(A, T))
GOAL_IN_GAA(A, B, C) → S2T_IN_GA(A, T)
S2T_IN_GA(0, L) → U22_GA(L, eq_in_ag(L, nil))
S2T_IN_GA(0, L) → EQ_IN_AG(L, nil)
S2T_IN_GA(X, node(T, X5, T)) → U23_GA(X, T, X5, p_in_ga(X, P))
S2T_IN_GA(X, node(T, X5, T)) → P_IN_GA(X, P)
U23_GA(X, T, X5, p_out_ga(X, P)) → U24_GA(X, T, X5, s2t_in_ga(P, T))
U23_GA(X, T, X5, p_out_ga(X, P)) → S2T_IN_GA(P, T)
S2T_IN_GA(X, node(nil, X6, T)) → U25_GA(X, X6, T, p_in_ga(X, P))
S2T_IN_GA(X, node(nil, X6, T)) → P_IN_GA(X, P)
U25_GA(X, X6, T, p_out_ga(X, P)) → U26_GA(X, X6, T, s2t_in_ga(P, T))
U25_GA(X, X6, T, p_out_ga(X, P)) → S2T_IN_GA(P, T)
S2T_IN_GA(X, node(T, X7, nil)) → U27_GA(X, T, X7, p_in_ga(X, P))
S2T_IN_GA(X, node(T, X7, nil)) → P_IN_GA(X, P)
U27_GA(X, T, X7, p_out_ga(X, P)) → U28_GA(X, T, X7, s2t_in_ga(P, T))
U27_GA(X, T, X7, p_out_ga(X, P)) → S2T_IN_GA(P, T)
U1_GAA(A, B, C, s2t_out_ga(A, T)) → U2_GAA(A, B, C, tapplast_in_aaa(T, B, C))
U1_GAA(A, B, C, s2t_out_ga(A, T)) → TAPPLAST_IN_AAA(T, B, C)
TAPPLAST_IN_AAA(L, X, Last) → U3_AAA(L, X, Last, tappend_in_aaa(L, node(nil, X, nil), LX))
TAPPLAST_IN_AAA(L, X, Last) → TAPPEND_IN_AAA(L, node(nil, X, nil), LX)
TAPPEND_IN_AAA(nil, Y, Z) → U7_AAA(Y, Z, eq_in_aa(Y, Z))
TAPPEND_IN_AAA(nil, Y, Z) → EQ_IN_AA(Y, Z)
TAPPEND_IN_AAA(T, T1, node(T1, X, T2)) → U8_AAA(T, T1, X, T2, left_in_ag(T, nil))
TAPPEND_IN_AAA(T, T1, node(T1, X, T2)) → LEFT_IN_AG(T, nil)
U8_AAA(T, T1, X, T2, left_out_ag(T, nil)) → U9_AAA(T, T1, X, T2, right_in_aa(T, T2))
U8_AAA(T, T1, X, T2, left_out_ag(T, nil)) → RIGHT_IN_AA(T, T2)
U9_AAA(T, T1, X, T2, right_out_aa(T, T2)) → U10_AAA(T, T1, X, T2, value_in_aa(T, X))
U9_AAA(T, T1, X, T2, right_out_aa(T, T2)) → VALUE_IN_AA(T, X)
TAPPEND_IN_AAA(T, T2, node(T1, X, T2)) → U11_AAA(T, T2, T1, X, left_in_aa(T, T1))
TAPPEND_IN_AAA(T, T2, node(T1, X, T2)) → LEFT_IN_AA(T, T1)
U11_AAA(T, T2, T1, X, left_out_aa(T, T1)) → U12_AAA(T, T2, T1, X, right_in_ag(T, nil))
U11_AAA(T, T2, T1, X, left_out_aa(T, T1)) → RIGHT_IN_AG(T, nil)
U12_AAA(T, T2, T1, X, right_out_ag(T, nil)) → U13_AAA(T, T2, T1, X, value_in_aa(T, X))
U12_AAA(T, T2, T1, X, right_out_ag(T, nil)) → VALUE_IN_AA(T, X)
TAPPEND_IN_AAA(T, T3, node(U, X, T2)) → U14_AAA(T, T3, U, X, T2, left_in_aa(T, T1))
TAPPEND_IN_AAA(T, T3, node(U, X, T2)) → LEFT_IN_AA(T, T1)
U14_AAA(T, T3, U, X, T2, left_out_aa(T, T1)) → U15_AAA(T, T3, U, X, T2, T1, right_in_aa(T, T2))
U14_AAA(T, T3, U, X, T2, left_out_aa(T, T1)) → RIGHT_IN_AA(T, T2)
U15_AAA(T, T3, U, X, T2, T1, right_out_aa(T, T2)) → U16_AAA(T, T3, U, X, T2, T1, value_in_aa(T, X))
U15_AAA(T, T3, U, X, T2, T1, right_out_aa(T, T2)) → VALUE_IN_AA(T, X)
U16_AAA(T, T3, U, X, T2, T1, value_out_aa(T, X)) → U17_AAA(T, T3, U, X, T2, tappend_in_aaa(T1, T3, U))
U16_AAA(T, T3, U, X, T2, T1, value_out_aa(T, X)) → TAPPEND_IN_AAA(T1, T3, U)
TAPPEND_IN_AAA(T, T1, node(T1, X, U)) → U18_AAA(T, T1, X, U, left_in_aa(T, T1))
TAPPEND_IN_AAA(T, T1, node(T1, X, U)) → LEFT_IN_AA(T, T1)
U18_AAA(T, T1, X, U, left_out_aa(T, T1)) → U19_AAA(T, T1, X, U, right_in_aa(T, T2))
U18_AAA(T, T1, X, U, left_out_aa(T, T1)) → RIGHT_IN_AA(T, T2)
U19_AAA(T, T1, X, U, right_out_aa(T, T2)) → U20_AAA(T, T1, X, U, T2, value_in_aa(T, X))
U19_AAA(T, T1, X, U, right_out_aa(T, T2)) → VALUE_IN_AA(T, X)
U20_AAA(T, T1, X, U, T2, value_out_aa(T, X)) → U21_AAA(T, T1, X, U, tappend_in_aaa(T2, T3, U))
U20_AAA(T, T1, X, U, T2, value_out_aa(T, X)) → TAPPEND_IN_AAA(T2, T3, U)
U3_AAA(L, X, Last, tappend_out_aaa(L, node(nil, X, nil), LX)) → U4_AAA(L, X, Last, tlast_in_aa(Last, LX))
U3_AAA(L, X, Last, tappend_out_aaa(L, node(nil, X, nil), LX)) → TLAST_IN_AA(Last, LX)
TLAST_IN_AA(X, node(L, X1, X2)) → U5_AA(X, L, X1, X2, tlast_in_aa(X, L))
TLAST_IN_AA(X, node(L, X1, X2)) → TLAST_IN_AA(X, L)
TLAST_IN_AA(X, node(X3, X4, R)) → U6_AA(X, X3, X4, R, tlast_in_aa(X, R))
TLAST_IN_AA(X, node(X3, X4, R)) → TLAST_IN_AA(X, R)
goal_in_gaa(A, B, C) → U1_gaa(A, B, C, s2t_in_ga(A, T))
s2t_in_ga(0, L) → U22_ga(L, eq_in_ag(L, nil))
eq_in_ag(X, X) → eq_out_ag(X, X)
U22_ga(L, eq_out_ag(L, nil)) → s2t_out_ga(0, L)
s2t_in_ga(X, node(T, X5, T)) → U23_ga(X, T, X5, p_in_ga(X, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U23_ga(X, T, X5, p_out_ga(X, P)) → U24_ga(X, T, X5, s2t_in_ga(P, T))
s2t_in_ga(X, node(nil, X6, T)) → U25_ga(X, X6, T, p_in_ga(X, P))
U25_ga(X, X6, T, p_out_ga(X, P)) → U26_ga(X, X6, T, s2t_in_ga(P, T))
s2t_in_ga(X, node(T, X7, nil)) → U27_ga(X, T, X7, p_in_ga(X, P))
U27_ga(X, T, X7, p_out_ga(X, P)) → U28_ga(X, T, X7, s2t_in_ga(P, T))
s2t_in_ga(X, node(nil, X8, nil)) → s2t_out_ga(X, node(nil, X8, nil))
U28_ga(X, T, X7, s2t_out_ga(P, T)) → s2t_out_ga(X, node(T, X7, nil))
U26_ga(X, X6, T, s2t_out_ga(P, T)) → s2t_out_ga(X, node(nil, X6, T))
U24_ga(X, T, X5, s2t_out_ga(P, T)) → s2t_out_ga(X, node(T, X5, T))
U1_gaa(A, B, C, s2t_out_ga(A, T)) → U2_gaa(A, B, C, tapplast_in_aaa(T, B, C))
tapplast_in_aaa(L, X, Last) → U3_aaa(L, X, Last, tappend_in_aaa(L, node(nil, X, nil), LX))
tappend_in_aaa(nil, Y, Z) → U7_aaa(Y, Z, eq_in_aa(Y, Z))
eq_in_aa(X, X) → eq_out_aa(X, X)
U7_aaa(Y, Z, eq_out_aa(Y, Z)) → tappend_out_aaa(nil, Y, Z)
tappend_in_aaa(T, T1, node(T1, X, T2)) → U8_aaa(T, T1, X, T2, left_in_ag(T, nil))
left_in_ag(nil, nil) → left_out_ag(nil, nil)
left_in_ag(node(L, X9, X10), L) → left_out_ag(node(L, X9, X10), L)
U8_aaa(T, T1, X, T2, left_out_ag(T, nil)) → U9_aaa(T, T1, X, T2, right_in_aa(T, T2))
right_in_aa(nil, nil) → right_out_aa(nil, nil)
right_in_aa(node(X11, X12, R), R) → right_out_aa(node(X11, X12, R), R)
U9_aaa(T, T1, X, T2, right_out_aa(T, T2)) → U10_aaa(T, T1, X, T2, value_in_aa(T, X))
value_in_aa(nil, nil) → value_out_aa(nil, nil)
value_in_aa(node(X13, X, X14), X) → value_out_aa(node(X13, X, X14), X)
U10_aaa(T, T1, X, T2, value_out_aa(T, X)) → tappend_out_aaa(T, T1, node(T1, X, T2))
tappend_in_aaa(T, T2, node(T1, X, T2)) → U11_aaa(T, T2, T1, X, left_in_aa(T, T1))
left_in_aa(nil, nil) → left_out_aa(nil, nil)
left_in_aa(node(L, X9, X10), L) → left_out_aa(node(L, X9, X10), L)
U11_aaa(T, T2, T1, X, left_out_aa(T, T1)) → U12_aaa(T, T2, T1, X, right_in_ag(T, nil))
right_in_ag(nil, nil) → right_out_ag(nil, nil)
right_in_ag(node(X11, X12, R), R) → right_out_ag(node(X11, X12, R), R)
U12_aaa(T, T2, T1, X, right_out_ag(T, nil)) → U13_aaa(T, T2, T1, X, value_in_aa(T, X))
U13_aaa(T, T2, T1, X, value_out_aa(T, X)) → tappend_out_aaa(T, T2, node(T1, X, T2))
tappend_in_aaa(T, T3, node(U, X, T2)) → U14_aaa(T, T3, U, X, T2, left_in_aa(T, T1))
U14_aaa(T, T3, U, X, T2, left_out_aa(T, T1)) → U15_aaa(T, T3, U, X, T2, T1, right_in_aa(T, T2))
U15_aaa(T, T3, U, X, T2, T1, right_out_aa(T, T2)) → U16_aaa(T, T3, U, X, T2, T1, value_in_aa(T, X))
U16_aaa(T, T3, U, X, T2, T1, value_out_aa(T, X)) → U17_aaa(T, T3, U, X, T2, tappend_in_aaa(T1, T3, U))
tappend_in_aaa(T, T1, node(T1, X, U)) → U18_aaa(T, T1, X, U, left_in_aa(T, T1))
U18_aaa(T, T1, X, U, left_out_aa(T, T1)) → U19_aaa(T, T1, X, U, right_in_aa(T, T2))
U19_aaa(T, T1, X, U, right_out_aa(T, T2)) → U20_aaa(T, T1, X, U, T2, value_in_aa(T, X))
U20_aaa(T, T1, X, U, T2, value_out_aa(T, X)) → U21_aaa(T, T1, X, U, tappend_in_aaa(T2, T3, U))
U21_aaa(T, T1, X, U, tappend_out_aaa(T2, T3, U)) → tappend_out_aaa(T, T1, node(T1, X, U))
U17_aaa(T, T3, U, X, T2, tappend_out_aaa(T1, T3, U)) → tappend_out_aaa(T, T3, node(U, X, T2))
U3_aaa(L, X, Last, tappend_out_aaa(L, node(nil, X, nil), LX)) → U4_aaa(L, X, Last, tlast_in_aa(Last, LX))
tlast_in_aa(X, node(nil, X, nil)) → tlast_out_aa(X, node(nil, X, nil))
tlast_in_aa(X, node(L, X1, X2)) → U5_aa(X, L, X1, X2, tlast_in_aa(X, L))
tlast_in_aa(X, node(X3, X4, R)) → U6_aa(X, X3, X4, R, tlast_in_aa(X, R))
U6_aa(X, X3, X4, R, tlast_out_aa(X, R)) → tlast_out_aa(X, node(X3, X4, R))
U5_aa(X, L, X1, X2, tlast_out_aa(X, L)) → tlast_out_aa(X, node(L, X1, X2))
U4_aaa(L, X, Last, tlast_out_aa(Last, LX)) → tapplast_out_aaa(L, X, Last)
U2_gaa(A, B, C, tapplast_out_aaa(T, B, C)) → goal_out_gaa(A, B, C)
TLAST_IN_AA(X, node(X3, X4, R)) → TLAST_IN_AA(X, R)
TLAST_IN_AA(X, node(L, X1, X2)) → TLAST_IN_AA(X, L)
goal_in_gaa(A, B, C) → U1_gaa(A, B, C, s2t_in_ga(A, T))
s2t_in_ga(0, L) → U22_ga(L, eq_in_ag(L, nil))
eq_in_ag(X, X) → eq_out_ag(X, X)
U22_ga(L, eq_out_ag(L, nil)) → s2t_out_ga(0, L)
s2t_in_ga(X, node(T, X5, T)) → U23_ga(X, T, X5, p_in_ga(X, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U23_ga(X, T, X5, p_out_ga(X, P)) → U24_ga(X, T, X5, s2t_in_ga(P, T))
s2t_in_ga(X, node(nil, X6, T)) → U25_ga(X, X6, T, p_in_ga(X, P))
U25_ga(X, X6, T, p_out_ga(X, P)) → U26_ga(X, X6, T, s2t_in_ga(P, T))
s2t_in_ga(X, node(T, X7, nil)) → U27_ga(X, T, X7, p_in_ga(X, P))
U27_ga(X, T, X7, p_out_ga(X, P)) → U28_ga(X, T, X7, s2t_in_ga(P, T))
s2t_in_ga(X, node(nil, X8, nil)) → s2t_out_ga(X, node(nil, X8, nil))
U28_ga(X, T, X7, s2t_out_ga(P, T)) → s2t_out_ga(X, node(T, X7, nil))
U26_ga(X, X6, T, s2t_out_ga(P, T)) → s2t_out_ga(X, node(nil, X6, T))
U24_ga(X, T, X5, s2t_out_ga(P, T)) → s2t_out_ga(X, node(T, X5, T))
U1_gaa(A, B, C, s2t_out_ga(A, T)) → U2_gaa(A, B, C, tapplast_in_aaa(T, B, C))
tapplast_in_aaa(L, X, Last) → U3_aaa(L, X, Last, tappend_in_aaa(L, node(nil, X, nil), LX))
tappend_in_aaa(nil, Y, Z) → U7_aaa(Y, Z, eq_in_aa(Y, Z))
eq_in_aa(X, X) → eq_out_aa(X, X)
U7_aaa(Y, Z, eq_out_aa(Y, Z)) → tappend_out_aaa(nil, Y, Z)
tappend_in_aaa(T, T1, node(T1, X, T2)) → U8_aaa(T, T1, X, T2, left_in_ag(T, nil))
left_in_ag(nil, nil) → left_out_ag(nil, nil)
left_in_ag(node(L, X9, X10), L) → left_out_ag(node(L, X9, X10), L)
U8_aaa(T, T1, X, T2, left_out_ag(T, nil)) → U9_aaa(T, T1, X, T2, right_in_aa(T, T2))
right_in_aa(nil, nil) → right_out_aa(nil, nil)
right_in_aa(node(X11, X12, R), R) → right_out_aa(node(X11, X12, R), R)
U9_aaa(T, T1, X, T2, right_out_aa(T, T2)) → U10_aaa(T, T1, X, T2, value_in_aa(T, X))
value_in_aa(nil, nil) → value_out_aa(nil, nil)
value_in_aa(node(X13, X, X14), X) → value_out_aa(node(X13, X, X14), X)
U10_aaa(T, T1, X, T2, value_out_aa(T, X)) → tappend_out_aaa(T, T1, node(T1, X, T2))
tappend_in_aaa(T, T2, node(T1, X, T2)) → U11_aaa(T, T2, T1, X, left_in_aa(T, T1))
left_in_aa(nil, nil) → left_out_aa(nil, nil)
left_in_aa(node(L, X9, X10), L) → left_out_aa(node(L, X9, X10), L)
U11_aaa(T, T2, T1, X, left_out_aa(T, T1)) → U12_aaa(T, T2, T1, X, right_in_ag(T, nil))
right_in_ag(nil, nil) → right_out_ag(nil, nil)
right_in_ag(node(X11, X12, R), R) → right_out_ag(node(X11, X12, R), R)
U12_aaa(T, T2, T1, X, right_out_ag(T, nil)) → U13_aaa(T, T2, T1, X, value_in_aa(T, X))
U13_aaa(T, T2, T1, X, value_out_aa(T, X)) → tappend_out_aaa(T, T2, node(T1, X, T2))
tappend_in_aaa(T, T3, node(U, X, T2)) → U14_aaa(T, T3, U, X, T2, left_in_aa(T, T1))
U14_aaa(T, T3, U, X, T2, left_out_aa(T, T1)) → U15_aaa(T, T3, U, X, T2, T1, right_in_aa(T, T2))
U15_aaa(T, T3, U, X, T2, T1, right_out_aa(T, T2)) → U16_aaa(T, T3, U, X, T2, T1, value_in_aa(T, X))
U16_aaa(T, T3, U, X, T2, T1, value_out_aa(T, X)) → U17_aaa(T, T3, U, X, T2, tappend_in_aaa(T1, T3, U))
tappend_in_aaa(T, T1, node(T1, X, U)) → U18_aaa(T, T1, X, U, left_in_aa(T, T1))
U18_aaa(T, T1, X, U, left_out_aa(T, T1)) → U19_aaa(T, T1, X, U, right_in_aa(T, T2))
U19_aaa(T, T1, X, U, right_out_aa(T, T2)) → U20_aaa(T, T1, X, U, T2, value_in_aa(T, X))
U20_aaa(T, T1, X, U, T2, value_out_aa(T, X)) → U21_aaa(T, T1, X, U, tappend_in_aaa(T2, T3, U))
U21_aaa(T, T1, X, U, tappend_out_aaa(T2, T3, U)) → tappend_out_aaa(T, T1, node(T1, X, U))
U17_aaa(T, T3, U, X, T2, tappend_out_aaa(T1, T3, U)) → tappend_out_aaa(T, T3, node(U, X, T2))
U3_aaa(L, X, Last, tappend_out_aaa(L, node(nil, X, nil), LX)) → U4_aaa(L, X, Last, tlast_in_aa(Last, LX))
tlast_in_aa(X, node(nil, X, nil)) → tlast_out_aa(X, node(nil, X, nil))
tlast_in_aa(X, node(L, X1, X2)) → U5_aa(X, L, X1, X2, tlast_in_aa(X, L))
tlast_in_aa(X, node(X3, X4, R)) → U6_aa(X, X3, X4, R, tlast_in_aa(X, R))
U6_aa(X, X3, X4, R, tlast_out_aa(X, R)) → tlast_out_aa(X, node(X3, X4, R))
U5_aa(X, L, X1, X2, tlast_out_aa(X, L)) → tlast_out_aa(X, node(L, X1, X2))
U4_aaa(L, X, Last, tlast_out_aa(Last, LX)) → tapplast_out_aaa(L, X, Last)
U2_gaa(A, B, C, tapplast_out_aaa(T, B, C)) → goal_out_gaa(A, B, C)
TLAST_IN_AA(X, node(X3, X4, R)) → TLAST_IN_AA(X, R)
TLAST_IN_AA(X, node(L, X1, X2)) → TLAST_IN_AA(X, L)
TLAST_IN_AA → TLAST_IN_AA
TAPPEND_IN_AAA(T, T3, node(U, X, T2)) → U14_AAA(T, T3, U, X, T2, left_in_aa(T, T1))
U14_AAA(T, T3, U, X, T2, left_out_aa(T, T1)) → U15_AAA(T, T3, U, X, T2, T1, right_in_aa(T, T2))
U15_AAA(T, T3, U, X, T2, T1, right_out_aa(T, T2)) → U16_AAA(T, T3, U, X, T2, T1, value_in_aa(T, X))
U16_AAA(T, T3, U, X, T2, T1, value_out_aa(T, X)) → TAPPEND_IN_AAA(T1, T3, U)
TAPPEND_IN_AAA(T, T1, node(T1, X, U)) → U18_AAA(T, T1, X, U, left_in_aa(T, T1))
U18_AAA(T, T1, X, U, left_out_aa(T, T1)) → U19_AAA(T, T1, X, U, right_in_aa(T, T2))
U19_AAA(T, T1, X, U, right_out_aa(T, T2)) → U20_AAA(T, T1, X, U, T2, value_in_aa(T, X))
U20_AAA(T, T1, X, U, T2, value_out_aa(T, X)) → TAPPEND_IN_AAA(T2, T3, U)
goal_in_gaa(A, B, C) → U1_gaa(A, B, C, s2t_in_ga(A, T))
s2t_in_ga(0, L) → U22_ga(L, eq_in_ag(L, nil))
eq_in_ag(X, X) → eq_out_ag(X, X)
U22_ga(L, eq_out_ag(L, nil)) → s2t_out_ga(0, L)
s2t_in_ga(X, node(T, X5, T)) → U23_ga(X, T, X5, p_in_ga(X, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U23_ga(X, T, X5, p_out_ga(X, P)) → U24_ga(X, T, X5, s2t_in_ga(P, T))
s2t_in_ga(X, node(nil, X6, T)) → U25_ga(X, X6, T, p_in_ga(X, P))
U25_ga(X, X6, T, p_out_ga(X, P)) → U26_ga(X, X6, T, s2t_in_ga(P, T))
s2t_in_ga(X, node(T, X7, nil)) → U27_ga(X, T, X7, p_in_ga(X, P))
U27_ga(X, T, X7, p_out_ga(X, P)) → U28_ga(X, T, X7, s2t_in_ga(P, T))
s2t_in_ga(X, node(nil, X8, nil)) → s2t_out_ga(X, node(nil, X8, nil))
U28_ga(X, T, X7, s2t_out_ga(P, T)) → s2t_out_ga(X, node(T, X7, nil))
U26_ga(X, X6, T, s2t_out_ga(P, T)) → s2t_out_ga(X, node(nil, X6, T))
U24_ga(X, T, X5, s2t_out_ga(P, T)) → s2t_out_ga(X, node(T, X5, T))
U1_gaa(A, B, C, s2t_out_ga(A, T)) → U2_gaa(A, B, C, tapplast_in_aaa(T, B, C))
tapplast_in_aaa(L, X, Last) → U3_aaa(L, X, Last, tappend_in_aaa(L, node(nil, X, nil), LX))
tappend_in_aaa(nil, Y, Z) → U7_aaa(Y, Z, eq_in_aa(Y, Z))
eq_in_aa(X, X) → eq_out_aa(X, X)
U7_aaa(Y, Z, eq_out_aa(Y, Z)) → tappend_out_aaa(nil, Y, Z)
tappend_in_aaa(T, T1, node(T1, X, T2)) → U8_aaa(T, T1, X, T2, left_in_ag(T, nil))
left_in_ag(nil, nil) → left_out_ag(nil, nil)
left_in_ag(node(L, X9, X10), L) → left_out_ag(node(L, X9, X10), L)
U8_aaa(T, T1, X, T2, left_out_ag(T, nil)) → U9_aaa(T, T1, X, T2, right_in_aa(T, T2))
right_in_aa(nil, nil) → right_out_aa(nil, nil)
right_in_aa(node(X11, X12, R), R) → right_out_aa(node(X11, X12, R), R)
U9_aaa(T, T1, X, T2, right_out_aa(T, T2)) → U10_aaa(T, T1, X, T2, value_in_aa(T, X))
value_in_aa(nil, nil) → value_out_aa(nil, nil)
value_in_aa(node(X13, X, X14), X) → value_out_aa(node(X13, X, X14), X)
U10_aaa(T, T1, X, T2, value_out_aa(T, X)) → tappend_out_aaa(T, T1, node(T1, X, T2))
tappend_in_aaa(T, T2, node(T1, X, T2)) → U11_aaa(T, T2, T1, X, left_in_aa(T, T1))
left_in_aa(nil, nil) → left_out_aa(nil, nil)
left_in_aa(node(L, X9, X10), L) → left_out_aa(node(L, X9, X10), L)
U11_aaa(T, T2, T1, X, left_out_aa(T, T1)) → U12_aaa(T, T2, T1, X, right_in_ag(T, nil))
right_in_ag(nil, nil) → right_out_ag(nil, nil)
right_in_ag(node(X11, X12, R), R) → right_out_ag(node(X11, X12, R), R)
U12_aaa(T, T2, T1, X, right_out_ag(T, nil)) → U13_aaa(T, T2, T1, X, value_in_aa(T, X))
U13_aaa(T, T2, T1, X, value_out_aa(T, X)) → tappend_out_aaa(T, T2, node(T1, X, T2))
tappend_in_aaa(T, T3, node(U, X, T2)) → U14_aaa(T, T3, U, X, T2, left_in_aa(T, T1))
U14_aaa(T, T3, U, X, T2, left_out_aa(T, T1)) → U15_aaa(T, T3, U, X, T2, T1, right_in_aa(T, T2))
U15_aaa(T, T3, U, X, T2, T1, right_out_aa(T, T2)) → U16_aaa(T, T3, U, X, T2, T1, value_in_aa(T, X))
U16_aaa(T, T3, U, X, T2, T1, value_out_aa(T, X)) → U17_aaa(T, T3, U, X, T2, tappend_in_aaa(T1, T3, U))
tappend_in_aaa(T, T1, node(T1, X, U)) → U18_aaa(T, T1, X, U, left_in_aa(T, T1))
U18_aaa(T, T1, X, U, left_out_aa(T, T1)) → U19_aaa(T, T1, X, U, right_in_aa(T, T2))
U19_aaa(T, T1, X, U, right_out_aa(T, T2)) → U20_aaa(T, T1, X, U, T2, value_in_aa(T, X))
U20_aaa(T, T1, X, U, T2, value_out_aa(T, X)) → U21_aaa(T, T1, X, U, tappend_in_aaa(T2, T3, U))
U21_aaa(T, T1, X, U, tappend_out_aaa(T2, T3, U)) → tappend_out_aaa(T, T1, node(T1, X, U))
U17_aaa(T, T3, U, X, T2, tappend_out_aaa(T1, T3, U)) → tappend_out_aaa(T, T3, node(U, X, T2))
U3_aaa(L, X, Last, tappend_out_aaa(L, node(nil, X, nil), LX)) → U4_aaa(L, X, Last, tlast_in_aa(Last, LX))
tlast_in_aa(X, node(nil, X, nil)) → tlast_out_aa(X, node(nil, X, nil))
tlast_in_aa(X, node(L, X1, X2)) → U5_aa(X, L, X1, X2, tlast_in_aa(X, L))
tlast_in_aa(X, node(X3, X4, R)) → U6_aa(X, X3, X4, R, tlast_in_aa(X, R))
U6_aa(X, X3, X4, R, tlast_out_aa(X, R)) → tlast_out_aa(X, node(X3, X4, R))
U5_aa(X, L, X1, X2, tlast_out_aa(X, L)) → tlast_out_aa(X, node(L, X1, X2))
U4_aaa(L, X, Last, tlast_out_aa(Last, LX)) → tapplast_out_aaa(L, X, Last)
U2_gaa(A, B, C, tapplast_out_aaa(T, B, C)) → goal_out_gaa(A, B, C)
TAPPEND_IN_AAA(T, T3, node(U, X, T2)) → U14_AAA(T, T3, U, X, T2, left_in_aa(T, T1))
U14_AAA(T, T3, U, X, T2, left_out_aa(T, T1)) → U15_AAA(T, T3, U, X, T2, T1, right_in_aa(T, T2))
U15_AAA(T, T3, U, X, T2, T1, right_out_aa(T, T2)) → U16_AAA(T, T3, U, X, T2, T1, value_in_aa(T, X))
U16_AAA(T, T3, U, X, T2, T1, value_out_aa(T, X)) → TAPPEND_IN_AAA(T1, T3, U)
TAPPEND_IN_AAA(T, T1, node(T1, X, U)) → U18_AAA(T, T1, X, U, left_in_aa(T, T1))
U18_AAA(T, T1, X, U, left_out_aa(T, T1)) → U19_AAA(T, T1, X, U, right_in_aa(T, T2))
U19_AAA(T, T1, X, U, right_out_aa(T, T2)) → U20_AAA(T, T1, X, U, T2, value_in_aa(T, X))
U20_AAA(T, T1, X, U, T2, value_out_aa(T, X)) → TAPPEND_IN_AAA(T2, T3, U)
left_in_aa(nil, nil) → left_out_aa(nil, nil)
left_in_aa(node(L, X9, X10), L) → left_out_aa(node(L, X9, X10), L)
right_in_aa(nil, nil) → right_out_aa(nil, nil)
right_in_aa(node(X11, X12, R), R) → right_out_aa(node(X11, X12, R), R)
value_in_aa(nil, nil) → value_out_aa(nil, nil)
value_in_aa(node(X13, X, X14), X) → value_out_aa(node(X13, X, X14), X)
TAPPEND_IN_AAA → U14_AAA(left_in_aa)
U14_AAA(left_out_aa) → U15_AAA(right_in_aa)
U15_AAA(right_out_aa) → U16_AAA(value_in_aa)
U16_AAA(value_out_aa) → TAPPEND_IN_AAA
TAPPEND_IN_AAA → U18_AAA(left_in_aa)
U18_AAA(left_out_aa) → U19_AAA(right_in_aa)
U19_AAA(right_out_aa) → U20_AAA(value_in_aa)
U20_AAA(value_out_aa) → TAPPEND_IN_AAA
left_in_aa → left_out_aa
right_in_aa → right_out_aa
value_in_aa → value_out_aa
left_in_aa
right_in_aa
value_in_aa
TAPPEND_IN_AAA → U14_AAA(left_out_aa)
U14_AAA(left_out_aa) → U15_AAA(right_in_aa)
U15_AAA(right_out_aa) → U16_AAA(value_in_aa)
U16_AAA(value_out_aa) → TAPPEND_IN_AAA
TAPPEND_IN_AAA → U18_AAA(left_in_aa)
U18_AAA(left_out_aa) → U19_AAA(right_in_aa)
U19_AAA(right_out_aa) → U20_AAA(value_in_aa)
U20_AAA(value_out_aa) → TAPPEND_IN_AAA
TAPPEND_IN_AAA → U14_AAA(left_out_aa)
left_in_aa → left_out_aa
right_in_aa → right_out_aa
value_in_aa → value_out_aa
left_in_aa
right_in_aa
value_in_aa
U14_AAA(left_out_aa) → U15_AAA(right_out_aa)
U15_AAA(right_out_aa) → U16_AAA(value_in_aa)
U16_AAA(value_out_aa) → TAPPEND_IN_AAA
TAPPEND_IN_AAA → U18_AAA(left_in_aa)
U18_AAA(left_out_aa) → U19_AAA(right_in_aa)
U19_AAA(right_out_aa) → U20_AAA(value_in_aa)
U20_AAA(value_out_aa) → TAPPEND_IN_AAA
TAPPEND_IN_AAA → U14_AAA(left_out_aa)
U14_AAA(left_out_aa) → U15_AAA(right_out_aa)
left_in_aa → left_out_aa
right_in_aa → right_out_aa
value_in_aa → value_out_aa
left_in_aa
right_in_aa
value_in_aa
U15_AAA(right_out_aa) → U16_AAA(value_out_aa)
U16_AAA(value_out_aa) → TAPPEND_IN_AAA
TAPPEND_IN_AAA → U18_AAA(left_in_aa)
U18_AAA(left_out_aa) → U19_AAA(right_in_aa)
U19_AAA(right_out_aa) → U20_AAA(value_in_aa)
U20_AAA(value_out_aa) → TAPPEND_IN_AAA
TAPPEND_IN_AAA → U14_AAA(left_out_aa)
U14_AAA(left_out_aa) → U15_AAA(right_out_aa)
U15_AAA(right_out_aa) → U16_AAA(value_out_aa)
left_in_aa → left_out_aa
right_in_aa → right_out_aa
value_in_aa → value_out_aa
left_in_aa
right_in_aa
value_in_aa
TAPPEND_IN_AAA → U18_AAA(left_out_aa)
U16_AAA(value_out_aa) → TAPPEND_IN_AAA
U18_AAA(left_out_aa) → U19_AAA(right_in_aa)
U19_AAA(right_out_aa) → U20_AAA(value_in_aa)
U20_AAA(value_out_aa) → TAPPEND_IN_AAA
TAPPEND_IN_AAA → U14_AAA(left_out_aa)
U14_AAA(left_out_aa) → U15_AAA(right_out_aa)
U15_AAA(right_out_aa) → U16_AAA(value_out_aa)
TAPPEND_IN_AAA → U18_AAA(left_out_aa)
left_in_aa → left_out_aa
right_in_aa → right_out_aa
value_in_aa → value_out_aa
left_in_aa
right_in_aa
value_in_aa
U16_AAA(value_out_aa) → TAPPEND_IN_AAA
U18_AAA(left_out_aa) → U19_AAA(right_in_aa)
U19_AAA(right_out_aa) → U20_AAA(value_in_aa)
U20_AAA(value_out_aa) → TAPPEND_IN_AAA
TAPPEND_IN_AAA → U14_AAA(left_out_aa)
U14_AAA(left_out_aa) → U15_AAA(right_out_aa)
U15_AAA(right_out_aa) → U16_AAA(value_out_aa)
TAPPEND_IN_AAA → U18_AAA(left_out_aa)
value_in_aa → value_out_aa
right_in_aa → right_out_aa
left_in_aa
right_in_aa
value_in_aa
left_in_aa
U16_AAA(value_out_aa) → TAPPEND_IN_AAA
U18_AAA(left_out_aa) → U19_AAA(right_in_aa)
U19_AAA(right_out_aa) → U20_AAA(value_in_aa)
U20_AAA(value_out_aa) → TAPPEND_IN_AAA
TAPPEND_IN_AAA → U14_AAA(left_out_aa)
U14_AAA(left_out_aa) → U15_AAA(right_out_aa)
U15_AAA(right_out_aa) → U16_AAA(value_out_aa)
TAPPEND_IN_AAA → U18_AAA(left_out_aa)
value_in_aa → value_out_aa
right_in_aa → right_out_aa
right_in_aa
value_in_aa
U18_AAA(left_out_aa) → U19_AAA(right_out_aa)
U16_AAA(value_out_aa) → TAPPEND_IN_AAA
U19_AAA(right_out_aa) → U20_AAA(value_in_aa)
U20_AAA(value_out_aa) → TAPPEND_IN_AAA
TAPPEND_IN_AAA → U14_AAA(left_out_aa)
U14_AAA(left_out_aa) → U15_AAA(right_out_aa)
U15_AAA(right_out_aa) → U16_AAA(value_out_aa)
TAPPEND_IN_AAA → U18_AAA(left_out_aa)
U18_AAA(left_out_aa) → U19_AAA(right_out_aa)
value_in_aa → value_out_aa
right_in_aa → right_out_aa
right_in_aa
value_in_aa
U16_AAA(value_out_aa) → TAPPEND_IN_AAA
U19_AAA(right_out_aa) → U20_AAA(value_in_aa)
U20_AAA(value_out_aa) → TAPPEND_IN_AAA
TAPPEND_IN_AAA → U14_AAA(left_out_aa)
U14_AAA(left_out_aa) → U15_AAA(right_out_aa)
U15_AAA(right_out_aa) → U16_AAA(value_out_aa)
TAPPEND_IN_AAA → U18_AAA(left_out_aa)
U18_AAA(left_out_aa) → U19_AAA(right_out_aa)
value_in_aa → value_out_aa
right_in_aa
value_in_aa
right_in_aa
U16_AAA(value_out_aa) → TAPPEND_IN_AAA
U19_AAA(right_out_aa) → U20_AAA(value_in_aa)
U20_AAA(value_out_aa) → TAPPEND_IN_AAA
TAPPEND_IN_AAA → U14_AAA(left_out_aa)
U14_AAA(left_out_aa) → U15_AAA(right_out_aa)
U15_AAA(right_out_aa) → U16_AAA(value_out_aa)
TAPPEND_IN_AAA → U18_AAA(left_out_aa)
U18_AAA(left_out_aa) → U19_AAA(right_out_aa)
value_in_aa → value_out_aa
value_in_aa
U19_AAA(right_out_aa) → U20_AAA(value_out_aa)
U16_AAA(value_out_aa) → TAPPEND_IN_AAA
U20_AAA(value_out_aa) → TAPPEND_IN_AAA
TAPPEND_IN_AAA → U14_AAA(left_out_aa)
U14_AAA(left_out_aa) → U15_AAA(right_out_aa)
U15_AAA(right_out_aa) → U16_AAA(value_out_aa)
TAPPEND_IN_AAA → U18_AAA(left_out_aa)
U18_AAA(left_out_aa) → U19_AAA(right_out_aa)
U19_AAA(right_out_aa) → U20_AAA(value_out_aa)
value_in_aa → value_out_aa
value_in_aa
U16_AAA(value_out_aa) → TAPPEND_IN_AAA
U20_AAA(value_out_aa) → TAPPEND_IN_AAA
TAPPEND_IN_AAA → U14_AAA(left_out_aa)
U14_AAA(left_out_aa) → U15_AAA(right_out_aa)
U15_AAA(right_out_aa) → U16_AAA(value_out_aa)
TAPPEND_IN_AAA → U18_AAA(left_out_aa)
U18_AAA(left_out_aa) → U19_AAA(right_out_aa)
U19_AAA(right_out_aa) → U20_AAA(value_out_aa)
value_in_aa
value_in_aa
U16_AAA(value_out_aa) → TAPPEND_IN_AAA
U20_AAA(value_out_aa) → TAPPEND_IN_AAA
TAPPEND_IN_AAA → U14_AAA(left_out_aa)
U14_AAA(left_out_aa) → U15_AAA(right_out_aa)
U15_AAA(right_out_aa) → U16_AAA(value_out_aa)
TAPPEND_IN_AAA → U18_AAA(left_out_aa)
U18_AAA(left_out_aa) → U19_AAA(right_out_aa)
U19_AAA(right_out_aa) → U20_AAA(value_out_aa)
S2T_IN_GA(X, node(T, X5, T)) → U23_GA(X, T, X5, p_in_ga(X, P))
U23_GA(X, T, X5, p_out_ga(X, P)) → S2T_IN_GA(P, T)
S2T_IN_GA(X, node(nil, X6, T)) → U25_GA(X, X6, T, p_in_ga(X, P))
U25_GA(X, X6, T, p_out_ga(X, P)) → S2T_IN_GA(P, T)
S2T_IN_GA(X, node(T, X7, nil)) → U27_GA(X, T, X7, p_in_ga(X, P))
U27_GA(X, T, X7, p_out_ga(X, P)) → S2T_IN_GA(P, T)
goal_in_gaa(A, B, C) → U1_gaa(A, B, C, s2t_in_ga(A, T))
s2t_in_ga(0, L) → U22_ga(L, eq_in_ag(L, nil))
eq_in_ag(X, X) → eq_out_ag(X, X)
U22_ga(L, eq_out_ag(L, nil)) → s2t_out_ga(0, L)
s2t_in_ga(X, node(T, X5, T)) → U23_ga(X, T, X5, p_in_ga(X, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U23_ga(X, T, X5, p_out_ga(X, P)) → U24_ga(X, T, X5, s2t_in_ga(P, T))
s2t_in_ga(X, node(nil, X6, T)) → U25_ga(X, X6, T, p_in_ga(X, P))
U25_ga(X, X6, T, p_out_ga(X, P)) → U26_ga(X, X6, T, s2t_in_ga(P, T))
s2t_in_ga(X, node(T, X7, nil)) → U27_ga(X, T, X7, p_in_ga(X, P))
U27_ga(X, T, X7, p_out_ga(X, P)) → U28_ga(X, T, X7, s2t_in_ga(P, T))
s2t_in_ga(X, node(nil, X8, nil)) → s2t_out_ga(X, node(nil, X8, nil))
U28_ga(X, T, X7, s2t_out_ga(P, T)) → s2t_out_ga(X, node(T, X7, nil))
U26_ga(X, X6, T, s2t_out_ga(P, T)) → s2t_out_ga(X, node(nil, X6, T))
U24_ga(X, T, X5, s2t_out_ga(P, T)) → s2t_out_ga(X, node(T, X5, T))
U1_gaa(A, B, C, s2t_out_ga(A, T)) → U2_gaa(A, B, C, tapplast_in_aaa(T, B, C))
tapplast_in_aaa(L, X, Last) → U3_aaa(L, X, Last, tappend_in_aaa(L, node(nil, X, nil), LX))
tappend_in_aaa(nil, Y, Z) → U7_aaa(Y, Z, eq_in_aa(Y, Z))
eq_in_aa(X, X) → eq_out_aa(X, X)
U7_aaa(Y, Z, eq_out_aa(Y, Z)) → tappend_out_aaa(nil, Y, Z)
tappend_in_aaa(T, T1, node(T1, X, T2)) → U8_aaa(T, T1, X, T2, left_in_ag(T, nil))
left_in_ag(nil, nil) → left_out_ag(nil, nil)
left_in_ag(node(L, X9, X10), L) → left_out_ag(node(L, X9, X10), L)
U8_aaa(T, T1, X, T2, left_out_ag(T, nil)) → U9_aaa(T, T1, X, T2, right_in_aa(T, T2))
right_in_aa(nil, nil) → right_out_aa(nil, nil)
right_in_aa(node(X11, X12, R), R) → right_out_aa(node(X11, X12, R), R)
U9_aaa(T, T1, X, T2, right_out_aa(T, T2)) → U10_aaa(T, T1, X, T2, value_in_aa(T, X))
value_in_aa(nil, nil) → value_out_aa(nil, nil)
value_in_aa(node(X13, X, X14), X) → value_out_aa(node(X13, X, X14), X)
U10_aaa(T, T1, X, T2, value_out_aa(T, X)) → tappend_out_aaa(T, T1, node(T1, X, T2))
tappend_in_aaa(T, T2, node(T1, X, T2)) → U11_aaa(T, T2, T1, X, left_in_aa(T, T1))
left_in_aa(nil, nil) → left_out_aa(nil, nil)
left_in_aa(node(L, X9, X10), L) → left_out_aa(node(L, X9, X10), L)
U11_aaa(T, T2, T1, X, left_out_aa(T, T1)) → U12_aaa(T, T2, T1, X, right_in_ag(T, nil))
right_in_ag(nil, nil) → right_out_ag(nil, nil)
right_in_ag(node(X11, X12, R), R) → right_out_ag(node(X11, X12, R), R)
U12_aaa(T, T2, T1, X, right_out_ag(T, nil)) → U13_aaa(T, T2, T1, X, value_in_aa(T, X))
U13_aaa(T, T2, T1, X, value_out_aa(T, X)) → tappend_out_aaa(T, T2, node(T1, X, T2))
tappend_in_aaa(T, T3, node(U, X, T2)) → U14_aaa(T, T3, U, X, T2, left_in_aa(T, T1))
U14_aaa(T, T3, U, X, T2, left_out_aa(T, T1)) → U15_aaa(T, T3, U, X, T2, T1, right_in_aa(T, T2))
U15_aaa(T, T3, U, X, T2, T1, right_out_aa(T, T2)) → U16_aaa(T, T3, U, X, T2, T1, value_in_aa(T, X))
U16_aaa(T, T3, U, X, T2, T1, value_out_aa(T, X)) → U17_aaa(T, T3, U, X, T2, tappend_in_aaa(T1, T3, U))
tappend_in_aaa(T, T1, node(T1, X, U)) → U18_aaa(T, T1, X, U, left_in_aa(T, T1))
U18_aaa(T, T1, X, U, left_out_aa(T, T1)) → U19_aaa(T, T1, X, U, right_in_aa(T, T2))
U19_aaa(T, T1, X, U, right_out_aa(T, T2)) → U20_aaa(T, T1, X, U, T2, value_in_aa(T, X))
U20_aaa(T, T1, X, U, T2, value_out_aa(T, X)) → U21_aaa(T, T1, X, U, tappend_in_aaa(T2, T3, U))
U21_aaa(T, T1, X, U, tappend_out_aaa(T2, T3, U)) → tappend_out_aaa(T, T1, node(T1, X, U))
U17_aaa(T, T3, U, X, T2, tappend_out_aaa(T1, T3, U)) → tappend_out_aaa(T, T3, node(U, X, T2))
U3_aaa(L, X, Last, tappend_out_aaa(L, node(nil, X, nil), LX)) → U4_aaa(L, X, Last, tlast_in_aa(Last, LX))
tlast_in_aa(X, node(nil, X, nil)) → tlast_out_aa(X, node(nil, X, nil))
tlast_in_aa(X, node(L, X1, X2)) → U5_aa(X, L, X1, X2, tlast_in_aa(X, L))
tlast_in_aa(X, node(X3, X4, R)) → U6_aa(X, X3, X4, R, tlast_in_aa(X, R))
U6_aa(X, X3, X4, R, tlast_out_aa(X, R)) → tlast_out_aa(X, node(X3, X4, R))
U5_aa(X, L, X1, X2, tlast_out_aa(X, L)) → tlast_out_aa(X, node(L, X1, X2))
U4_aaa(L, X, Last, tlast_out_aa(Last, LX)) → tapplast_out_aaa(L, X, Last)
U2_gaa(A, B, C, tapplast_out_aaa(T, B, C)) → goal_out_gaa(A, B, C)
S2T_IN_GA(X, node(T, X5, T)) → U23_GA(X, T, X5, p_in_ga(X, P))
U23_GA(X, T, X5, p_out_ga(X, P)) → S2T_IN_GA(P, T)
S2T_IN_GA(X, node(nil, X6, T)) → U25_GA(X, X6, T, p_in_ga(X, P))
U25_GA(X, X6, T, p_out_ga(X, P)) → S2T_IN_GA(P, T)
S2T_IN_GA(X, node(T, X7, nil)) → U27_GA(X, T, X7, p_in_ga(X, P))
U27_GA(X, T, X7, p_out_ga(X, P)) → S2T_IN_GA(P, T)
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
S2T_IN_GA(X) → U23_GA(p_in_ga(X))
U23_GA(p_out_ga(P)) → S2T_IN_GA(P)
S2T_IN_GA(X) → U25_GA(p_in_ga(X))
U25_GA(p_out_ga(P)) → S2T_IN_GA(P)
S2T_IN_GA(X) → U27_GA(p_in_ga(X))
U27_GA(p_out_ga(P)) → S2T_IN_GA(P)
p_in_ga(0) → p_out_ga(0)
p_in_ga(s(X)) → p_out_ga(X)
p_in_ga(x0)
Used ordering: POLO with Polynomial interpretation [POLO]:
p_in_ga(s(X)) → p_out_ga(X)
POL(0) = 0
POL(S2T_IN_GA(x1)) = x1
POL(U23_GA(x1)) = x1
POL(U25_GA(x1)) = x1
POL(U27_GA(x1)) = x1
POL(p_in_ga(x1)) = x1
POL(p_out_ga(x1)) = 2·x1
POL(s(x1)) = 2 + 2·x1
S2T_IN_GA(X) → U23_GA(p_in_ga(X))
U23_GA(p_out_ga(P)) → S2T_IN_GA(P)
S2T_IN_GA(X) → U25_GA(p_in_ga(X))
U25_GA(p_out_ga(P)) → S2T_IN_GA(P)
S2T_IN_GA(X) → U27_GA(p_in_ga(X))
U27_GA(p_out_ga(P)) → S2T_IN_GA(P)
p_in_ga(0) → p_out_ga(0)
p_in_ga(x0)
S2T_IN_GA(0) → U23_GA(p_out_ga(0))
U23_GA(p_out_ga(P)) → S2T_IN_GA(P)
S2T_IN_GA(X) → U25_GA(p_in_ga(X))
U25_GA(p_out_ga(P)) → S2T_IN_GA(P)
S2T_IN_GA(X) → U27_GA(p_in_ga(X))
U27_GA(p_out_ga(P)) → S2T_IN_GA(P)
S2T_IN_GA(0) → U23_GA(p_out_ga(0))
p_in_ga(0) → p_out_ga(0)
p_in_ga(x0)
S2T_IN_GA(0) → U25_GA(p_out_ga(0))
U23_GA(p_out_ga(P)) → S2T_IN_GA(P)
U25_GA(p_out_ga(P)) → S2T_IN_GA(P)
S2T_IN_GA(X) → U27_GA(p_in_ga(X))
U27_GA(p_out_ga(P)) → S2T_IN_GA(P)
S2T_IN_GA(0) → U23_GA(p_out_ga(0))
S2T_IN_GA(0) → U25_GA(p_out_ga(0))
p_in_ga(0) → p_out_ga(0)
p_in_ga(x0)
S2T_IN_GA(0) → U27_GA(p_out_ga(0))
U23_GA(p_out_ga(P)) → S2T_IN_GA(P)
U25_GA(p_out_ga(P)) → S2T_IN_GA(P)
U27_GA(p_out_ga(P)) → S2T_IN_GA(P)
S2T_IN_GA(0) → U23_GA(p_out_ga(0))
S2T_IN_GA(0) → U25_GA(p_out_ga(0))
S2T_IN_GA(0) → U27_GA(p_out_ga(0))
p_in_ga(0) → p_out_ga(0)
p_in_ga(x0)
U23_GA(p_out_ga(P)) → S2T_IN_GA(P)
U25_GA(p_out_ga(P)) → S2T_IN_GA(P)
U27_GA(p_out_ga(P)) → S2T_IN_GA(P)
S2T_IN_GA(0) → U23_GA(p_out_ga(0))
S2T_IN_GA(0) → U25_GA(p_out_ga(0))
S2T_IN_GA(0) → U27_GA(p_out_ga(0))
p_in_ga(x0)
p_in_ga(x0)
U23_GA(p_out_ga(P)) → S2T_IN_GA(P)
U25_GA(p_out_ga(P)) → S2T_IN_GA(P)
U27_GA(p_out_ga(P)) → S2T_IN_GA(P)
S2T_IN_GA(0) → U23_GA(p_out_ga(0))
S2T_IN_GA(0) → U25_GA(p_out_ga(0))
S2T_IN_GA(0) → U27_GA(p_out_ga(0))
U23_GA(p_out_ga(0)) → S2T_IN_GA(0)
U25_GA(p_out_ga(P)) → S2T_IN_GA(P)
U27_GA(p_out_ga(P)) → S2T_IN_GA(P)
S2T_IN_GA(0) → U23_GA(p_out_ga(0))
S2T_IN_GA(0) → U25_GA(p_out_ga(0))
S2T_IN_GA(0) → U27_GA(p_out_ga(0))
U23_GA(p_out_ga(0)) → S2T_IN_GA(0)
U25_GA(p_out_ga(0)) → S2T_IN_GA(0)
U27_GA(p_out_ga(P)) → S2T_IN_GA(P)
S2T_IN_GA(0) → U23_GA(p_out_ga(0))
S2T_IN_GA(0) → U25_GA(p_out_ga(0))
S2T_IN_GA(0) → U27_GA(p_out_ga(0))
U23_GA(p_out_ga(0)) → S2T_IN_GA(0)
U25_GA(p_out_ga(0)) → S2T_IN_GA(0)
U27_GA(p_out_ga(0)) → S2T_IN_GA(0)
S2T_IN_GA(0) → U23_GA(p_out_ga(0))
S2T_IN_GA(0) → U25_GA(p_out_ga(0))
S2T_IN_GA(0) → U27_GA(p_out_ga(0))
U23_GA(p_out_ga(0)) → S2T_IN_GA(0)
U25_GA(p_out_ga(0)) → S2T_IN_GA(0)
U27_GA(p_out_ga(0)) → S2T_IN_GA(0)
goal_in_gaa(A, B, C) → U1_gaa(A, B, C, s2t_in_ga(A, T))
s2t_in_ga(0, L) → U22_ga(L, eq_in_ag(L, nil))
eq_in_ag(X, X) → eq_out_ag(X, X)
U22_ga(L, eq_out_ag(L, nil)) → s2t_out_ga(0, L)
s2t_in_ga(X, node(T, X5, T)) → U23_ga(X, T, X5, p_in_ga(X, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U23_ga(X, T, X5, p_out_ga(X, P)) → U24_ga(X, T, X5, s2t_in_ga(P, T))
s2t_in_ga(X, node(nil, X6, T)) → U25_ga(X, X6, T, p_in_ga(X, P))
U25_ga(X, X6, T, p_out_ga(X, P)) → U26_ga(X, X6, T, s2t_in_ga(P, T))
s2t_in_ga(X, node(T, X7, nil)) → U27_ga(X, T, X7, p_in_ga(X, P))
U27_ga(X, T, X7, p_out_ga(X, P)) → U28_ga(X, T, X7, s2t_in_ga(P, T))
s2t_in_ga(X, node(nil, X8, nil)) → s2t_out_ga(X, node(nil, X8, nil))
U28_ga(X, T, X7, s2t_out_ga(P, T)) → s2t_out_ga(X, node(T, X7, nil))
U26_ga(X, X6, T, s2t_out_ga(P, T)) → s2t_out_ga(X, node(nil, X6, T))
U24_ga(X, T, X5, s2t_out_ga(P, T)) → s2t_out_ga(X, node(T, X5, T))
U1_gaa(A, B, C, s2t_out_ga(A, T)) → U2_gaa(A, B, C, tapplast_in_aaa(T, B, C))
tapplast_in_aaa(L, X, Last) → U3_aaa(L, X, Last, tappend_in_aaa(L, node(nil, X, nil), LX))
tappend_in_aaa(nil, Y, Z) → U7_aaa(Y, Z, eq_in_aa(Y, Z))
eq_in_aa(X, X) → eq_out_aa(X, X)
U7_aaa(Y, Z, eq_out_aa(Y, Z)) → tappend_out_aaa(nil, Y, Z)
tappend_in_aaa(T, T1, node(T1, X, T2)) → U8_aaa(T, T1, X, T2, left_in_ag(T, nil))
left_in_ag(nil, nil) → left_out_ag(nil, nil)
left_in_ag(node(L, X9, X10), L) → left_out_ag(node(L, X9, X10), L)
U8_aaa(T, T1, X, T2, left_out_ag(T, nil)) → U9_aaa(T, T1, X, T2, right_in_aa(T, T2))
right_in_aa(nil, nil) → right_out_aa(nil, nil)
right_in_aa(node(X11, X12, R), R) → right_out_aa(node(X11, X12, R), R)
U9_aaa(T, T1, X, T2, right_out_aa(T, T2)) → U10_aaa(T, T1, X, T2, value_in_aa(T, X))
value_in_aa(nil, nil) → value_out_aa(nil, nil)
value_in_aa(node(X13, X, X14), X) → value_out_aa(node(X13, X, X14), X)
U10_aaa(T, T1, X, T2, value_out_aa(T, X)) → tappend_out_aaa(T, T1, node(T1, X, T2))
tappend_in_aaa(T, T2, node(T1, X, T2)) → U11_aaa(T, T2, T1, X, left_in_aa(T, T1))
left_in_aa(nil, nil) → left_out_aa(nil, nil)
left_in_aa(node(L, X9, X10), L) → left_out_aa(node(L, X9, X10), L)
U11_aaa(T, T2, T1, X, left_out_aa(T, T1)) → U12_aaa(T, T2, T1, X, right_in_ag(T, nil))
right_in_ag(nil, nil) → right_out_ag(nil, nil)
right_in_ag(node(X11, X12, R), R) → right_out_ag(node(X11, X12, R), R)
U12_aaa(T, T2, T1, X, right_out_ag(T, nil)) → U13_aaa(T, T2, T1, X, value_in_aa(T, X))
U13_aaa(T, T2, T1, X, value_out_aa(T, X)) → tappend_out_aaa(T, T2, node(T1, X, T2))
tappend_in_aaa(T, T3, node(U, X, T2)) → U14_aaa(T, T3, U, X, T2, left_in_aa(T, T1))
U14_aaa(T, T3, U, X, T2, left_out_aa(T, T1)) → U15_aaa(T, T3, U, X, T2, T1, right_in_aa(T, T2))
U15_aaa(T, T3, U, X, T2, T1, right_out_aa(T, T2)) → U16_aaa(T, T3, U, X, T2, T1, value_in_aa(T, X))
U16_aaa(T, T3, U, X, T2, T1, value_out_aa(T, X)) → U17_aaa(T, T3, U, X, T2, tappend_in_aaa(T1, T3, U))
tappend_in_aaa(T, T1, node(T1, X, U)) → U18_aaa(T, T1, X, U, left_in_aa(T, T1))
U18_aaa(T, T1, X, U, left_out_aa(T, T1)) → U19_aaa(T, T1, X, U, right_in_aa(T, T2))
U19_aaa(T, T1, X, U, right_out_aa(T, T2)) → U20_aaa(T, T1, X, U, T2, value_in_aa(T, X))
U20_aaa(T, T1, X, U, T2, value_out_aa(T, X)) → U21_aaa(T, T1, X, U, tappend_in_aaa(T2, T3, U))
U21_aaa(T, T1, X, U, tappend_out_aaa(T2, T3, U)) → tappend_out_aaa(T, T1, node(T1, X, U))
U17_aaa(T, T3, U, X, T2, tappend_out_aaa(T1, T3, U)) → tappend_out_aaa(T, T3, node(U, X, T2))
U3_aaa(L, X, Last, tappend_out_aaa(L, node(nil, X, nil), LX)) → U4_aaa(L, X, Last, tlast_in_aa(Last, LX))
tlast_in_aa(X, node(nil, X, nil)) → tlast_out_aa(X, node(nil, X, nil))
tlast_in_aa(X, node(L, X1, X2)) → U5_aa(X, L, X1, X2, tlast_in_aa(X, L))
tlast_in_aa(X, node(X3, X4, R)) → U6_aa(X, X3, X4, R, tlast_in_aa(X, R))
U6_aa(X, X3, X4, R, tlast_out_aa(X, R)) → tlast_out_aa(X, node(X3, X4, R))
U5_aa(X, L, X1, X2, tlast_out_aa(X, L)) → tlast_out_aa(X, node(L, X1, X2))
U4_aaa(L, X, Last, tlast_out_aa(Last, LX)) → tapplast_out_aaa(L, X, Last)
U2_gaa(A, B, C, tapplast_out_aaa(T, B, C)) → goal_out_gaa(A, B, C)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
goal_in_gaa(A, B, C) → U1_gaa(A, B, C, s2t_in_ga(A, T))
s2t_in_ga(0, L) → U22_ga(L, eq_in_ag(L, nil))
eq_in_ag(X, X) → eq_out_ag(X, X)
U22_ga(L, eq_out_ag(L, nil)) → s2t_out_ga(0, L)
s2t_in_ga(X, node(T, X5, T)) → U23_ga(X, T, X5, p_in_ga(X, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U23_ga(X, T, X5, p_out_ga(X, P)) → U24_ga(X, T, X5, s2t_in_ga(P, T))
s2t_in_ga(X, node(nil, X6, T)) → U25_ga(X, X6, T, p_in_ga(X, P))
U25_ga(X, X6, T, p_out_ga(X, P)) → U26_ga(X, X6, T, s2t_in_ga(P, T))
s2t_in_ga(X, node(T, X7, nil)) → U27_ga(X, T, X7, p_in_ga(X, P))
U27_ga(X, T, X7, p_out_ga(X, P)) → U28_ga(X, T, X7, s2t_in_ga(P, T))
s2t_in_ga(X, node(nil, X8, nil)) → s2t_out_ga(X, node(nil, X8, nil))
U28_ga(X, T, X7, s2t_out_ga(P, T)) → s2t_out_ga(X, node(T, X7, nil))
U26_ga(X, X6, T, s2t_out_ga(P, T)) → s2t_out_ga(X, node(nil, X6, T))
U24_ga(X, T, X5, s2t_out_ga(P, T)) → s2t_out_ga(X, node(T, X5, T))
U1_gaa(A, B, C, s2t_out_ga(A, T)) → U2_gaa(A, B, C, tapplast_in_aaa(T, B, C))
tapplast_in_aaa(L, X, Last) → U3_aaa(L, X, Last, tappend_in_aaa(L, node(nil, X, nil), LX))
tappend_in_aaa(nil, Y, Z) → U7_aaa(Y, Z, eq_in_aa(Y, Z))
eq_in_aa(X, X) → eq_out_aa(X, X)
U7_aaa(Y, Z, eq_out_aa(Y, Z)) → tappend_out_aaa(nil, Y, Z)
tappend_in_aaa(T, T1, node(T1, X, T2)) → U8_aaa(T, T1, X, T2, left_in_ag(T, nil))
left_in_ag(nil, nil) → left_out_ag(nil, nil)
left_in_ag(node(L, X9, X10), L) → left_out_ag(node(L, X9, X10), L)
U8_aaa(T, T1, X, T2, left_out_ag(T, nil)) → U9_aaa(T, T1, X, T2, right_in_aa(T, T2))
right_in_aa(nil, nil) → right_out_aa(nil, nil)
right_in_aa(node(X11, X12, R), R) → right_out_aa(node(X11, X12, R), R)
U9_aaa(T, T1, X, T2, right_out_aa(T, T2)) → U10_aaa(T, T1, X, T2, value_in_aa(T, X))
value_in_aa(nil, nil) → value_out_aa(nil, nil)
value_in_aa(node(X13, X, X14), X) → value_out_aa(node(X13, X, X14), X)
U10_aaa(T, T1, X, T2, value_out_aa(T, X)) → tappend_out_aaa(T, T1, node(T1, X, T2))
tappend_in_aaa(T, T2, node(T1, X, T2)) → U11_aaa(T, T2, T1, X, left_in_aa(T, T1))
left_in_aa(nil, nil) → left_out_aa(nil, nil)
left_in_aa(node(L, X9, X10), L) → left_out_aa(node(L, X9, X10), L)
U11_aaa(T, T2, T1, X, left_out_aa(T, T1)) → U12_aaa(T, T2, T1, X, right_in_ag(T, nil))
right_in_ag(nil, nil) → right_out_ag(nil, nil)
right_in_ag(node(X11, X12, R), R) → right_out_ag(node(X11, X12, R), R)
U12_aaa(T, T2, T1, X, right_out_ag(T, nil)) → U13_aaa(T, T2, T1, X, value_in_aa(T, X))
U13_aaa(T, T2, T1, X, value_out_aa(T, X)) → tappend_out_aaa(T, T2, node(T1, X, T2))
tappend_in_aaa(T, T3, node(U, X, T2)) → U14_aaa(T, T3, U, X, T2, left_in_aa(T, T1))
U14_aaa(T, T3, U, X, T2, left_out_aa(T, T1)) → U15_aaa(T, T3, U, X, T2, T1, right_in_aa(T, T2))
U15_aaa(T, T3, U, X, T2, T1, right_out_aa(T, T2)) → U16_aaa(T, T3, U, X, T2, T1, value_in_aa(T, X))
U16_aaa(T, T3, U, X, T2, T1, value_out_aa(T, X)) → U17_aaa(T, T3, U, X, T2, tappend_in_aaa(T1, T3, U))
tappend_in_aaa(T, T1, node(T1, X, U)) → U18_aaa(T, T1, X, U, left_in_aa(T, T1))
U18_aaa(T, T1, X, U, left_out_aa(T, T1)) → U19_aaa(T, T1, X, U, right_in_aa(T, T2))
U19_aaa(T, T1, X, U, right_out_aa(T, T2)) → U20_aaa(T, T1, X, U, T2, value_in_aa(T, X))
U20_aaa(T, T1, X, U, T2, value_out_aa(T, X)) → U21_aaa(T, T1, X, U, tappend_in_aaa(T2, T3, U))
U21_aaa(T, T1, X, U, tappend_out_aaa(T2, T3, U)) → tappend_out_aaa(T, T1, node(T1, X, U))
U17_aaa(T, T3, U, X, T2, tappend_out_aaa(T1, T3, U)) → tappend_out_aaa(T, T3, node(U, X, T2))
U3_aaa(L, X, Last, tappend_out_aaa(L, node(nil, X, nil), LX)) → U4_aaa(L, X, Last, tlast_in_aa(Last, LX))
tlast_in_aa(X, node(nil, X, nil)) → tlast_out_aa(X, node(nil, X, nil))
tlast_in_aa(X, node(L, X1, X2)) → U5_aa(X, L, X1, X2, tlast_in_aa(X, L))
tlast_in_aa(X, node(X3, X4, R)) → U6_aa(X, X3, X4, R, tlast_in_aa(X, R))
U6_aa(X, X3, X4, R, tlast_out_aa(X, R)) → tlast_out_aa(X, node(X3, X4, R))
U5_aa(X, L, X1, X2, tlast_out_aa(X, L)) → tlast_out_aa(X, node(L, X1, X2))
U4_aaa(L, X, Last, tlast_out_aa(Last, LX)) → tapplast_out_aaa(L, X, Last)
U2_gaa(A, B, C, tapplast_out_aaa(T, B, C)) → goal_out_gaa(A, B, C)
GOAL_IN_GAA(A, B, C) → U1_GAA(A, B, C, s2t_in_ga(A, T))
GOAL_IN_GAA(A, B, C) → S2T_IN_GA(A, T)
S2T_IN_GA(0, L) → U22_GA(L, eq_in_ag(L, nil))
S2T_IN_GA(0, L) → EQ_IN_AG(L, nil)
S2T_IN_GA(X, node(T, X5, T)) → U23_GA(X, T, X5, p_in_ga(X, P))
S2T_IN_GA(X, node(T, X5, T)) → P_IN_GA(X, P)
U23_GA(X, T, X5, p_out_ga(X, P)) → U24_GA(X, T, X5, s2t_in_ga(P, T))
U23_GA(X, T, X5, p_out_ga(X, P)) → S2T_IN_GA(P, T)
S2T_IN_GA(X, node(nil, X6, T)) → U25_GA(X, X6, T, p_in_ga(X, P))
S2T_IN_GA(X, node(nil, X6, T)) → P_IN_GA(X, P)
U25_GA(X, X6, T, p_out_ga(X, P)) → U26_GA(X, X6, T, s2t_in_ga(P, T))
U25_GA(X, X6, T, p_out_ga(X, P)) → S2T_IN_GA(P, T)
S2T_IN_GA(X, node(T, X7, nil)) → U27_GA(X, T, X7, p_in_ga(X, P))
S2T_IN_GA(X, node(T, X7, nil)) → P_IN_GA(X, P)
U27_GA(X, T, X7, p_out_ga(X, P)) → U28_GA(X, T, X7, s2t_in_ga(P, T))
U27_GA(X, T, X7, p_out_ga(X, P)) → S2T_IN_GA(P, T)
U1_GAA(A, B, C, s2t_out_ga(A, T)) → U2_GAA(A, B, C, tapplast_in_aaa(T, B, C))
U1_GAA(A, B, C, s2t_out_ga(A, T)) → TAPPLAST_IN_AAA(T, B, C)
TAPPLAST_IN_AAA(L, X, Last) → U3_AAA(L, X, Last, tappend_in_aaa(L, node(nil, X, nil), LX))
TAPPLAST_IN_AAA(L, X, Last) → TAPPEND_IN_AAA(L, node(nil, X, nil), LX)
TAPPEND_IN_AAA(nil, Y, Z) → U7_AAA(Y, Z, eq_in_aa(Y, Z))
TAPPEND_IN_AAA(nil, Y, Z) → EQ_IN_AA(Y, Z)
TAPPEND_IN_AAA(T, T1, node(T1, X, T2)) → U8_AAA(T, T1, X, T2, left_in_ag(T, nil))
TAPPEND_IN_AAA(T, T1, node(T1, X, T2)) → LEFT_IN_AG(T, nil)
U8_AAA(T, T1, X, T2, left_out_ag(T, nil)) → U9_AAA(T, T1, X, T2, right_in_aa(T, T2))
U8_AAA(T, T1, X, T2, left_out_ag(T, nil)) → RIGHT_IN_AA(T, T2)
U9_AAA(T, T1, X, T2, right_out_aa(T, T2)) → U10_AAA(T, T1, X, T2, value_in_aa(T, X))
U9_AAA(T, T1, X, T2, right_out_aa(T, T2)) → VALUE_IN_AA(T, X)
TAPPEND_IN_AAA(T, T2, node(T1, X, T2)) → U11_AAA(T, T2, T1, X, left_in_aa(T, T1))
TAPPEND_IN_AAA(T, T2, node(T1, X, T2)) → LEFT_IN_AA(T, T1)
U11_AAA(T, T2, T1, X, left_out_aa(T, T1)) → U12_AAA(T, T2, T1, X, right_in_ag(T, nil))
U11_AAA(T, T2, T1, X, left_out_aa(T, T1)) → RIGHT_IN_AG(T, nil)
U12_AAA(T, T2, T1, X, right_out_ag(T, nil)) → U13_AAA(T, T2, T1, X, value_in_aa(T, X))
U12_AAA(T, T2, T1, X, right_out_ag(T, nil)) → VALUE_IN_AA(T, X)
TAPPEND_IN_AAA(T, T3, node(U, X, T2)) → U14_AAA(T, T3, U, X, T2, left_in_aa(T, T1))
TAPPEND_IN_AAA(T, T3, node(U, X, T2)) → LEFT_IN_AA(T, T1)
U14_AAA(T, T3, U, X, T2, left_out_aa(T, T1)) → U15_AAA(T, T3, U, X, T2, T1, right_in_aa(T, T2))
U14_AAA(T, T3, U, X, T2, left_out_aa(T, T1)) → RIGHT_IN_AA(T, T2)
U15_AAA(T, T3, U, X, T2, T1, right_out_aa(T, T2)) → U16_AAA(T, T3, U, X, T2, T1, value_in_aa(T, X))
U15_AAA(T, T3, U, X, T2, T1, right_out_aa(T, T2)) → VALUE_IN_AA(T, X)
U16_AAA(T, T3, U, X, T2, T1, value_out_aa(T, X)) → U17_AAA(T, T3, U, X, T2, tappend_in_aaa(T1, T3, U))
U16_AAA(T, T3, U, X, T2, T1, value_out_aa(T, X)) → TAPPEND_IN_AAA(T1, T3, U)
TAPPEND_IN_AAA(T, T1, node(T1, X, U)) → U18_AAA(T, T1, X, U, left_in_aa(T, T1))
TAPPEND_IN_AAA(T, T1, node(T1, X, U)) → LEFT_IN_AA(T, T1)
U18_AAA(T, T1, X, U, left_out_aa(T, T1)) → U19_AAA(T, T1, X, U, right_in_aa(T, T2))
U18_AAA(T, T1, X, U, left_out_aa(T, T1)) → RIGHT_IN_AA(T, T2)
U19_AAA(T, T1, X, U, right_out_aa(T, T2)) → U20_AAA(T, T1, X, U, T2, value_in_aa(T, X))
U19_AAA(T, T1, X, U, right_out_aa(T, T2)) → VALUE_IN_AA(T, X)
U20_AAA(T, T1, X, U, T2, value_out_aa(T, X)) → U21_AAA(T, T1, X, U, tappend_in_aaa(T2, T3, U))
U20_AAA(T, T1, X, U, T2, value_out_aa(T, X)) → TAPPEND_IN_AAA(T2, T3, U)
U3_AAA(L, X, Last, tappend_out_aaa(L, node(nil, X, nil), LX)) → U4_AAA(L, X, Last, tlast_in_aa(Last, LX))
U3_AAA(L, X, Last, tappend_out_aaa(L, node(nil, X, nil), LX)) → TLAST_IN_AA(Last, LX)
TLAST_IN_AA(X, node(L, X1, X2)) → U5_AA(X, L, X1, X2, tlast_in_aa(X, L))
TLAST_IN_AA(X, node(L, X1, X2)) → TLAST_IN_AA(X, L)
TLAST_IN_AA(X, node(X3, X4, R)) → U6_AA(X, X3, X4, R, tlast_in_aa(X, R))
TLAST_IN_AA(X, node(X3, X4, R)) → TLAST_IN_AA(X, R)
goal_in_gaa(A, B, C) → U1_gaa(A, B, C, s2t_in_ga(A, T))
s2t_in_ga(0, L) → U22_ga(L, eq_in_ag(L, nil))
eq_in_ag(X, X) → eq_out_ag(X, X)
U22_ga(L, eq_out_ag(L, nil)) → s2t_out_ga(0, L)
s2t_in_ga(X, node(T, X5, T)) → U23_ga(X, T, X5, p_in_ga(X, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U23_ga(X, T, X5, p_out_ga(X, P)) → U24_ga(X, T, X5, s2t_in_ga(P, T))
s2t_in_ga(X, node(nil, X6, T)) → U25_ga(X, X6, T, p_in_ga(X, P))
U25_ga(X, X6, T, p_out_ga(X, P)) → U26_ga(X, X6, T, s2t_in_ga(P, T))
s2t_in_ga(X, node(T, X7, nil)) → U27_ga(X, T, X7, p_in_ga(X, P))
U27_ga(X, T, X7, p_out_ga(X, P)) → U28_ga(X, T, X7, s2t_in_ga(P, T))
s2t_in_ga(X, node(nil, X8, nil)) → s2t_out_ga(X, node(nil, X8, nil))
U28_ga(X, T, X7, s2t_out_ga(P, T)) → s2t_out_ga(X, node(T, X7, nil))
U26_ga(X, X6, T, s2t_out_ga(P, T)) → s2t_out_ga(X, node(nil, X6, T))
U24_ga(X, T, X5, s2t_out_ga(P, T)) → s2t_out_ga(X, node(T, X5, T))
U1_gaa(A, B, C, s2t_out_ga(A, T)) → U2_gaa(A, B, C, tapplast_in_aaa(T, B, C))
tapplast_in_aaa(L, X, Last) → U3_aaa(L, X, Last, tappend_in_aaa(L, node(nil, X, nil), LX))
tappend_in_aaa(nil, Y, Z) → U7_aaa(Y, Z, eq_in_aa(Y, Z))
eq_in_aa(X, X) → eq_out_aa(X, X)
U7_aaa(Y, Z, eq_out_aa(Y, Z)) → tappend_out_aaa(nil, Y, Z)
tappend_in_aaa(T, T1, node(T1, X, T2)) → U8_aaa(T, T1, X, T2, left_in_ag(T, nil))
left_in_ag(nil, nil) → left_out_ag(nil, nil)
left_in_ag(node(L, X9, X10), L) → left_out_ag(node(L, X9, X10), L)
U8_aaa(T, T1, X, T2, left_out_ag(T, nil)) → U9_aaa(T, T1, X, T2, right_in_aa(T, T2))
right_in_aa(nil, nil) → right_out_aa(nil, nil)
right_in_aa(node(X11, X12, R), R) → right_out_aa(node(X11, X12, R), R)
U9_aaa(T, T1, X, T2, right_out_aa(T, T2)) → U10_aaa(T, T1, X, T2, value_in_aa(T, X))
value_in_aa(nil, nil) → value_out_aa(nil, nil)
value_in_aa(node(X13, X, X14), X) → value_out_aa(node(X13, X, X14), X)
U10_aaa(T, T1, X, T2, value_out_aa(T, X)) → tappend_out_aaa(T, T1, node(T1, X, T2))
tappend_in_aaa(T, T2, node(T1, X, T2)) → U11_aaa(T, T2, T1, X, left_in_aa(T, T1))
left_in_aa(nil, nil) → left_out_aa(nil, nil)
left_in_aa(node(L, X9, X10), L) → left_out_aa(node(L, X9, X10), L)
U11_aaa(T, T2, T1, X, left_out_aa(T, T1)) → U12_aaa(T, T2, T1, X, right_in_ag(T, nil))
right_in_ag(nil, nil) → right_out_ag(nil, nil)
right_in_ag(node(X11, X12, R), R) → right_out_ag(node(X11, X12, R), R)
U12_aaa(T, T2, T1, X, right_out_ag(T, nil)) → U13_aaa(T, T2, T1, X, value_in_aa(T, X))
U13_aaa(T, T2, T1, X, value_out_aa(T, X)) → tappend_out_aaa(T, T2, node(T1, X, T2))
tappend_in_aaa(T, T3, node(U, X, T2)) → U14_aaa(T, T3, U, X, T2, left_in_aa(T, T1))
U14_aaa(T, T3, U, X, T2, left_out_aa(T, T1)) → U15_aaa(T, T3, U, X, T2, T1, right_in_aa(T, T2))
U15_aaa(T, T3, U, X, T2, T1, right_out_aa(T, T2)) → U16_aaa(T, T3, U, X, T2, T1, value_in_aa(T, X))
U16_aaa(T, T3, U, X, T2, T1, value_out_aa(T, X)) → U17_aaa(T, T3, U, X, T2, tappend_in_aaa(T1, T3, U))
tappend_in_aaa(T, T1, node(T1, X, U)) → U18_aaa(T, T1, X, U, left_in_aa(T, T1))
U18_aaa(T, T1, X, U, left_out_aa(T, T1)) → U19_aaa(T, T1, X, U, right_in_aa(T, T2))
U19_aaa(T, T1, X, U, right_out_aa(T, T2)) → U20_aaa(T, T1, X, U, T2, value_in_aa(T, X))
U20_aaa(T, T1, X, U, T2, value_out_aa(T, X)) → U21_aaa(T, T1, X, U, tappend_in_aaa(T2, T3, U))
U21_aaa(T, T1, X, U, tappend_out_aaa(T2, T3, U)) → tappend_out_aaa(T, T1, node(T1, X, U))
U17_aaa(T, T3, U, X, T2, tappend_out_aaa(T1, T3, U)) → tappend_out_aaa(T, T3, node(U, X, T2))
U3_aaa(L, X, Last, tappend_out_aaa(L, node(nil, X, nil), LX)) → U4_aaa(L, X, Last, tlast_in_aa(Last, LX))
tlast_in_aa(X, node(nil, X, nil)) → tlast_out_aa(X, node(nil, X, nil))
tlast_in_aa(X, node(L, X1, X2)) → U5_aa(X, L, X1, X2, tlast_in_aa(X, L))
tlast_in_aa(X, node(X3, X4, R)) → U6_aa(X, X3, X4, R, tlast_in_aa(X, R))
U6_aa(X, X3, X4, R, tlast_out_aa(X, R)) → tlast_out_aa(X, node(X3, X4, R))
U5_aa(X, L, X1, X2, tlast_out_aa(X, L)) → tlast_out_aa(X, node(L, X1, X2))
U4_aaa(L, X, Last, tlast_out_aa(Last, LX)) → tapplast_out_aaa(L, X, Last)
U2_gaa(A, B, C, tapplast_out_aaa(T, B, C)) → goal_out_gaa(A, B, C)
GOAL_IN_GAA(A, B, C) → U1_GAA(A, B, C, s2t_in_ga(A, T))
GOAL_IN_GAA(A, B, C) → S2T_IN_GA(A, T)
S2T_IN_GA(0, L) → U22_GA(L, eq_in_ag(L, nil))
S2T_IN_GA(0, L) → EQ_IN_AG(L, nil)
S2T_IN_GA(X, node(T, X5, T)) → U23_GA(X, T, X5, p_in_ga(X, P))
S2T_IN_GA(X, node(T, X5, T)) → P_IN_GA(X, P)
U23_GA(X, T, X5, p_out_ga(X, P)) → U24_GA(X, T, X5, s2t_in_ga(P, T))
U23_GA(X, T, X5, p_out_ga(X, P)) → S2T_IN_GA(P, T)
S2T_IN_GA(X, node(nil, X6, T)) → U25_GA(X, X6, T, p_in_ga(X, P))
S2T_IN_GA(X, node(nil, X6, T)) → P_IN_GA(X, P)
U25_GA(X, X6, T, p_out_ga(X, P)) → U26_GA(X, X6, T, s2t_in_ga(P, T))
U25_GA(X, X6, T, p_out_ga(X, P)) → S2T_IN_GA(P, T)
S2T_IN_GA(X, node(T, X7, nil)) → U27_GA(X, T, X7, p_in_ga(X, P))
S2T_IN_GA(X, node(T, X7, nil)) → P_IN_GA(X, P)
U27_GA(X, T, X7, p_out_ga(X, P)) → U28_GA(X, T, X7, s2t_in_ga(P, T))
U27_GA(X, T, X7, p_out_ga(X, P)) → S2T_IN_GA(P, T)
U1_GAA(A, B, C, s2t_out_ga(A, T)) → U2_GAA(A, B, C, tapplast_in_aaa(T, B, C))
U1_GAA(A, B, C, s2t_out_ga(A, T)) → TAPPLAST_IN_AAA(T, B, C)
TAPPLAST_IN_AAA(L, X, Last) → U3_AAA(L, X, Last, tappend_in_aaa(L, node(nil, X, nil), LX))
TAPPLAST_IN_AAA(L, X, Last) → TAPPEND_IN_AAA(L, node(nil, X, nil), LX)
TAPPEND_IN_AAA(nil, Y, Z) → U7_AAA(Y, Z, eq_in_aa(Y, Z))
TAPPEND_IN_AAA(nil, Y, Z) → EQ_IN_AA(Y, Z)
TAPPEND_IN_AAA(T, T1, node(T1, X, T2)) → U8_AAA(T, T1, X, T2, left_in_ag(T, nil))
TAPPEND_IN_AAA(T, T1, node(T1, X, T2)) → LEFT_IN_AG(T, nil)
U8_AAA(T, T1, X, T2, left_out_ag(T, nil)) → U9_AAA(T, T1, X, T2, right_in_aa(T, T2))
U8_AAA(T, T1, X, T2, left_out_ag(T, nil)) → RIGHT_IN_AA(T, T2)
U9_AAA(T, T1, X, T2, right_out_aa(T, T2)) → U10_AAA(T, T1, X, T2, value_in_aa(T, X))
U9_AAA(T, T1, X, T2, right_out_aa(T, T2)) → VALUE_IN_AA(T, X)
TAPPEND_IN_AAA(T, T2, node(T1, X, T2)) → U11_AAA(T, T2, T1, X, left_in_aa(T, T1))
TAPPEND_IN_AAA(T, T2, node(T1, X, T2)) → LEFT_IN_AA(T, T1)
U11_AAA(T, T2, T1, X, left_out_aa(T, T1)) → U12_AAA(T, T2, T1, X, right_in_ag(T, nil))
U11_AAA(T, T2, T1, X, left_out_aa(T, T1)) → RIGHT_IN_AG(T, nil)
U12_AAA(T, T2, T1, X, right_out_ag(T, nil)) → U13_AAA(T, T2, T1, X, value_in_aa(T, X))
U12_AAA(T, T2, T1, X, right_out_ag(T, nil)) → VALUE_IN_AA(T, X)
TAPPEND_IN_AAA(T, T3, node(U, X, T2)) → U14_AAA(T, T3, U, X, T2, left_in_aa(T, T1))
TAPPEND_IN_AAA(T, T3, node(U, X, T2)) → LEFT_IN_AA(T, T1)
U14_AAA(T, T3, U, X, T2, left_out_aa(T, T1)) → U15_AAA(T, T3, U, X, T2, T1, right_in_aa(T, T2))
U14_AAA(T, T3, U, X, T2, left_out_aa(T, T1)) → RIGHT_IN_AA(T, T2)
U15_AAA(T, T3, U, X, T2, T1, right_out_aa(T, T2)) → U16_AAA(T, T3, U, X, T2, T1, value_in_aa(T, X))
U15_AAA(T, T3, U, X, T2, T1, right_out_aa(T, T2)) → VALUE_IN_AA(T, X)
U16_AAA(T, T3, U, X, T2, T1, value_out_aa(T, X)) → U17_AAA(T, T3, U, X, T2, tappend_in_aaa(T1, T3, U))
U16_AAA(T, T3, U, X, T2, T1, value_out_aa(T, X)) → TAPPEND_IN_AAA(T1, T3, U)
TAPPEND_IN_AAA(T, T1, node(T1, X, U)) → U18_AAA(T, T1, X, U, left_in_aa(T, T1))
TAPPEND_IN_AAA(T, T1, node(T1, X, U)) → LEFT_IN_AA(T, T1)
U18_AAA(T, T1, X, U, left_out_aa(T, T1)) → U19_AAA(T, T1, X, U, right_in_aa(T, T2))
U18_AAA(T, T1, X, U, left_out_aa(T, T1)) → RIGHT_IN_AA(T, T2)
U19_AAA(T, T1, X, U, right_out_aa(T, T2)) → U20_AAA(T, T1, X, U, T2, value_in_aa(T, X))
U19_AAA(T, T1, X, U, right_out_aa(T, T2)) → VALUE_IN_AA(T, X)
U20_AAA(T, T1, X, U, T2, value_out_aa(T, X)) → U21_AAA(T, T1, X, U, tappend_in_aaa(T2, T3, U))
U20_AAA(T, T1, X, U, T2, value_out_aa(T, X)) → TAPPEND_IN_AAA(T2, T3, U)
U3_AAA(L, X, Last, tappend_out_aaa(L, node(nil, X, nil), LX)) → U4_AAA(L, X, Last, tlast_in_aa(Last, LX))
U3_AAA(L, X, Last, tappend_out_aaa(L, node(nil, X, nil), LX)) → TLAST_IN_AA(Last, LX)
TLAST_IN_AA(X, node(L, X1, X2)) → U5_AA(X, L, X1, X2, tlast_in_aa(X, L))
TLAST_IN_AA(X, node(L, X1, X2)) → TLAST_IN_AA(X, L)
TLAST_IN_AA(X, node(X3, X4, R)) → U6_AA(X, X3, X4, R, tlast_in_aa(X, R))
TLAST_IN_AA(X, node(X3, X4, R)) → TLAST_IN_AA(X, R)
goal_in_gaa(A, B, C) → U1_gaa(A, B, C, s2t_in_ga(A, T))
s2t_in_ga(0, L) → U22_ga(L, eq_in_ag(L, nil))
eq_in_ag(X, X) → eq_out_ag(X, X)
U22_ga(L, eq_out_ag(L, nil)) → s2t_out_ga(0, L)
s2t_in_ga(X, node(T, X5, T)) → U23_ga(X, T, X5, p_in_ga(X, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U23_ga(X, T, X5, p_out_ga(X, P)) → U24_ga(X, T, X5, s2t_in_ga(P, T))
s2t_in_ga(X, node(nil, X6, T)) → U25_ga(X, X6, T, p_in_ga(X, P))
U25_ga(X, X6, T, p_out_ga(X, P)) → U26_ga(X, X6, T, s2t_in_ga(P, T))
s2t_in_ga(X, node(T, X7, nil)) → U27_ga(X, T, X7, p_in_ga(X, P))
U27_ga(X, T, X7, p_out_ga(X, P)) → U28_ga(X, T, X7, s2t_in_ga(P, T))
s2t_in_ga(X, node(nil, X8, nil)) → s2t_out_ga(X, node(nil, X8, nil))
U28_ga(X, T, X7, s2t_out_ga(P, T)) → s2t_out_ga(X, node(T, X7, nil))
U26_ga(X, X6, T, s2t_out_ga(P, T)) → s2t_out_ga(X, node(nil, X6, T))
U24_ga(X, T, X5, s2t_out_ga(P, T)) → s2t_out_ga(X, node(T, X5, T))
U1_gaa(A, B, C, s2t_out_ga(A, T)) → U2_gaa(A, B, C, tapplast_in_aaa(T, B, C))
tapplast_in_aaa(L, X, Last) → U3_aaa(L, X, Last, tappend_in_aaa(L, node(nil, X, nil), LX))
tappend_in_aaa(nil, Y, Z) → U7_aaa(Y, Z, eq_in_aa(Y, Z))
eq_in_aa(X, X) → eq_out_aa(X, X)
U7_aaa(Y, Z, eq_out_aa(Y, Z)) → tappend_out_aaa(nil, Y, Z)
tappend_in_aaa(T, T1, node(T1, X, T2)) → U8_aaa(T, T1, X, T2, left_in_ag(T, nil))
left_in_ag(nil, nil) → left_out_ag(nil, nil)
left_in_ag(node(L, X9, X10), L) → left_out_ag(node(L, X9, X10), L)
U8_aaa(T, T1, X, T2, left_out_ag(T, nil)) → U9_aaa(T, T1, X, T2, right_in_aa(T, T2))
right_in_aa(nil, nil) → right_out_aa(nil, nil)
right_in_aa(node(X11, X12, R), R) → right_out_aa(node(X11, X12, R), R)
U9_aaa(T, T1, X, T2, right_out_aa(T, T2)) → U10_aaa(T, T1, X, T2, value_in_aa(T, X))
value_in_aa(nil, nil) → value_out_aa(nil, nil)
value_in_aa(node(X13, X, X14), X) → value_out_aa(node(X13, X, X14), X)
U10_aaa(T, T1, X, T2, value_out_aa(T, X)) → tappend_out_aaa(T, T1, node(T1, X, T2))
tappend_in_aaa(T, T2, node(T1, X, T2)) → U11_aaa(T, T2, T1, X, left_in_aa(T, T1))
left_in_aa(nil, nil) → left_out_aa(nil, nil)
left_in_aa(node(L, X9, X10), L) → left_out_aa(node(L, X9, X10), L)
U11_aaa(T, T2, T1, X, left_out_aa(T, T1)) → U12_aaa(T, T2, T1, X, right_in_ag(T, nil))
right_in_ag(nil, nil) → right_out_ag(nil, nil)
right_in_ag(node(X11, X12, R), R) → right_out_ag(node(X11, X12, R), R)
U12_aaa(T, T2, T1, X, right_out_ag(T, nil)) → U13_aaa(T, T2, T1, X, value_in_aa(T, X))
U13_aaa(T, T2, T1, X, value_out_aa(T, X)) → tappend_out_aaa(T, T2, node(T1, X, T2))
tappend_in_aaa(T, T3, node(U, X, T2)) → U14_aaa(T, T3, U, X, T2, left_in_aa(T, T1))
U14_aaa(T, T3, U, X, T2, left_out_aa(T, T1)) → U15_aaa(T, T3, U, X, T2, T1, right_in_aa(T, T2))
U15_aaa(T, T3, U, X, T2, T1, right_out_aa(T, T2)) → U16_aaa(T, T3, U, X, T2, T1, value_in_aa(T, X))
U16_aaa(T, T3, U, X, T2, T1, value_out_aa(T, X)) → U17_aaa(T, T3, U, X, T2, tappend_in_aaa(T1, T3, U))
tappend_in_aaa(T, T1, node(T1, X, U)) → U18_aaa(T, T1, X, U, left_in_aa(T, T1))
U18_aaa(T, T1, X, U, left_out_aa(T, T1)) → U19_aaa(T, T1, X, U, right_in_aa(T, T2))
U19_aaa(T, T1, X, U, right_out_aa(T, T2)) → U20_aaa(T, T1, X, U, T2, value_in_aa(T, X))
U20_aaa(T, T1, X, U, T2, value_out_aa(T, X)) → U21_aaa(T, T1, X, U, tappend_in_aaa(T2, T3, U))
U21_aaa(T, T1, X, U, tappend_out_aaa(T2, T3, U)) → tappend_out_aaa(T, T1, node(T1, X, U))
U17_aaa(T, T3, U, X, T2, tappend_out_aaa(T1, T3, U)) → tappend_out_aaa(T, T3, node(U, X, T2))
U3_aaa(L, X, Last, tappend_out_aaa(L, node(nil, X, nil), LX)) → U4_aaa(L, X, Last, tlast_in_aa(Last, LX))
tlast_in_aa(X, node(nil, X, nil)) → tlast_out_aa(X, node(nil, X, nil))
tlast_in_aa(X, node(L, X1, X2)) → U5_aa(X, L, X1, X2, tlast_in_aa(X, L))
tlast_in_aa(X, node(X3, X4, R)) → U6_aa(X, X3, X4, R, tlast_in_aa(X, R))
U6_aa(X, X3, X4, R, tlast_out_aa(X, R)) → tlast_out_aa(X, node(X3, X4, R))
U5_aa(X, L, X1, X2, tlast_out_aa(X, L)) → tlast_out_aa(X, node(L, X1, X2))
U4_aaa(L, X, Last, tlast_out_aa(Last, LX)) → tapplast_out_aaa(L, X, Last)
U2_gaa(A, B, C, tapplast_out_aaa(T, B, C)) → goal_out_gaa(A, B, C)
TLAST_IN_AA(X, node(X3, X4, R)) → TLAST_IN_AA(X, R)
TLAST_IN_AA(X, node(L, X1, X2)) → TLAST_IN_AA(X, L)
goal_in_gaa(A, B, C) → U1_gaa(A, B, C, s2t_in_ga(A, T))
s2t_in_ga(0, L) → U22_ga(L, eq_in_ag(L, nil))
eq_in_ag(X, X) → eq_out_ag(X, X)
U22_ga(L, eq_out_ag(L, nil)) → s2t_out_ga(0, L)
s2t_in_ga(X, node(T, X5, T)) → U23_ga(X, T, X5, p_in_ga(X, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U23_ga(X, T, X5, p_out_ga(X, P)) → U24_ga(X, T, X5, s2t_in_ga(P, T))
s2t_in_ga(X, node(nil, X6, T)) → U25_ga(X, X6, T, p_in_ga(X, P))
U25_ga(X, X6, T, p_out_ga(X, P)) → U26_ga(X, X6, T, s2t_in_ga(P, T))
s2t_in_ga(X, node(T, X7, nil)) → U27_ga(X, T, X7, p_in_ga(X, P))
U27_ga(X, T, X7, p_out_ga(X, P)) → U28_ga(X, T, X7, s2t_in_ga(P, T))
s2t_in_ga(X, node(nil, X8, nil)) → s2t_out_ga(X, node(nil, X8, nil))
U28_ga(X, T, X7, s2t_out_ga(P, T)) → s2t_out_ga(X, node(T, X7, nil))
U26_ga(X, X6, T, s2t_out_ga(P, T)) → s2t_out_ga(X, node(nil, X6, T))
U24_ga(X, T, X5, s2t_out_ga(P, T)) → s2t_out_ga(X, node(T, X5, T))
U1_gaa(A, B, C, s2t_out_ga(A, T)) → U2_gaa(A, B, C, tapplast_in_aaa(T, B, C))
tapplast_in_aaa(L, X, Last) → U3_aaa(L, X, Last, tappend_in_aaa(L, node(nil, X, nil), LX))
tappend_in_aaa(nil, Y, Z) → U7_aaa(Y, Z, eq_in_aa(Y, Z))
eq_in_aa(X, X) → eq_out_aa(X, X)
U7_aaa(Y, Z, eq_out_aa(Y, Z)) → tappend_out_aaa(nil, Y, Z)
tappend_in_aaa(T, T1, node(T1, X, T2)) → U8_aaa(T, T1, X, T2, left_in_ag(T, nil))
left_in_ag(nil, nil) → left_out_ag(nil, nil)
left_in_ag(node(L, X9, X10), L) → left_out_ag(node(L, X9, X10), L)
U8_aaa(T, T1, X, T2, left_out_ag(T, nil)) → U9_aaa(T, T1, X, T2, right_in_aa(T, T2))
right_in_aa(nil, nil) → right_out_aa(nil, nil)
right_in_aa(node(X11, X12, R), R) → right_out_aa(node(X11, X12, R), R)
U9_aaa(T, T1, X, T2, right_out_aa(T, T2)) → U10_aaa(T, T1, X, T2, value_in_aa(T, X))
value_in_aa(nil, nil) → value_out_aa(nil, nil)
value_in_aa(node(X13, X, X14), X) → value_out_aa(node(X13, X, X14), X)
U10_aaa(T, T1, X, T2, value_out_aa(T, X)) → tappend_out_aaa(T, T1, node(T1, X, T2))
tappend_in_aaa(T, T2, node(T1, X, T2)) → U11_aaa(T, T2, T1, X, left_in_aa(T, T1))
left_in_aa(nil, nil) → left_out_aa(nil, nil)
left_in_aa(node(L, X9, X10), L) → left_out_aa(node(L, X9, X10), L)
U11_aaa(T, T2, T1, X, left_out_aa(T, T1)) → U12_aaa(T, T2, T1, X, right_in_ag(T, nil))
right_in_ag(nil, nil) → right_out_ag(nil, nil)
right_in_ag(node(X11, X12, R), R) → right_out_ag(node(X11, X12, R), R)
U12_aaa(T, T2, T1, X, right_out_ag(T, nil)) → U13_aaa(T, T2, T1, X, value_in_aa(T, X))
U13_aaa(T, T2, T1, X, value_out_aa(T, X)) → tappend_out_aaa(T, T2, node(T1, X, T2))
tappend_in_aaa(T, T3, node(U, X, T2)) → U14_aaa(T, T3, U, X, T2, left_in_aa(T, T1))
U14_aaa(T, T3, U, X, T2, left_out_aa(T, T1)) → U15_aaa(T, T3, U, X, T2, T1, right_in_aa(T, T2))
U15_aaa(T, T3, U, X, T2, T1, right_out_aa(T, T2)) → U16_aaa(T, T3, U, X, T2, T1, value_in_aa(T, X))
U16_aaa(T, T3, U, X, T2, T1, value_out_aa(T, X)) → U17_aaa(T, T3, U, X, T2, tappend_in_aaa(T1, T3, U))
tappend_in_aaa(T, T1, node(T1, X, U)) → U18_aaa(T, T1, X, U, left_in_aa(T, T1))
U18_aaa(T, T1, X, U, left_out_aa(T, T1)) → U19_aaa(T, T1, X, U, right_in_aa(T, T2))
U19_aaa(T, T1, X, U, right_out_aa(T, T2)) → U20_aaa(T, T1, X, U, T2, value_in_aa(T, X))
U20_aaa(T, T1, X, U, T2, value_out_aa(T, X)) → U21_aaa(T, T1, X, U, tappend_in_aaa(T2, T3, U))
U21_aaa(T, T1, X, U, tappend_out_aaa(T2, T3, U)) → tappend_out_aaa(T, T1, node(T1, X, U))
U17_aaa(T, T3, U, X, T2, tappend_out_aaa(T1, T3, U)) → tappend_out_aaa(T, T3, node(U, X, T2))
U3_aaa(L, X, Last, tappend_out_aaa(L, node(nil, X, nil), LX)) → U4_aaa(L, X, Last, tlast_in_aa(Last, LX))
tlast_in_aa(X, node(nil, X, nil)) → tlast_out_aa(X, node(nil, X, nil))
tlast_in_aa(X, node(L, X1, X2)) → U5_aa(X, L, X1, X2, tlast_in_aa(X, L))
tlast_in_aa(X, node(X3, X4, R)) → U6_aa(X, X3, X4, R, tlast_in_aa(X, R))
U6_aa(X, X3, X4, R, tlast_out_aa(X, R)) → tlast_out_aa(X, node(X3, X4, R))
U5_aa(X, L, X1, X2, tlast_out_aa(X, L)) → tlast_out_aa(X, node(L, X1, X2))
U4_aaa(L, X, Last, tlast_out_aa(Last, LX)) → tapplast_out_aaa(L, X, Last)
U2_gaa(A, B, C, tapplast_out_aaa(T, B, C)) → goal_out_gaa(A, B, C)
TLAST_IN_AA(X, node(X3, X4, R)) → TLAST_IN_AA(X, R)
TLAST_IN_AA(X, node(L, X1, X2)) → TLAST_IN_AA(X, L)
TLAST_IN_AA → TLAST_IN_AA
TAPPEND_IN_AAA(T, T3, node(U, X, T2)) → U14_AAA(T, T3, U, X, T2, left_in_aa(T, T1))
U14_AAA(T, T3, U, X, T2, left_out_aa(T, T1)) → U15_AAA(T, T3, U, X, T2, T1, right_in_aa(T, T2))
U15_AAA(T, T3, U, X, T2, T1, right_out_aa(T, T2)) → U16_AAA(T, T3, U, X, T2, T1, value_in_aa(T, X))
U16_AAA(T, T3, U, X, T2, T1, value_out_aa(T, X)) → TAPPEND_IN_AAA(T1, T3, U)
TAPPEND_IN_AAA(T, T1, node(T1, X, U)) → U18_AAA(T, T1, X, U, left_in_aa(T, T1))
U18_AAA(T, T1, X, U, left_out_aa(T, T1)) → U19_AAA(T, T1, X, U, right_in_aa(T, T2))
U19_AAA(T, T1, X, U, right_out_aa(T, T2)) → U20_AAA(T, T1, X, U, T2, value_in_aa(T, X))
U20_AAA(T, T1, X, U, T2, value_out_aa(T, X)) → TAPPEND_IN_AAA(T2, T3, U)
goal_in_gaa(A, B, C) → U1_gaa(A, B, C, s2t_in_ga(A, T))
s2t_in_ga(0, L) → U22_ga(L, eq_in_ag(L, nil))
eq_in_ag(X, X) → eq_out_ag(X, X)
U22_ga(L, eq_out_ag(L, nil)) → s2t_out_ga(0, L)
s2t_in_ga(X, node(T, X5, T)) → U23_ga(X, T, X5, p_in_ga(X, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U23_ga(X, T, X5, p_out_ga(X, P)) → U24_ga(X, T, X5, s2t_in_ga(P, T))
s2t_in_ga(X, node(nil, X6, T)) → U25_ga(X, X6, T, p_in_ga(X, P))
U25_ga(X, X6, T, p_out_ga(X, P)) → U26_ga(X, X6, T, s2t_in_ga(P, T))
s2t_in_ga(X, node(T, X7, nil)) → U27_ga(X, T, X7, p_in_ga(X, P))
U27_ga(X, T, X7, p_out_ga(X, P)) → U28_ga(X, T, X7, s2t_in_ga(P, T))
s2t_in_ga(X, node(nil, X8, nil)) → s2t_out_ga(X, node(nil, X8, nil))
U28_ga(X, T, X7, s2t_out_ga(P, T)) → s2t_out_ga(X, node(T, X7, nil))
U26_ga(X, X6, T, s2t_out_ga(P, T)) → s2t_out_ga(X, node(nil, X6, T))
U24_ga(X, T, X5, s2t_out_ga(P, T)) → s2t_out_ga(X, node(T, X5, T))
U1_gaa(A, B, C, s2t_out_ga(A, T)) → U2_gaa(A, B, C, tapplast_in_aaa(T, B, C))
tapplast_in_aaa(L, X, Last) → U3_aaa(L, X, Last, tappend_in_aaa(L, node(nil, X, nil), LX))
tappend_in_aaa(nil, Y, Z) → U7_aaa(Y, Z, eq_in_aa(Y, Z))
eq_in_aa(X, X) → eq_out_aa(X, X)
U7_aaa(Y, Z, eq_out_aa(Y, Z)) → tappend_out_aaa(nil, Y, Z)
tappend_in_aaa(T, T1, node(T1, X, T2)) → U8_aaa(T, T1, X, T2, left_in_ag(T, nil))
left_in_ag(nil, nil) → left_out_ag(nil, nil)
left_in_ag(node(L, X9, X10), L) → left_out_ag(node(L, X9, X10), L)
U8_aaa(T, T1, X, T2, left_out_ag(T, nil)) → U9_aaa(T, T1, X, T2, right_in_aa(T, T2))
right_in_aa(nil, nil) → right_out_aa(nil, nil)
right_in_aa(node(X11, X12, R), R) → right_out_aa(node(X11, X12, R), R)
U9_aaa(T, T1, X, T2, right_out_aa(T, T2)) → U10_aaa(T, T1, X, T2, value_in_aa(T, X))
value_in_aa(nil, nil) → value_out_aa(nil, nil)
value_in_aa(node(X13, X, X14), X) → value_out_aa(node(X13, X, X14), X)
U10_aaa(T, T1, X, T2, value_out_aa(T, X)) → tappend_out_aaa(T, T1, node(T1, X, T2))
tappend_in_aaa(T, T2, node(T1, X, T2)) → U11_aaa(T, T2, T1, X, left_in_aa(T, T1))
left_in_aa(nil, nil) → left_out_aa(nil, nil)
left_in_aa(node(L, X9, X10), L) → left_out_aa(node(L, X9, X10), L)
U11_aaa(T, T2, T1, X, left_out_aa(T, T1)) → U12_aaa(T, T2, T1, X, right_in_ag(T, nil))
right_in_ag(nil, nil) → right_out_ag(nil, nil)
right_in_ag(node(X11, X12, R), R) → right_out_ag(node(X11, X12, R), R)
U12_aaa(T, T2, T1, X, right_out_ag(T, nil)) → U13_aaa(T, T2, T1, X, value_in_aa(T, X))
U13_aaa(T, T2, T1, X, value_out_aa(T, X)) → tappend_out_aaa(T, T2, node(T1, X, T2))
tappend_in_aaa(T, T3, node(U, X, T2)) → U14_aaa(T, T3, U, X, T2, left_in_aa(T, T1))
U14_aaa(T, T3, U, X, T2, left_out_aa(T, T1)) → U15_aaa(T, T3, U, X, T2, T1, right_in_aa(T, T2))
U15_aaa(T, T3, U, X, T2, T1, right_out_aa(T, T2)) → U16_aaa(T, T3, U, X, T2, T1, value_in_aa(T, X))
U16_aaa(T, T3, U, X, T2, T1, value_out_aa(T, X)) → U17_aaa(T, T3, U, X, T2, tappend_in_aaa(T1, T3, U))
tappend_in_aaa(T, T1, node(T1, X, U)) → U18_aaa(T, T1, X, U, left_in_aa(T, T1))
U18_aaa(T, T1, X, U, left_out_aa(T, T1)) → U19_aaa(T, T1, X, U, right_in_aa(T, T2))
U19_aaa(T, T1, X, U, right_out_aa(T, T2)) → U20_aaa(T, T1, X, U, T2, value_in_aa(T, X))
U20_aaa(T, T1, X, U, T2, value_out_aa(T, X)) → U21_aaa(T, T1, X, U, tappend_in_aaa(T2, T3, U))
U21_aaa(T, T1, X, U, tappend_out_aaa(T2, T3, U)) → tappend_out_aaa(T, T1, node(T1, X, U))
U17_aaa(T, T3, U, X, T2, tappend_out_aaa(T1, T3, U)) → tappend_out_aaa(T, T3, node(U, X, T2))
U3_aaa(L, X, Last, tappend_out_aaa(L, node(nil, X, nil), LX)) → U4_aaa(L, X, Last, tlast_in_aa(Last, LX))
tlast_in_aa(X, node(nil, X, nil)) → tlast_out_aa(X, node(nil, X, nil))
tlast_in_aa(X, node(L, X1, X2)) → U5_aa(X, L, X1, X2, tlast_in_aa(X, L))
tlast_in_aa(X, node(X3, X4, R)) → U6_aa(X, X3, X4, R, tlast_in_aa(X, R))
U6_aa(X, X3, X4, R, tlast_out_aa(X, R)) → tlast_out_aa(X, node(X3, X4, R))
U5_aa(X, L, X1, X2, tlast_out_aa(X, L)) → tlast_out_aa(X, node(L, X1, X2))
U4_aaa(L, X, Last, tlast_out_aa(Last, LX)) → tapplast_out_aaa(L, X, Last)
U2_gaa(A, B, C, tapplast_out_aaa(T, B, C)) → goal_out_gaa(A, B, C)
TAPPEND_IN_AAA(T, T3, node(U, X, T2)) → U14_AAA(T, T3, U, X, T2, left_in_aa(T, T1))
U14_AAA(T, T3, U, X, T2, left_out_aa(T, T1)) → U15_AAA(T, T3, U, X, T2, T1, right_in_aa(T, T2))
U15_AAA(T, T3, U, X, T2, T1, right_out_aa(T, T2)) → U16_AAA(T, T3, U, X, T2, T1, value_in_aa(T, X))
U16_AAA(T, T3, U, X, T2, T1, value_out_aa(T, X)) → TAPPEND_IN_AAA(T1, T3, U)
TAPPEND_IN_AAA(T, T1, node(T1, X, U)) → U18_AAA(T, T1, X, U, left_in_aa(T, T1))
U18_AAA(T, T1, X, U, left_out_aa(T, T1)) → U19_AAA(T, T1, X, U, right_in_aa(T, T2))
U19_AAA(T, T1, X, U, right_out_aa(T, T2)) → U20_AAA(T, T1, X, U, T2, value_in_aa(T, X))
U20_AAA(T, T1, X, U, T2, value_out_aa(T, X)) → TAPPEND_IN_AAA(T2, T3, U)
left_in_aa(nil, nil) → left_out_aa(nil, nil)
left_in_aa(node(L, X9, X10), L) → left_out_aa(node(L, X9, X10), L)
right_in_aa(nil, nil) → right_out_aa(nil, nil)
right_in_aa(node(X11, X12, R), R) → right_out_aa(node(X11, X12, R), R)
value_in_aa(nil, nil) → value_out_aa(nil, nil)
value_in_aa(node(X13, X, X14), X) → value_out_aa(node(X13, X, X14), X)
TAPPEND_IN_AAA → U14_AAA(left_in_aa)
U14_AAA(left_out_aa) → U15_AAA(right_in_aa)
U15_AAA(right_out_aa) → U16_AAA(value_in_aa)
U16_AAA(value_out_aa) → TAPPEND_IN_AAA
TAPPEND_IN_AAA → U18_AAA(left_in_aa)
U18_AAA(left_out_aa) → U19_AAA(right_in_aa)
U19_AAA(right_out_aa) → U20_AAA(value_in_aa)
U20_AAA(value_out_aa) → TAPPEND_IN_AAA
left_in_aa → left_out_aa
right_in_aa → right_out_aa
value_in_aa → value_out_aa
left_in_aa
right_in_aa
value_in_aa
TAPPEND_IN_AAA → U14_AAA(left_out_aa)
U14_AAA(left_out_aa) → U15_AAA(right_in_aa)
U15_AAA(right_out_aa) → U16_AAA(value_in_aa)
U16_AAA(value_out_aa) → TAPPEND_IN_AAA
TAPPEND_IN_AAA → U18_AAA(left_in_aa)
U18_AAA(left_out_aa) → U19_AAA(right_in_aa)
U19_AAA(right_out_aa) → U20_AAA(value_in_aa)
U20_AAA(value_out_aa) → TAPPEND_IN_AAA
TAPPEND_IN_AAA → U14_AAA(left_out_aa)
left_in_aa → left_out_aa
right_in_aa → right_out_aa
value_in_aa → value_out_aa
left_in_aa
right_in_aa
value_in_aa
U14_AAA(left_out_aa) → U15_AAA(right_out_aa)
U15_AAA(right_out_aa) → U16_AAA(value_in_aa)
U16_AAA(value_out_aa) → TAPPEND_IN_AAA
TAPPEND_IN_AAA → U18_AAA(left_in_aa)
U18_AAA(left_out_aa) → U19_AAA(right_in_aa)
U19_AAA(right_out_aa) → U20_AAA(value_in_aa)
U20_AAA(value_out_aa) → TAPPEND_IN_AAA
TAPPEND_IN_AAA → U14_AAA(left_out_aa)
U14_AAA(left_out_aa) → U15_AAA(right_out_aa)
left_in_aa → left_out_aa
right_in_aa → right_out_aa
value_in_aa → value_out_aa
left_in_aa
right_in_aa
value_in_aa
U15_AAA(right_out_aa) → U16_AAA(value_out_aa)
U16_AAA(value_out_aa) → TAPPEND_IN_AAA
TAPPEND_IN_AAA → U18_AAA(left_in_aa)
U18_AAA(left_out_aa) → U19_AAA(right_in_aa)
U19_AAA(right_out_aa) → U20_AAA(value_in_aa)
U20_AAA(value_out_aa) → TAPPEND_IN_AAA
TAPPEND_IN_AAA → U14_AAA(left_out_aa)
U14_AAA(left_out_aa) → U15_AAA(right_out_aa)
U15_AAA(right_out_aa) → U16_AAA(value_out_aa)
left_in_aa → left_out_aa
right_in_aa → right_out_aa
value_in_aa → value_out_aa
left_in_aa
right_in_aa
value_in_aa
TAPPEND_IN_AAA → U18_AAA(left_out_aa)
U16_AAA(value_out_aa) → TAPPEND_IN_AAA
U18_AAA(left_out_aa) → U19_AAA(right_in_aa)
U19_AAA(right_out_aa) → U20_AAA(value_in_aa)
U20_AAA(value_out_aa) → TAPPEND_IN_AAA
TAPPEND_IN_AAA → U14_AAA(left_out_aa)
U14_AAA(left_out_aa) → U15_AAA(right_out_aa)
U15_AAA(right_out_aa) → U16_AAA(value_out_aa)
TAPPEND_IN_AAA → U18_AAA(left_out_aa)
left_in_aa → left_out_aa
right_in_aa → right_out_aa
value_in_aa → value_out_aa
left_in_aa
right_in_aa
value_in_aa
U16_AAA(value_out_aa) → TAPPEND_IN_AAA
U18_AAA(left_out_aa) → U19_AAA(right_in_aa)
U19_AAA(right_out_aa) → U20_AAA(value_in_aa)
U20_AAA(value_out_aa) → TAPPEND_IN_AAA
TAPPEND_IN_AAA → U14_AAA(left_out_aa)
U14_AAA(left_out_aa) → U15_AAA(right_out_aa)
U15_AAA(right_out_aa) → U16_AAA(value_out_aa)
TAPPEND_IN_AAA → U18_AAA(left_out_aa)
value_in_aa → value_out_aa
right_in_aa → right_out_aa
left_in_aa
right_in_aa
value_in_aa
left_in_aa
U16_AAA(value_out_aa) → TAPPEND_IN_AAA
U18_AAA(left_out_aa) → U19_AAA(right_in_aa)
U19_AAA(right_out_aa) → U20_AAA(value_in_aa)
U20_AAA(value_out_aa) → TAPPEND_IN_AAA
TAPPEND_IN_AAA → U14_AAA(left_out_aa)
U14_AAA(left_out_aa) → U15_AAA(right_out_aa)
U15_AAA(right_out_aa) → U16_AAA(value_out_aa)
TAPPEND_IN_AAA → U18_AAA(left_out_aa)
value_in_aa → value_out_aa
right_in_aa → right_out_aa
right_in_aa
value_in_aa
U18_AAA(left_out_aa) → U19_AAA(right_out_aa)
U16_AAA(value_out_aa) → TAPPEND_IN_AAA
U19_AAA(right_out_aa) → U20_AAA(value_in_aa)
U20_AAA(value_out_aa) → TAPPEND_IN_AAA
TAPPEND_IN_AAA → U14_AAA(left_out_aa)
U14_AAA(left_out_aa) → U15_AAA(right_out_aa)
U15_AAA(right_out_aa) → U16_AAA(value_out_aa)
TAPPEND_IN_AAA → U18_AAA(left_out_aa)
U18_AAA(left_out_aa) → U19_AAA(right_out_aa)
value_in_aa → value_out_aa
right_in_aa → right_out_aa
right_in_aa
value_in_aa
U16_AAA(value_out_aa) → TAPPEND_IN_AAA
U19_AAA(right_out_aa) → U20_AAA(value_in_aa)
U20_AAA(value_out_aa) → TAPPEND_IN_AAA
TAPPEND_IN_AAA → U14_AAA(left_out_aa)
U14_AAA(left_out_aa) → U15_AAA(right_out_aa)
U15_AAA(right_out_aa) → U16_AAA(value_out_aa)
TAPPEND_IN_AAA → U18_AAA(left_out_aa)
U18_AAA(left_out_aa) → U19_AAA(right_out_aa)
value_in_aa → value_out_aa
right_in_aa
value_in_aa
right_in_aa
U16_AAA(value_out_aa) → TAPPEND_IN_AAA
U19_AAA(right_out_aa) → U20_AAA(value_in_aa)
U20_AAA(value_out_aa) → TAPPEND_IN_AAA
TAPPEND_IN_AAA → U14_AAA(left_out_aa)
U14_AAA(left_out_aa) → U15_AAA(right_out_aa)
U15_AAA(right_out_aa) → U16_AAA(value_out_aa)
TAPPEND_IN_AAA → U18_AAA(left_out_aa)
U18_AAA(left_out_aa) → U19_AAA(right_out_aa)
value_in_aa → value_out_aa
value_in_aa
U19_AAA(right_out_aa) → U20_AAA(value_out_aa)
U16_AAA(value_out_aa) → TAPPEND_IN_AAA
U20_AAA(value_out_aa) → TAPPEND_IN_AAA
TAPPEND_IN_AAA → U14_AAA(left_out_aa)
U14_AAA(left_out_aa) → U15_AAA(right_out_aa)
U15_AAA(right_out_aa) → U16_AAA(value_out_aa)
TAPPEND_IN_AAA → U18_AAA(left_out_aa)
U18_AAA(left_out_aa) → U19_AAA(right_out_aa)
U19_AAA(right_out_aa) → U20_AAA(value_out_aa)
value_in_aa → value_out_aa
value_in_aa
U16_AAA(value_out_aa) → TAPPEND_IN_AAA
U20_AAA(value_out_aa) → TAPPEND_IN_AAA
TAPPEND_IN_AAA → U14_AAA(left_out_aa)
U14_AAA(left_out_aa) → U15_AAA(right_out_aa)
U15_AAA(right_out_aa) → U16_AAA(value_out_aa)
TAPPEND_IN_AAA → U18_AAA(left_out_aa)
U18_AAA(left_out_aa) → U19_AAA(right_out_aa)
U19_AAA(right_out_aa) → U20_AAA(value_out_aa)
value_in_aa
value_in_aa
U16_AAA(value_out_aa) → TAPPEND_IN_AAA
U20_AAA(value_out_aa) → TAPPEND_IN_AAA
TAPPEND_IN_AAA → U14_AAA(left_out_aa)
U14_AAA(left_out_aa) → U15_AAA(right_out_aa)
U15_AAA(right_out_aa) → U16_AAA(value_out_aa)
TAPPEND_IN_AAA → U18_AAA(left_out_aa)
U18_AAA(left_out_aa) → U19_AAA(right_out_aa)
U19_AAA(right_out_aa) → U20_AAA(value_out_aa)
S2T_IN_GA(X, node(T, X5, T)) → U23_GA(X, T, X5, p_in_ga(X, P))
U23_GA(X, T, X5, p_out_ga(X, P)) → S2T_IN_GA(P, T)
S2T_IN_GA(X, node(nil, X6, T)) → U25_GA(X, X6, T, p_in_ga(X, P))
U25_GA(X, X6, T, p_out_ga(X, P)) → S2T_IN_GA(P, T)
S2T_IN_GA(X, node(T, X7, nil)) → U27_GA(X, T, X7, p_in_ga(X, P))
U27_GA(X, T, X7, p_out_ga(X, P)) → S2T_IN_GA(P, T)
goal_in_gaa(A, B, C) → U1_gaa(A, B, C, s2t_in_ga(A, T))
s2t_in_ga(0, L) → U22_ga(L, eq_in_ag(L, nil))
eq_in_ag(X, X) → eq_out_ag(X, X)
U22_ga(L, eq_out_ag(L, nil)) → s2t_out_ga(0, L)
s2t_in_ga(X, node(T, X5, T)) → U23_ga(X, T, X5, p_in_ga(X, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U23_ga(X, T, X5, p_out_ga(X, P)) → U24_ga(X, T, X5, s2t_in_ga(P, T))
s2t_in_ga(X, node(nil, X6, T)) → U25_ga(X, X6, T, p_in_ga(X, P))
U25_ga(X, X6, T, p_out_ga(X, P)) → U26_ga(X, X6, T, s2t_in_ga(P, T))
s2t_in_ga(X, node(T, X7, nil)) → U27_ga(X, T, X7, p_in_ga(X, P))
U27_ga(X, T, X7, p_out_ga(X, P)) → U28_ga(X, T, X7, s2t_in_ga(P, T))
s2t_in_ga(X, node(nil, X8, nil)) → s2t_out_ga(X, node(nil, X8, nil))
U28_ga(X, T, X7, s2t_out_ga(P, T)) → s2t_out_ga(X, node(T, X7, nil))
U26_ga(X, X6, T, s2t_out_ga(P, T)) → s2t_out_ga(X, node(nil, X6, T))
U24_ga(X, T, X5, s2t_out_ga(P, T)) → s2t_out_ga(X, node(T, X5, T))
U1_gaa(A, B, C, s2t_out_ga(A, T)) → U2_gaa(A, B, C, tapplast_in_aaa(T, B, C))
tapplast_in_aaa(L, X, Last) → U3_aaa(L, X, Last, tappend_in_aaa(L, node(nil, X, nil), LX))
tappend_in_aaa(nil, Y, Z) → U7_aaa(Y, Z, eq_in_aa(Y, Z))
eq_in_aa(X, X) → eq_out_aa(X, X)
U7_aaa(Y, Z, eq_out_aa(Y, Z)) → tappend_out_aaa(nil, Y, Z)
tappend_in_aaa(T, T1, node(T1, X, T2)) → U8_aaa(T, T1, X, T2, left_in_ag(T, nil))
left_in_ag(nil, nil) → left_out_ag(nil, nil)
left_in_ag(node(L, X9, X10), L) → left_out_ag(node(L, X9, X10), L)
U8_aaa(T, T1, X, T2, left_out_ag(T, nil)) → U9_aaa(T, T1, X, T2, right_in_aa(T, T2))
right_in_aa(nil, nil) → right_out_aa(nil, nil)
right_in_aa(node(X11, X12, R), R) → right_out_aa(node(X11, X12, R), R)
U9_aaa(T, T1, X, T2, right_out_aa(T, T2)) → U10_aaa(T, T1, X, T2, value_in_aa(T, X))
value_in_aa(nil, nil) → value_out_aa(nil, nil)
value_in_aa(node(X13, X, X14), X) → value_out_aa(node(X13, X, X14), X)
U10_aaa(T, T1, X, T2, value_out_aa(T, X)) → tappend_out_aaa(T, T1, node(T1, X, T2))
tappend_in_aaa(T, T2, node(T1, X, T2)) → U11_aaa(T, T2, T1, X, left_in_aa(T, T1))
left_in_aa(nil, nil) → left_out_aa(nil, nil)
left_in_aa(node(L, X9, X10), L) → left_out_aa(node(L, X9, X10), L)
U11_aaa(T, T2, T1, X, left_out_aa(T, T1)) → U12_aaa(T, T2, T1, X, right_in_ag(T, nil))
right_in_ag(nil, nil) → right_out_ag(nil, nil)
right_in_ag(node(X11, X12, R), R) → right_out_ag(node(X11, X12, R), R)
U12_aaa(T, T2, T1, X, right_out_ag(T, nil)) → U13_aaa(T, T2, T1, X, value_in_aa(T, X))
U13_aaa(T, T2, T1, X, value_out_aa(T, X)) → tappend_out_aaa(T, T2, node(T1, X, T2))
tappend_in_aaa(T, T3, node(U, X, T2)) → U14_aaa(T, T3, U, X, T2, left_in_aa(T, T1))
U14_aaa(T, T3, U, X, T2, left_out_aa(T, T1)) → U15_aaa(T, T3, U, X, T2, T1, right_in_aa(T, T2))
U15_aaa(T, T3, U, X, T2, T1, right_out_aa(T, T2)) → U16_aaa(T, T3, U, X, T2, T1, value_in_aa(T, X))
U16_aaa(T, T3, U, X, T2, T1, value_out_aa(T, X)) → U17_aaa(T, T3, U, X, T2, tappend_in_aaa(T1, T3, U))
tappend_in_aaa(T, T1, node(T1, X, U)) → U18_aaa(T, T1, X, U, left_in_aa(T, T1))
U18_aaa(T, T1, X, U, left_out_aa(T, T1)) → U19_aaa(T, T1, X, U, right_in_aa(T, T2))
U19_aaa(T, T1, X, U, right_out_aa(T, T2)) → U20_aaa(T, T1, X, U, T2, value_in_aa(T, X))
U20_aaa(T, T1, X, U, T2, value_out_aa(T, X)) → U21_aaa(T, T1, X, U, tappend_in_aaa(T2, T3, U))
U21_aaa(T, T1, X, U, tappend_out_aaa(T2, T3, U)) → tappend_out_aaa(T, T1, node(T1, X, U))
U17_aaa(T, T3, U, X, T2, tappend_out_aaa(T1, T3, U)) → tappend_out_aaa(T, T3, node(U, X, T2))
U3_aaa(L, X, Last, tappend_out_aaa(L, node(nil, X, nil), LX)) → U4_aaa(L, X, Last, tlast_in_aa(Last, LX))
tlast_in_aa(X, node(nil, X, nil)) → tlast_out_aa(X, node(nil, X, nil))
tlast_in_aa(X, node(L, X1, X2)) → U5_aa(X, L, X1, X2, tlast_in_aa(X, L))
tlast_in_aa(X, node(X3, X4, R)) → U6_aa(X, X3, X4, R, tlast_in_aa(X, R))
U6_aa(X, X3, X4, R, tlast_out_aa(X, R)) → tlast_out_aa(X, node(X3, X4, R))
U5_aa(X, L, X1, X2, tlast_out_aa(X, L)) → tlast_out_aa(X, node(L, X1, X2))
U4_aaa(L, X, Last, tlast_out_aa(Last, LX)) → tapplast_out_aaa(L, X, Last)
U2_gaa(A, B, C, tapplast_out_aaa(T, B, C)) → goal_out_gaa(A, B, C)
S2T_IN_GA(X, node(T, X5, T)) → U23_GA(X, T, X5, p_in_ga(X, P))
U23_GA(X, T, X5, p_out_ga(X, P)) → S2T_IN_GA(P, T)
S2T_IN_GA(X, node(nil, X6, T)) → U25_GA(X, X6, T, p_in_ga(X, P))
U25_GA(X, X6, T, p_out_ga(X, P)) → S2T_IN_GA(P, T)
S2T_IN_GA(X, node(T, X7, nil)) → U27_GA(X, T, X7, p_in_ga(X, P))
U27_GA(X, T, X7, p_out_ga(X, P)) → S2T_IN_GA(P, T)
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
S2T_IN_GA(X) → U23_GA(X, p_in_ga(X))
U23_GA(X, p_out_ga(X, P)) → S2T_IN_GA(P)
S2T_IN_GA(X) → U25_GA(X, p_in_ga(X))
U25_GA(X, p_out_ga(X, P)) → S2T_IN_GA(P)
S2T_IN_GA(X) → U27_GA(X, p_in_ga(X))
U27_GA(X, p_out_ga(X, P)) → S2T_IN_GA(P)
p_in_ga(0) → p_out_ga(0, 0)
p_in_ga(s(X)) → p_out_ga(s(X), X)
p_in_ga(x0)
S2T_IN_GA(0) → U23_GA(0, p_out_ga(0, 0))
S2T_IN_GA(s(x0)) → U23_GA(s(x0), p_out_ga(s(x0), x0))
U23_GA(X, p_out_ga(X, P)) → S2T_IN_GA(P)
S2T_IN_GA(X) → U25_GA(X, p_in_ga(X))
U25_GA(X, p_out_ga(X, P)) → S2T_IN_GA(P)
S2T_IN_GA(X) → U27_GA(X, p_in_ga(X))
U27_GA(X, p_out_ga(X, P)) → S2T_IN_GA(P)
S2T_IN_GA(0) → U23_GA(0, p_out_ga(0, 0))
S2T_IN_GA(s(x0)) → U23_GA(s(x0), p_out_ga(s(x0), x0))
p_in_ga(0) → p_out_ga(0, 0)
p_in_ga(s(X)) → p_out_ga(s(X), X)
p_in_ga(x0)
S2T_IN_GA(0) → U25_GA(0, p_out_ga(0, 0))
S2T_IN_GA(s(x0)) → U25_GA(s(x0), p_out_ga(s(x0), x0))
U23_GA(X, p_out_ga(X, P)) → S2T_IN_GA(P)
U25_GA(X, p_out_ga(X, P)) → S2T_IN_GA(P)
S2T_IN_GA(X) → U27_GA(X, p_in_ga(X))
U27_GA(X, p_out_ga(X, P)) → S2T_IN_GA(P)
S2T_IN_GA(0) → U23_GA(0, p_out_ga(0, 0))
S2T_IN_GA(s(x0)) → U23_GA(s(x0), p_out_ga(s(x0), x0))
S2T_IN_GA(0) → U25_GA(0, p_out_ga(0, 0))
S2T_IN_GA(s(x0)) → U25_GA(s(x0), p_out_ga(s(x0), x0))
p_in_ga(0) → p_out_ga(0, 0)
p_in_ga(s(X)) → p_out_ga(s(X), X)
p_in_ga(x0)
S2T_IN_GA(0) → U27_GA(0, p_out_ga(0, 0))
S2T_IN_GA(s(x0)) → U27_GA(s(x0), p_out_ga(s(x0), x0))
U23_GA(X, p_out_ga(X, P)) → S2T_IN_GA(P)
U25_GA(X, p_out_ga(X, P)) → S2T_IN_GA(P)
U27_GA(X, p_out_ga(X, P)) → S2T_IN_GA(P)
S2T_IN_GA(0) → U23_GA(0, p_out_ga(0, 0))
S2T_IN_GA(s(x0)) → U23_GA(s(x0), p_out_ga(s(x0), x0))
S2T_IN_GA(0) → U25_GA(0, p_out_ga(0, 0))
S2T_IN_GA(s(x0)) → U25_GA(s(x0), p_out_ga(s(x0), x0))
S2T_IN_GA(0) → U27_GA(0, p_out_ga(0, 0))
S2T_IN_GA(s(x0)) → U27_GA(s(x0), p_out_ga(s(x0), x0))
p_in_ga(0) → p_out_ga(0, 0)
p_in_ga(s(X)) → p_out_ga(s(X), X)
p_in_ga(x0)
U23_GA(X, p_out_ga(X, P)) → S2T_IN_GA(P)
U25_GA(X, p_out_ga(X, P)) → S2T_IN_GA(P)
U27_GA(X, p_out_ga(X, P)) → S2T_IN_GA(P)
S2T_IN_GA(0) → U23_GA(0, p_out_ga(0, 0))
S2T_IN_GA(s(x0)) → U23_GA(s(x0), p_out_ga(s(x0), x0))
S2T_IN_GA(0) → U25_GA(0, p_out_ga(0, 0))
S2T_IN_GA(s(x0)) → U25_GA(s(x0), p_out_ga(s(x0), x0))
S2T_IN_GA(0) → U27_GA(0, p_out_ga(0, 0))
S2T_IN_GA(s(x0)) → U27_GA(s(x0), p_out_ga(s(x0), x0))
p_in_ga(x0)
p_in_ga(x0)
U23_GA(X, p_out_ga(X, P)) → S2T_IN_GA(P)
U25_GA(X, p_out_ga(X, P)) → S2T_IN_GA(P)
U27_GA(X, p_out_ga(X, P)) → S2T_IN_GA(P)
S2T_IN_GA(0) → U23_GA(0, p_out_ga(0, 0))
S2T_IN_GA(s(x0)) → U23_GA(s(x0), p_out_ga(s(x0), x0))
S2T_IN_GA(0) → U25_GA(0, p_out_ga(0, 0))
S2T_IN_GA(s(x0)) → U25_GA(s(x0), p_out_ga(s(x0), x0))
S2T_IN_GA(0) → U27_GA(0, p_out_ga(0, 0))
S2T_IN_GA(s(x0)) → U27_GA(s(x0), p_out_ga(s(x0), x0))
U23_GA(0, p_out_ga(0, 0)) → S2T_IN_GA(0)
U23_GA(s(z0), p_out_ga(s(z0), z0)) → S2T_IN_GA(z0)
U25_GA(X, p_out_ga(X, P)) → S2T_IN_GA(P)
U27_GA(X, p_out_ga(X, P)) → S2T_IN_GA(P)
S2T_IN_GA(0) → U23_GA(0, p_out_ga(0, 0))
S2T_IN_GA(s(x0)) → U23_GA(s(x0), p_out_ga(s(x0), x0))
S2T_IN_GA(0) → U25_GA(0, p_out_ga(0, 0))
S2T_IN_GA(s(x0)) → U25_GA(s(x0), p_out_ga(s(x0), x0))
S2T_IN_GA(0) → U27_GA(0, p_out_ga(0, 0))
S2T_IN_GA(s(x0)) → U27_GA(s(x0), p_out_ga(s(x0), x0))
U23_GA(0, p_out_ga(0, 0)) → S2T_IN_GA(0)
U23_GA(s(z0), p_out_ga(s(z0), z0)) → S2T_IN_GA(z0)
U25_GA(0, p_out_ga(0, 0)) → S2T_IN_GA(0)
U25_GA(s(z0), p_out_ga(s(z0), z0)) → S2T_IN_GA(z0)
U27_GA(X, p_out_ga(X, P)) → S2T_IN_GA(P)
S2T_IN_GA(0) → U23_GA(0, p_out_ga(0, 0))
S2T_IN_GA(s(x0)) → U23_GA(s(x0), p_out_ga(s(x0), x0))
S2T_IN_GA(0) → U25_GA(0, p_out_ga(0, 0))
S2T_IN_GA(s(x0)) → U25_GA(s(x0), p_out_ga(s(x0), x0))
S2T_IN_GA(0) → U27_GA(0, p_out_ga(0, 0))
S2T_IN_GA(s(x0)) → U27_GA(s(x0), p_out_ga(s(x0), x0))
U23_GA(0, p_out_ga(0, 0)) → S2T_IN_GA(0)
U23_GA(s(z0), p_out_ga(s(z0), z0)) → S2T_IN_GA(z0)
U25_GA(0, p_out_ga(0, 0)) → S2T_IN_GA(0)
U25_GA(s(z0), p_out_ga(s(z0), z0)) → S2T_IN_GA(z0)
U27_GA(0, p_out_ga(0, 0)) → S2T_IN_GA(0)
U27_GA(s(z0), p_out_ga(s(z0), z0)) → S2T_IN_GA(z0)
S2T_IN_GA(0) → U23_GA(0, p_out_ga(0, 0))
S2T_IN_GA(s(x0)) → U23_GA(s(x0), p_out_ga(s(x0), x0))
S2T_IN_GA(0) → U25_GA(0, p_out_ga(0, 0))
S2T_IN_GA(s(x0)) → U25_GA(s(x0), p_out_ga(s(x0), x0))
S2T_IN_GA(0) → U27_GA(0, p_out_ga(0, 0))
S2T_IN_GA(s(x0)) → U27_GA(s(x0), p_out_ga(s(x0), x0))
U23_GA(0, p_out_ga(0, 0)) → S2T_IN_GA(0)
U23_GA(s(z0), p_out_ga(s(z0), z0)) → S2T_IN_GA(z0)
U25_GA(0, p_out_ga(0, 0)) → S2T_IN_GA(0)
U25_GA(s(z0), p_out_ga(s(z0), z0)) → S2T_IN_GA(z0)
U27_GA(0, p_out_ga(0, 0)) → S2T_IN_GA(0)
U27_GA(s(z0), p_out_ga(s(z0), z0)) → S2T_IN_GA(z0)
U23_GA(0, p_out_ga(0, 0)) → S2T_IN_GA(0)
S2T_IN_GA(0) → U23_GA(0, p_out_ga(0, 0))
S2T_IN_GA(0) → U25_GA(0, p_out_ga(0, 0))
U25_GA(0, p_out_ga(0, 0)) → S2T_IN_GA(0)
S2T_IN_GA(0) → U27_GA(0, p_out_ga(0, 0))
U27_GA(0, p_out_ga(0, 0)) → S2T_IN_GA(0)
S2T_IN_GA(s(x0)) → U23_GA(s(x0), p_out_ga(s(x0), x0))
U23_GA(s(z0), p_out_ga(s(z0), z0)) → S2T_IN_GA(z0)
S2T_IN_GA(s(x0)) → U25_GA(s(x0), p_out_ga(s(x0), x0))
U25_GA(s(z0), p_out_ga(s(z0), z0)) → S2T_IN_GA(z0)
S2T_IN_GA(s(x0)) → U27_GA(s(x0), p_out_ga(s(x0), x0))
U27_GA(s(z0), p_out_ga(s(z0), z0)) → S2T_IN_GA(z0)
From the DPs we obtained the following set of size-change graphs: