0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 67 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 0 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 PiDP
↳7 UsableRulesProof (⇔, 0 ms)
↳8 PiDP
↳9 PiDPToQDPProof (⇒, 0 ms)
↳10 QDP
↳11 QDPSizeChangeProof (⇔, 4 ms)
↳12 YES
flA_in_gga([], [], 0) → flA_out_gga([], [], 0)
flA_in_gga(.(T8, T9), T10, s(T12)) → U1_gga(T8, T9, T10, T12, pB_in_gagga(T8, X13, T10, T9, T12))
pB_in_gagga([], T17, T17, T9, T12) → U2_gagga(T17, T9, T12, flA_in_gga(T9, T17, T12))
U2_gagga(T17, T9, T12, flA_out_gga(T9, T17, T12)) → pB_out_gagga([], T17, T17, T9, T12)
pB_in_gagga(.(T24, T25), X38, .(T24, T26), T9, T12) → U3_gagga(T24, T25, X38, T26, T9, T12, pB_in_gagga(T25, X38, T26, T9, T12))
U3_gagga(T24, T25, X38, T26, T9, T12, pB_out_gagga(T25, X38, T26, T9, T12)) → pB_out_gagga(.(T24, T25), X38, .(T24, T26), T9, T12)
U1_gga(T8, T9, T10, T12, pB_out_gagga(T8, X13, T10, T9, T12)) → flA_out_gga(.(T8, T9), T10, s(T12))
FLA_IN_GGA(.(T8, T9), T10, s(T12)) → U1_GGA(T8, T9, T10, T12, pB_in_gagga(T8, X13, T10, T9, T12))
FLA_IN_GGA(.(T8, T9), T10, s(T12)) → PB_IN_GAGGA(T8, X13, T10, T9, T12)
PB_IN_GAGGA([], T17, T17, T9, T12) → U2_GAGGA(T17, T9, T12, flA_in_gga(T9, T17, T12))
PB_IN_GAGGA([], T17, T17, T9, T12) → FLA_IN_GGA(T9, T17, T12)
PB_IN_GAGGA(.(T24, T25), X38, .(T24, T26), T9, T12) → U3_GAGGA(T24, T25, X38, T26, T9, T12, pB_in_gagga(T25, X38, T26, T9, T12))
PB_IN_GAGGA(.(T24, T25), X38, .(T24, T26), T9, T12) → PB_IN_GAGGA(T25, X38, T26, T9, T12)
flA_in_gga([], [], 0) → flA_out_gga([], [], 0)
flA_in_gga(.(T8, T9), T10, s(T12)) → U1_gga(T8, T9, T10, T12, pB_in_gagga(T8, X13, T10, T9, T12))
pB_in_gagga([], T17, T17, T9, T12) → U2_gagga(T17, T9, T12, flA_in_gga(T9, T17, T12))
U2_gagga(T17, T9, T12, flA_out_gga(T9, T17, T12)) → pB_out_gagga([], T17, T17, T9, T12)
pB_in_gagga(.(T24, T25), X38, .(T24, T26), T9, T12) → U3_gagga(T24, T25, X38, T26, T9, T12, pB_in_gagga(T25, X38, T26, T9, T12))
U3_gagga(T24, T25, X38, T26, T9, T12, pB_out_gagga(T25, X38, T26, T9, T12)) → pB_out_gagga(.(T24, T25), X38, .(T24, T26), T9, T12)
U1_gga(T8, T9, T10, T12, pB_out_gagga(T8, X13, T10, T9, T12)) → flA_out_gga(.(T8, T9), T10, s(T12))
FLA_IN_GGA(.(T8, T9), T10, s(T12)) → U1_GGA(T8, T9, T10, T12, pB_in_gagga(T8, X13, T10, T9, T12))
FLA_IN_GGA(.(T8, T9), T10, s(T12)) → PB_IN_GAGGA(T8, X13, T10, T9, T12)
PB_IN_GAGGA([], T17, T17, T9, T12) → U2_GAGGA(T17, T9, T12, flA_in_gga(T9, T17, T12))
PB_IN_GAGGA([], T17, T17, T9, T12) → FLA_IN_GGA(T9, T17, T12)
PB_IN_GAGGA(.(T24, T25), X38, .(T24, T26), T9, T12) → U3_GAGGA(T24, T25, X38, T26, T9, T12, pB_in_gagga(T25, X38, T26, T9, T12))
PB_IN_GAGGA(.(T24, T25), X38, .(T24, T26), T9, T12) → PB_IN_GAGGA(T25, X38, T26, T9, T12)
flA_in_gga([], [], 0) → flA_out_gga([], [], 0)
flA_in_gga(.(T8, T9), T10, s(T12)) → U1_gga(T8, T9, T10, T12, pB_in_gagga(T8, X13, T10, T9, T12))
pB_in_gagga([], T17, T17, T9, T12) → U2_gagga(T17, T9, T12, flA_in_gga(T9, T17, T12))
U2_gagga(T17, T9, T12, flA_out_gga(T9, T17, T12)) → pB_out_gagga([], T17, T17, T9, T12)
pB_in_gagga(.(T24, T25), X38, .(T24, T26), T9, T12) → U3_gagga(T24, T25, X38, T26, T9, T12, pB_in_gagga(T25, X38, T26, T9, T12))
U3_gagga(T24, T25, X38, T26, T9, T12, pB_out_gagga(T25, X38, T26, T9, T12)) → pB_out_gagga(.(T24, T25), X38, .(T24, T26), T9, T12)
U1_gga(T8, T9, T10, T12, pB_out_gagga(T8, X13, T10, T9, T12)) → flA_out_gga(.(T8, T9), T10, s(T12))
FLA_IN_GGA(.(T8, T9), T10, s(T12)) → PB_IN_GAGGA(T8, X13, T10, T9, T12)
PB_IN_GAGGA([], T17, T17, T9, T12) → FLA_IN_GGA(T9, T17, T12)
PB_IN_GAGGA(.(T24, T25), X38, .(T24, T26), T9, T12) → PB_IN_GAGGA(T25, X38, T26, T9, T12)
flA_in_gga([], [], 0) → flA_out_gga([], [], 0)
flA_in_gga(.(T8, T9), T10, s(T12)) → U1_gga(T8, T9, T10, T12, pB_in_gagga(T8, X13, T10, T9, T12))
pB_in_gagga([], T17, T17, T9, T12) → U2_gagga(T17, T9, T12, flA_in_gga(T9, T17, T12))
U2_gagga(T17, T9, T12, flA_out_gga(T9, T17, T12)) → pB_out_gagga([], T17, T17, T9, T12)
pB_in_gagga(.(T24, T25), X38, .(T24, T26), T9, T12) → U3_gagga(T24, T25, X38, T26, T9, T12, pB_in_gagga(T25, X38, T26, T9, T12))
U3_gagga(T24, T25, X38, T26, T9, T12, pB_out_gagga(T25, X38, T26, T9, T12)) → pB_out_gagga(.(T24, T25), X38, .(T24, T26), T9, T12)
U1_gga(T8, T9, T10, T12, pB_out_gagga(T8, X13, T10, T9, T12)) → flA_out_gga(.(T8, T9), T10, s(T12))
FLA_IN_GGA(.(T8, T9), T10, s(T12)) → PB_IN_GAGGA(T8, X13, T10, T9, T12)
PB_IN_GAGGA([], T17, T17, T9, T12) → FLA_IN_GGA(T9, T17, T12)
PB_IN_GAGGA(.(T24, T25), X38, .(T24, T26), T9, T12) → PB_IN_GAGGA(T25, X38, T26, T9, T12)
FLA_IN_GGA(.(T8, T9), T10) → PB_IN_GAGGA(T8, T10, T9)
PB_IN_GAGGA([], T17, T9) → FLA_IN_GGA(T9, T17)
PB_IN_GAGGA(.(T24, T25), .(T24, T26), T9) → PB_IN_GAGGA(T25, T26, T9)
From the DPs we obtained the following set of size-change graphs: