0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 58 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 24 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 PiDP
↳7 UsableRulesProof (⇔, 0 ms)
↳8 PiDP
↳9 PiDPToQDPProof (⇒, 19 ms)
↳10 QDP
↳11 QDPSizeChangeProof (⇔, 0 ms)
↳12 YES
sumA_in_gga([], [], []) → sumA_out_gga([], [], [])
sumA_in_gga(.(T10, T11), .(T12, T13), .(T16, T17)) → U1_gga(T10, T11, T12, T13, T16, T17, pB_in_ggagga(T10, T12, T16, T11, T13, T17))
pB_in_ggagga(0, T22, T22, T11, T13, T23) → U2_ggagga(T22, T11, T13, T23, sumA_in_gga(T11, T13, T23))
U2_ggagga(T22, T11, T13, T23, sumA_out_gga(T11, T13, T23)) → pB_out_ggagga(0, T22, T22, T11, T13, T23)
pB_in_ggagga(s(T30), T31, s(T33), T11, T13, T34) → U3_ggagga(T30, T31, T33, T11, T13, T34, pB_in_ggagga(T30, T31, T33, T11, T13, T34))
U3_ggagga(T30, T31, T33, T11, T13, T34, pB_out_ggagga(T30, T31, T33, T11, T13, T34)) → pB_out_ggagga(s(T30), T31, s(T33), T11, T13, T34)
U1_gga(T10, T11, T12, T13, T16, T17, pB_out_ggagga(T10, T12, T16, T11, T13, T17)) → sumA_out_gga(.(T10, T11), .(T12, T13), .(T16, T17))
SUMA_IN_GGA(.(T10, T11), .(T12, T13), .(T16, T17)) → U1_GGA(T10, T11, T12, T13, T16, T17, pB_in_ggagga(T10, T12, T16, T11, T13, T17))
SUMA_IN_GGA(.(T10, T11), .(T12, T13), .(T16, T17)) → PB_IN_GGAGGA(T10, T12, T16, T11, T13, T17)
PB_IN_GGAGGA(0, T22, T22, T11, T13, T23) → U2_GGAGGA(T22, T11, T13, T23, sumA_in_gga(T11, T13, T23))
PB_IN_GGAGGA(0, T22, T22, T11, T13, T23) → SUMA_IN_GGA(T11, T13, T23)
PB_IN_GGAGGA(s(T30), T31, s(T33), T11, T13, T34) → U3_GGAGGA(T30, T31, T33, T11, T13, T34, pB_in_ggagga(T30, T31, T33, T11, T13, T34))
PB_IN_GGAGGA(s(T30), T31, s(T33), T11, T13, T34) → PB_IN_GGAGGA(T30, T31, T33, T11, T13, T34)
sumA_in_gga([], [], []) → sumA_out_gga([], [], [])
sumA_in_gga(.(T10, T11), .(T12, T13), .(T16, T17)) → U1_gga(T10, T11, T12, T13, T16, T17, pB_in_ggagga(T10, T12, T16, T11, T13, T17))
pB_in_ggagga(0, T22, T22, T11, T13, T23) → U2_ggagga(T22, T11, T13, T23, sumA_in_gga(T11, T13, T23))
U2_ggagga(T22, T11, T13, T23, sumA_out_gga(T11, T13, T23)) → pB_out_ggagga(0, T22, T22, T11, T13, T23)
pB_in_ggagga(s(T30), T31, s(T33), T11, T13, T34) → U3_ggagga(T30, T31, T33, T11, T13, T34, pB_in_ggagga(T30, T31, T33, T11, T13, T34))
U3_ggagga(T30, T31, T33, T11, T13, T34, pB_out_ggagga(T30, T31, T33, T11, T13, T34)) → pB_out_ggagga(s(T30), T31, s(T33), T11, T13, T34)
U1_gga(T10, T11, T12, T13, T16, T17, pB_out_ggagga(T10, T12, T16, T11, T13, T17)) → sumA_out_gga(.(T10, T11), .(T12, T13), .(T16, T17))
SUMA_IN_GGA(.(T10, T11), .(T12, T13), .(T16, T17)) → U1_GGA(T10, T11, T12, T13, T16, T17, pB_in_ggagga(T10, T12, T16, T11, T13, T17))
SUMA_IN_GGA(.(T10, T11), .(T12, T13), .(T16, T17)) → PB_IN_GGAGGA(T10, T12, T16, T11, T13, T17)
PB_IN_GGAGGA(0, T22, T22, T11, T13, T23) → U2_GGAGGA(T22, T11, T13, T23, sumA_in_gga(T11, T13, T23))
PB_IN_GGAGGA(0, T22, T22, T11, T13, T23) → SUMA_IN_GGA(T11, T13, T23)
PB_IN_GGAGGA(s(T30), T31, s(T33), T11, T13, T34) → U3_GGAGGA(T30, T31, T33, T11, T13, T34, pB_in_ggagga(T30, T31, T33, T11, T13, T34))
PB_IN_GGAGGA(s(T30), T31, s(T33), T11, T13, T34) → PB_IN_GGAGGA(T30, T31, T33, T11, T13, T34)
sumA_in_gga([], [], []) → sumA_out_gga([], [], [])
sumA_in_gga(.(T10, T11), .(T12, T13), .(T16, T17)) → U1_gga(T10, T11, T12, T13, T16, T17, pB_in_ggagga(T10, T12, T16, T11, T13, T17))
pB_in_ggagga(0, T22, T22, T11, T13, T23) → U2_ggagga(T22, T11, T13, T23, sumA_in_gga(T11, T13, T23))
U2_ggagga(T22, T11, T13, T23, sumA_out_gga(T11, T13, T23)) → pB_out_ggagga(0, T22, T22, T11, T13, T23)
pB_in_ggagga(s(T30), T31, s(T33), T11, T13, T34) → U3_ggagga(T30, T31, T33, T11, T13, T34, pB_in_ggagga(T30, T31, T33, T11, T13, T34))
U3_ggagga(T30, T31, T33, T11, T13, T34, pB_out_ggagga(T30, T31, T33, T11, T13, T34)) → pB_out_ggagga(s(T30), T31, s(T33), T11, T13, T34)
U1_gga(T10, T11, T12, T13, T16, T17, pB_out_ggagga(T10, T12, T16, T11, T13, T17)) → sumA_out_gga(.(T10, T11), .(T12, T13), .(T16, T17))
SUMA_IN_GGA(.(T10, T11), .(T12, T13), .(T16, T17)) → PB_IN_GGAGGA(T10, T12, T16, T11, T13, T17)
PB_IN_GGAGGA(0, T22, T22, T11, T13, T23) → SUMA_IN_GGA(T11, T13, T23)
PB_IN_GGAGGA(s(T30), T31, s(T33), T11, T13, T34) → PB_IN_GGAGGA(T30, T31, T33, T11, T13, T34)
sumA_in_gga([], [], []) → sumA_out_gga([], [], [])
sumA_in_gga(.(T10, T11), .(T12, T13), .(T16, T17)) → U1_gga(T10, T11, T12, T13, T16, T17, pB_in_ggagga(T10, T12, T16, T11, T13, T17))
pB_in_ggagga(0, T22, T22, T11, T13, T23) → U2_ggagga(T22, T11, T13, T23, sumA_in_gga(T11, T13, T23))
U2_ggagga(T22, T11, T13, T23, sumA_out_gga(T11, T13, T23)) → pB_out_ggagga(0, T22, T22, T11, T13, T23)
pB_in_ggagga(s(T30), T31, s(T33), T11, T13, T34) → U3_ggagga(T30, T31, T33, T11, T13, T34, pB_in_ggagga(T30, T31, T33, T11, T13, T34))
U3_ggagga(T30, T31, T33, T11, T13, T34, pB_out_ggagga(T30, T31, T33, T11, T13, T34)) → pB_out_ggagga(s(T30), T31, s(T33), T11, T13, T34)
U1_gga(T10, T11, T12, T13, T16, T17, pB_out_ggagga(T10, T12, T16, T11, T13, T17)) → sumA_out_gga(.(T10, T11), .(T12, T13), .(T16, T17))
SUMA_IN_GGA(.(T10, T11), .(T12, T13), .(T16, T17)) → PB_IN_GGAGGA(T10, T12, T16, T11, T13, T17)
PB_IN_GGAGGA(0, T22, T22, T11, T13, T23) → SUMA_IN_GGA(T11, T13, T23)
PB_IN_GGAGGA(s(T30), T31, s(T33), T11, T13, T34) → PB_IN_GGAGGA(T30, T31, T33, T11, T13, T34)
SUMA_IN_GGA(.(T10, T11), .(T12, T13)) → PB_IN_GGAGGA(T10, T12, T11, T13)
PB_IN_GGAGGA(0, T22, T11, T13) → SUMA_IN_GGA(T11, T13)
PB_IN_GGAGGA(s(T30), T31, T11, T13) → PB_IN_GGAGGA(T30, T31, T11, T13)
From the DPs we obtained the following set of size-change graphs: