0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 55 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 13 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 PiDP
↳7 UsableRulesProof (⇔, 0 ms)
↳8 PiDP
↳9 PiDPToQDPProof (⇒, 8 ms)
↳10 QDP
↳11 QDPSizeChangeProof (⇔, 0 ms)
↳12 YES
flA_in_gaa([], [], 0) → flA_out_gaa([], [], 0)
flA_in_gaa(.(T8, T9), T12, s(T13)) → U1_gaa(T8, T9, T12, T13, pB_in_gaaga(T8, X13, T12, T9, T13))
pB_in_gaaga([], T19, T19, T9, T20) → U2_gaaga(T19, T9, T20, flA_in_gaa(T9, T19, T20))
U2_gaaga(T19, T9, T20, flA_out_gaa(T9, T19, T20)) → pB_out_gaaga([], T19, T19, T9, T20)
pB_in_gaaga(.(T27, T28), X38, .(T27, T30), T9, T31) → U3_gaaga(T27, T28, X38, T30, T9, T31, pB_in_gaaga(T28, X38, T30, T9, T31))
U3_gaaga(T27, T28, X38, T30, T9, T31, pB_out_gaaga(T28, X38, T30, T9, T31)) → pB_out_gaaga(.(T27, T28), X38, .(T27, T30), T9, T31)
U1_gaa(T8, T9, T12, T13, pB_out_gaaga(T8, X13, T12, T9, T13)) → flA_out_gaa(.(T8, T9), T12, s(T13))
FLA_IN_GAA(.(T8, T9), T12, s(T13)) → U1_GAA(T8, T9, T12, T13, pB_in_gaaga(T8, X13, T12, T9, T13))
FLA_IN_GAA(.(T8, T9), T12, s(T13)) → PB_IN_GAAGA(T8, X13, T12, T9, T13)
PB_IN_GAAGA([], T19, T19, T9, T20) → U2_GAAGA(T19, T9, T20, flA_in_gaa(T9, T19, T20))
PB_IN_GAAGA([], T19, T19, T9, T20) → FLA_IN_GAA(T9, T19, T20)
PB_IN_GAAGA(.(T27, T28), X38, .(T27, T30), T9, T31) → U3_GAAGA(T27, T28, X38, T30, T9, T31, pB_in_gaaga(T28, X38, T30, T9, T31))
PB_IN_GAAGA(.(T27, T28), X38, .(T27, T30), T9, T31) → PB_IN_GAAGA(T28, X38, T30, T9, T31)
flA_in_gaa([], [], 0) → flA_out_gaa([], [], 0)
flA_in_gaa(.(T8, T9), T12, s(T13)) → U1_gaa(T8, T9, T12, T13, pB_in_gaaga(T8, X13, T12, T9, T13))
pB_in_gaaga([], T19, T19, T9, T20) → U2_gaaga(T19, T9, T20, flA_in_gaa(T9, T19, T20))
U2_gaaga(T19, T9, T20, flA_out_gaa(T9, T19, T20)) → pB_out_gaaga([], T19, T19, T9, T20)
pB_in_gaaga(.(T27, T28), X38, .(T27, T30), T9, T31) → U3_gaaga(T27, T28, X38, T30, T9, T31, pB_in_gaaga(T28, X38, T30, T9, T31))
U3_gaaga(T27, T28, X38, T30, T9, T31, pB_out_gaaga(T28, X38, T30, T9, T31)) → pB_out_gaaga(.(T27, T28), X38, .(T27, T30), T9, T31)
U1_gaa(T8, T9, T12, T13, pB_out_gaaga(T8, X13, T12, T9, T13)) → flA_out_gaa(.(T8, T9), T12, s(T13))
FLA_IN_GAA(.(T8, T9), T12, s(T13)) → U1_GAA(T8, T9, T12, T13, pB_in_gaaga(T8, X13, T12, T9, T13))
FLA_IN_GAA(.(T8, T9), T12, s(T13)) → PB_IN_GAAGA(T8, X13, T12, T9, T13)
PB_IN_GAAGA([], T19, T19, T9, T20) → U2_GAAGA(T19, T9, T20, flA_in_gaa(T9, T19, T20))
PB_IN_GAAGA([], T19, T19, T9, T20) → FLA_IN_GAA(T9, T19, T20)
PB_IN_GAAGA(.(T27, T28), X38, .(T27, T30), T9, T31) → U3_GAAGA(T27, T28, X38, T30, T9, T31, pB_in_gaaga(T28, X38, T30, T9, T31))
PB_IN_GAAGA(.(T27, T28), X38, .(T27, T30), T9, T31) → PB_IN_GAAGA(T28, X38, T30, T9, T31)
flA_in_gaa([], [], 0) → flA_out_gaa([], [], 0)
flA_in_gaa(.(T8, T9), T12, s(T13)) → U1_gaa(T8, T9, T12, T13, pB_in_gaaga(T8, X13, T12, T9, T13))
pB_in_gaaga([], T19, T19, T9, T20) → U2_gaaga(T19, T9, T20, flA_in_gaa(T9, T19, T20))
U2_gaaga(T19, T9, T20, flA_out_gaa(T9, T19, T20)) → pB_out_gaaga([], T19, T19, T9, T20)
pB_in_gaaga(.(T27, T28), X38, .(T27, T30), T9, T31) → U3_gaaga(T27, T28, X38, T30, T9, T31, pB_in_gaaga(T28, X38, T30, T9, T31))
U3_gaaga(T27, T28, X38, T30, T9, T31, pB_out_gaaga(T28, X38, T30, T9, T31)) → pB_out_gaaga(.(T27, T28), X38, .(T27, T30), T9, T31)
U1_gaa(T8, T9, T12, T13, pB_out_gaaga(T8, X13, T12, T9, T13)) → flA_out_gaa(.(T8, T9), T12, s(T13))
FLA_IN_GAA(.(T8, T9), T12, s(T13)) → PB_IN_GAAGA(T8, X13, T12, T9, T13)
PB_IN_GAAGA([], T19, T19, T9, T20) → FLA_IN_GAA(T9, T19, T20)
PB_IN_GAAGA(.(T27, T28), X38, .(T27, T30), T9, T31) → PB_IN_GAAGA(T28, X38, T30, T9, T31)
flA_in_gaa([], [], 0) → flA_out_gaa([], [], 0)
flA_in_gaa(.(T8, T9), T12, s(T13)) → U1_gaa(T8, T9, T12, T13, pB_in_gaaga(T8, X13, T12, T9, T13))
pB_in_gaaga([], T19, T19, T9, T20) → U2_gaaga(T19, T9, T20, flA_in_gaa(T9, T19, T20))
U2_gaaga(T19, T9, T20, flA_out_gaa(T9, T19, T20)) → pB_out_gaaga([], T19, T19, T9, T20)
pB_in_gaaga(.(T27, T28), X38, .(T27, T30), T9, T31) → U3_gaaga(T27, T28, X38, T30, T9, T31, pB_in_gaaga(T28, X38, T30, T9, T31))
U3_gaaga(T27, T28, X38, T30, T9, T31, pB_out_gaaga(T28, X38, T30, T9, T31)) → pB_out_gaaga(.(T27, T28), X38, .(T27, T30), T9, T31)
U1_gaa(T8, T9, T12, T13, pB_out_gaaga(T8, X13, T12, T9, T13)) → flA_out_gaa(.(T8, T9), T12, s(T13))
FLA_IN_GAA(.(T8, T9), T12, s(T13)) → PB_IN_GAAGA(T8, X13, T12, T9, T13)
PB_IN_GAAGA([], T19, T19, T9, T20) → FLA_IN_GAA(T9, T19, T20)
PB_IN_GAAGA(.(T27, T28), X38, .(T27, T30), T9, T31) → PB_IN_GAAGA(T28, X38, T30, T9, T31)
FLA_IN_GAA(.(T8, T9)) → PB_IN_GAAGA(T8, T9)
PB_IN_GAAGA([], T9) → FLA_IN_GAA(T9)
PB_IN_GAAGA(.(T27, T28), T9) → PB_IN_GAAGA(T28, T9)
From the DPs we obtained the following set of size-change graphs: