0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 155 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 22 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 PiDP
↳7 UsableRulesProof (⇔, 0 ms)
↳8 PiDP
↳9 PiDPToQDPProof (⇒, 29 ms)
↳10 QDP
↳11 QDPSizeChangeProof (⇔, 0 ms)
↳12 YES
fA_in_gga(T5, [], T5) → fA_out_gga(T5, [], T5)
fA_in_gga(.(T9, []), [], []) → fA_out_gga(.(T9, []), [], [])
fA_in_gga(.(T9, .(T25, T26)), [], T28) → U1_gga(T9, T25, T26, T28, fA_in_gga(.(T25, T26), T26, T28))
fA_in_gga([], .(T48, []), .(T48, [])) → fA_out_gga([], .(T48, []), .(T48, []))
fA_in_gga([], .(T68, []), []) → fA_out_gga([], .(T68, []), [])
fA_in_gga([], .(T68, .(T85, T86)), T88) → U2_gga(T68, T85, T86, T88, fA_in_gga(.(T85, T86), T86, T88))
fA_in_gga(.(T97, []), T106, T106) → fA_out_gga(.(T97, []), T106, T106)
fA_in_gga(.(T97, .(T119, T120)), [], T122) → U3_gga(T97, T119, T120, T122, fA_in_gga(.(T119, T120), T120, T122))
fA_in_gga(.(T97, T137), .(T135, T136), T139) → U4_gga(T97, T137, T135, T136, T139, fA_in_gga(T137, T136, T139))
U4_gga(T97, T137, T135, T136, T139, fA_out_gga(T137, T136, T139)) → fA_out_gga(.(T97, T137), .(T135, T136), T139)
U3_gga(T97, T119, T120, T122, fA_out_gga(.(T119, T120), T120, T122)) → fA_out_gga(.(T97, .(T119, T120)), [], T122)
U2_gga(T68, T85, T86, T88, fA_out_gga(.(T85, T86), T86, T88)) → fA_out_gga([], .(T68, .(T85, T86)), T88)
U1_gga(T9, T25, T26, T28, fA_out_gga(.(T25, T26), T26, T28)) → fA_out_gga(.(T9, .(T25, T26)), [], T28)
FA_IN_GGA(.(T9, .(T25, T26)), [], T28) → U1_GGA(T9, T25, T26, T28, fA_in_gga(.(T25, T26), T26, T28))
FA_IN_GGA(.(T9, .(T25, T26)), [], T28) → FA_IN_GGA(.(T25, T26), T26, T28)
FA_IN_GGA([], .(T68, .(T85, T86)), T88) → U2_GGA(T68, T85, T86, T88, fA_in_gga(.(T85, T86), T86, T88))
FA_IN_GGA([], .(T68, .(T85, T86)), T88) → FA_IN_GGA(.(T85, T86), T86, T88)
FA_IN_GGA(.(T97, .(T119, T120)), [], T122) → U3_GGA(T97, T119, T120, T122, fA_in_gga(.(T119, T120), T120, T122))
FA_IN_GGA(.(T97, T137), .(T135, T136), T139) → U4_GGA(T97, T137, T135, T136, T139, fA_in_gga(T137, T136, T139))
FA_IN_GGA(.(T97, T137), .(T135, T136), T139) → FA_IN_GGA(T137, T136, T139)
fA_in_gga(T5, [], T5) → fA_out_gga(T5, [], T5)
fA_in_gga(.(T9, []), [], []) → fA_out_gga(.(T9, []), [], [])
fA_in_gga(.(T9, .(T25, T26)), [], T28) → U1_gga(T9, T25, T26, T28, fA_in_gga(.(T25, T26), T26, T28))
fA_in_gga([], .(T48, []), .(T48, [])) → fA_out_gga([], .(T48, []), .(T48, []))
fA_in_gga([], .(T68, []), []) → fA_out_gga([], .(T68, []), [])
fA_in_gga([], .(T68, .(T85, T86)), T88) → U2_gga(T68, T85, T86, T88, fA_in_gga(.(T85, T86), T86, T88))
fA_in_gga(.(T97, []), T106, T106) → fA_out_gga(.(T97, []), T106, T106)
fA_in_gga(.(T97, .(T119, T120)), [], T122) → U3_gga(T97, T119, T120, T122, fA_in_gga(.(T119, T120), T120, T122))
fA_in_gga(.(T97, T137), .(T135, T136), T139) → U4_gga(T97, T137, T135, T136, T139, fA_in_gga(T137, T136, T139))
U4_gga(T97, T137, T135, T136, T139, fA_out_gga(T137, T136, T139)) → fA_out_gga(.(T97, T137), .(T135, T136), T139)
U3_gga(T97, T119, T120, T122, fA_out_gga(.(T119, T120), T120, T122)) → fA_out_gga(.(T97, .(T119, T120)), [], T122)
U2_gga(T68, T85, T86, T88, fA_out_gga(.(T85, T86), T86, T88)) → fA_out_gga([], .(T68, .(T85, T86)), T88)
U1_gga(T9, T25, T26, T28, fA_out_gga(.(T25, T26), T26, T28)) → fA_out_gga(.(T9, .(T25, T26)), [], T28)
FA_IN_GGA(.(T9, .(T25, T26)), [], T28) → U1_GGA(T9, T25, T26, T28, fA_in_gga(.(T25, T26), T26, T28))
FA_IN_GGA(.(T9, .(T25, T26)), [], T28) → FA_IN_GGA(.(T25, T26), T26, T28)
FA_IN_GGA([], .(T68, .(T85, T86)), T88) → U2_GGA(T68, T85, T86, T88, fA_in_gga(.(T85, T86), T86, T88))
FA_IN_GGA([], .(T68, .(T85, T86)), T88) → FA_IN_GGA(.(T85, T86), T86, T88)
FA_IN_GGA(.(T97, .(T119, T120)), [], T122) → U3_GGA(T97, T119, T120, T122, fA_in_gga(.(T119, T120), T120, T122))
FA_IN_GGA(.(T97, T137), .(T135, T136), T139) → U4_GGA(T97, T137, T135, T136, T139, fA_in_gga(T137, T136, T139))
FA_IN_GGA(.(T97, T137), .(T135, T136), T139) → FA_IN_GGA(T137, T136, T139)
fA_in_gga(T5, [], T5) → fA_out_gga(T5, [], T5)
fA_in_gga(.(T9, []), [], []) → fA_out_gga(.(T9, []), [], [])
fA_in_gga(.(T9, .(T25, T26)), [], T28) → U1_gga(T9, T25, T26, T28, fA_in_gga(.(T25, T26), T26, T28))
fA_in_gga([], .(T48, []), .(T48, [])) → fA_out_gga([], .(T48, []), .(T48, []))
fA_in_gga([], .(T68, []), []) → fA_out_gga([], .(T68, []), [])
fA_in_gga([], .(T68, .(T85, T86)), T88) → U2_gga(T68, T85, T86, T88, fA_in_gga(.(T85, T86), T86, T88))
fA_in_gga(.(T97, []), T106, T106) → fA_out_gga(.(T97, []), T106, T106)
fA_in_gga(.(T97, .(T119, T120)), [], T122) → U3_gga(T97, T119, T120, T122, fA_in_gga(.(T119, T120), T120, T122))
fA_in_gga(.(T97, T137), .(T135, T136), T139) → U4_gga(T97, T137, T135, T136, T139, fA_in_gga(T137, T136, T139))
U4_gga(T97, T137, T135, T136, T139, fA_out_gga(T137, T136, T139)) → fA_out_gga(.(T97, T137), .(T135, T136), T139)
U3_gga(T97, T119, T120, T122, fA_out_gga(.(T119, T120), T120, T122)) → fA_out_gga(.(T97, .(T119, T120)), [], T122)
U2_gga(T68, T85, T86, T88, fA_out_gga(.(T85, T86), T86, T88)) → fA_out_gga([], .(T68, .(T85, T86)), T88)
U1_gga(T9, T25, T26, T28, fA_out_gga(.(T25, T26), T26, T28)) → fA_out_gga(.(T9, .(T25, T26)), [], T28)
FA_IN_GGA(.(T97, T137), .(T135, T136), T139) → FA_IN_GGA(T137, T136, T139)
FA_IN_GGA(.(T9, .(T25, T26)), [], T28) → FA_IN_GGA(.(T25, T26), T26, T28)
FA_IN_GGA([], .(T68, .(T85, T86)), T88) → FA_IN_GGA(.(T85, T86), T86, T88)
fA_in_gga(T5, [], T5) → fA_out_gga(T5, [], T5)
fA_in_gga(.(T9, []), [], []) → fA_out_gga(.(T9, []), [], [])
fA_in_gga(.(T9, .(T25, T26)), [], T28) → U1_gga(T9, T25, T26, T28, fA_in_gga(.(T25, T26), T26, T28))
fA_in_gga([], .(T48, []), .(T48, [])) → fA_out_gga([], .(T48, []), .(T48, []))
fA_in_gga([], .(T68, []), []) → fA_out_gga([], .(T68, []), [])
fA_in_gga([], .(T68, .(T85, T86)), T88) → U2_gga(T68, T85, T86, T88, fA_in_gga(.(T85, T86), T86, T88))
fA_in_gga(.(T97, []), T106, T106) → fA_out_gga(.(T97, []), T106, T106)
fA_in_gga(.(T97, .(T119, T120)), [], T122) → U3_gga(T97, T119, T120, T122, fA_in_gga(.(T119, T120), T120, T122))
fA_in_gga(.(T97, T137), .(T135, T136), T139) → U4_gga(T97, T137, T135, T136, T139, fA_in_gga(T137, T136, T139))
U4_gga(T97, T137, T135, T136, T139, fA_out_gga(T137, T136, T139)) → fA_out_gga(.(T97, T137), .(T135, T136), T139)
U3_gga(T97, T119, T120, T122, fA_out_gga(.(T119, T120), T120, T122)) → fA_out_gga(.(T97, .(T119, T120)), [], T122)
U2_gga(T68, T85, T86, T88, fA_out_gga(.(T85, T86), T86, T88)) → fA_out_gga([], .(T68, .(T85, T86)), T88)
U1_gga(T9, T25, T26, T28, fA_out_gga(.(T25, T26), T26, T28)) → fA_out_gga(.(T9, .(T25, T26)), [], T28)
FA_IN_GGA(.(T97, T137), .(T135, T136), T139) → FA_IN_GGA(T137, T136, T139)
FA_IN_GGA(.(T9, .(T25, T26)), [], T28) → FA_IN_GGA(.(T25, T26), T26, T28)
FA_IN_GGA([], .(T68, .(T85, T86)), T88) → FA_IN_GGA(.(T85, T86), T86, T88)
FA_IN_GGA(.(T97, T137), .(T135, T136)) → FA_IN_GGA(T137, T136)
FA_IN_GGA(.(T9, .(T25, T26)), []) → FA_IN_GGA(.(T25, T26), T26)
FA_IN_GGA([], .(T68, .(T85, T86))) → FA_IN_GGA(.(T85, T86), T86)
From the DPs we obtained the following set of size-change graphs: