0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 64 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 15 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 PiDP
↳7 UsableRulesProof (⇔, 0 ms)
↳8 PiDP
↳9 PiDPToQDPProof (⇒, 26 ms)
↳10 QDP
↳11 QDPSizeChangeProof (⇔, 0 ms)
↳12 YES
sumA_in_gag([], [], []) → sumA_out_gag([], [], [])
sumA_in_gag(.(T10, T11), .(T16, T17), .(T14, T15)) → U1_gag(T10, T11, T16, T17, T14, T15, pB_in_gaggag(T10, T16, T14, T11, T17, T15))
pB_in_gaggag(0, T22, T22, T11, T23, T15) → U2_gaggag(T22, T11, T23, T15, sumA_in_gag(T11, T23, T15))
U2_gaggag(T22, T11, T23, T15, sumA_out_gag(T11, T23, T15)) → pB_out_gaggag(0, T22, T22, T11, T23, T15)
pB_in_gaggag(s(T30), T33, s(T32), T11, T34, T15) → U3_gaggag(T30, T33, T32, T11, T34, T15, pB_in_gaggag(T30, T33, T32, T11, T34, T15))
U3_gaggag(T30, T33, T32, T11, T34, T15, pB_out_gaggag(T30, T33, T32, T11, T34, T15)) → pB_out_gaggag(s(T30), T33, s(T32), T11, T34, T15)
U1_gag(T10, T11, T16, T17, T14, T15, pB_out_gaggag(T10, T16, T14, T11, T17, T15)) → sumA_out_gag(.(T10, T11), .(T16, T17), .(T14, T15))
SUMA_IN_GAG(.(T10, T11), .(T16, T17), .(T14, T15)) → U1_GAG(T10, T11, T16, T17, T14, T15, pB_in_gaggag(T10, T16, T14, T11, T17, T15))
SUMA_IN_GAG(.(T10, T11), .(T16, T17), .(T14, T15)) → PB_IN_GAGGAG(T10, T16, T14, T11, T17, T15)
PB_IN_GAGGAG(0, T22, T22, T11, T23, T15) → U2_GAGGAG(T22, T11, T23, T15, sumA_in_gag(T11, T23, T15))
PB_IN_GAGGAG(0, T22, T22, T11, T23, T15) → SUMA_IN_GAG(T11, T23, T15)
PB_IN_GAGGAG(s(T30), T33, s(T32), T11, T34, T15) → U3_GAGGAG(T30, T33, T32, T11, T34, T15, pB_in_gaggag(T30, T33, T32, T11, T34, T15))
PB_IN_GAGGAG(s(T30), T33, s(T32), T11, T34, T15) → PB_IN_GAGGAG(T30, T33, T32, T11, T34, T15)
sumA_in_gag([], [], []) → sumA_out_gag([], [], [])
sumA_in_gag(.(T10, T11), .(T16, T17), .(T14, T15)) → U1_gag(T10, T11, T16, T17, T14, T15, pB_in_gaggag(T10, T16, T14, T11, T17, T15))
pB_in_gaggag(0, T22, T22, T11, T23, T15) → U2_gaggag(T22, T11, T23, T15, sumA_in_gag(T11, T23, T15))
U2_gaggag(T22, T11, T23, T15, sumA_out_gag(T11, T23, T15)) → pB_out_gaggag(0, T22, T22, T11, T23, T15)
pB_in_gaggag(s(T30), T33, s(T32), T11, T34, T15) → U3_gaggag(T30, T33, T32, T11, T34, T15, pB_in_gaggag(T30, T33, T32, T11, T34, T15))
U3_gaggag(T30, T33, T32, T11, T34, T15, pB_out_gaggag(T30, T33, T32, T11, T34, T15)) → pB_out_gaggag(s(T30), T33, s(T32), T11, T34, T15)
U1_gag(T10, T11, T16, T17, T14, T15, pB_out_gaggag(T10, T16, T14, T11, T17, T15)) → sumA_out_gag(.(T10, T11), .(T16, T17), .(T14, T15))
SUMA_IN_GAG(.(T10, T11), .(T16, T17), .(T14, T15)) → U1_GAG(T10, T11, T16, T17, T14, T15, pB_in_gaggag(T10, T16, T14, T11, T17, T15))
SUMA_IN_GAG(.(T10, T11), .(T16, T17), .(T14, T15)) → PB_IN_GAGGAG(T10, T16, T14, T11, T17, T15)
PB_IN_GAGGAG(0, T22, T22, T11, T23, T15) → U2_GAGGAG(T22, T11, T23, T15, sumA_in_gag(T11, T23, T15))
PB_IN_GAGGAG(0, T22, T22, T11, T23, T15) → SUMA_IN_GAG(T11, T23, T15)
PB_IN_GAGGAG(s(T30), T33, s(T32), T11, T34, T15) → U3_GAGGAG(T30, T33, T32, T11, T34, T15, pB_in_gaggag(T30, T33, T32, T11, T34, T15))
PB_IN_GAGGAG(s(T30), T33, s(T32), T11, T34, T15) → PB_IN_GAGGAG(T30, T33, T32, T11, T34, T15)
sumA_in_gag([], [], []) → sumA_out_gag([], [], [])
sumA_in_gag(.(T10, T11), .(T16, T17), .(T14, T15)) → U1_gag(T10, T11, T16, T17, T14, T15, pB_in_gaggag(T10, T16, T14, T11, T17, T15))
pB_in_gaggag(0, T22, T22, T11, T23, T15) → U2_gaggag(T22, T11, T23, T15, sumA_in_gag(T11, T23, T15))
U2_gaggag(T22, T11, T23, T15, sumA_out_gag(T11, T23, T15)) → pB_out_gaggag(0, T22, T22, T11, T23, T15)
pB_in_gaggag(s(T30), T33, s(T32), T11, T34, T15) → U3_gaggag(T30, T33, T32, T11, T34, T15, pB_in_gaggag(T30, T33, T32, T11, T34, T15))
U3_gaggag(T30, T33, T32, T11, T34, T15, pB_out_gaggag(T30, T33, T32, T11, T34, T15)) → pB_out_gaggag(s(T30), T33, s(T32), T11, T34, T15)
U1_gag(T10, T11, T16, T17, T14, T15, pB_out_gaggag(T10, T16, T14, T11, T17, T15)) → sumA_out_gag(.(T10, T11), .(T16, T17), .(T14, T15))
SUMA_IN_GAG(.(T10, T11), .(T16, T17), .(T14, T15)) → PB_IN_GAGGAG(T10, T16, T14, T11, T17, T15)
PB_IN_GAGGAG(0, T22, T22, T11, T23, T15) → SUMA_IN_GAG(T11, T23, T15)
PB_IN_GAGGAG(s(T30), T33, s(T32), T11, T34, T15) → PB_IN_GAGGAG(T30, T33, T32, T11, T34, T15)
sumA_in_gag([], [], []) → sumA_out_gag([], [], [])
sumA_in_gag(.(T10, T11), .(T16, T17), .(T14, T15)) → U1_gag(T10, T11, T16, T17, T14, T15, pB_in_gaggag(T10, T16, T14, T11, T17, T15))
pB_in_gaggag(0, T22, T22, T11, T23, T15) → U2_gaggag(T22, T11, T23, T15, sumA_in_gag(T11, T23, T15))
U2_gaggag(T22, T11, T23, T15, sumA_out_gag(T11, T23, T15)) → pB_out_gaggag(0, T22, T22, T11, T23, T15)
pB_in_gaggag(s(T30), T33, s(T32), T11, T34, T15) → U3_gaggag(T30, T33, T32, T11, T34, T15, pB_in_gaggag(T30, T33, T32, T11, T34, T15))
U3_gaggag(T30, T33, T32, T11, T34, T15, pB_out_gaggag(T30, T33, T32, T11, T34, T15)) → pB_out_gaggag(s(T30), T33, s(T32), T11, T34, T15)
U1_gag(T10, T11, T16, T17, T14, T15, pB_out_gaggag(T10, T16, T14, T11, T17, T15)) → sumA_out_gag(.(T10, T11), .(T16, T17), .(T14, T15))
SUMA_IN_GAG(.(T10, T11), .(T16, T17), .(T14, T15)) → PB_IN_GAGGAG(T10, T16, T14, T11, T17, T15)
PB_IN_GAGGAG(0, T22, T22, T11, T23, T15) → SUMA_IN_GAG(T11, T23, T15)
PB_IN_GAGGAG(s(T30), T33, s(T32), T11, T34, T15) → PB_IN_GAGGAG(T30, T33, T32, T11, T34, T15)
SUMA_IN_GAG(.(T10, T11), .(T14, T15)) → PB_IN_GAGGAG(T10, T14, T11, T15)
PB_IN_GAGGAG(0, T22, T11, T15) → SUMA_IN_GAG(T11, T15)
PB_IN_GAGGAG(s(T30), s(T32), T11, T15) → PB_IN_GAGGAG(T30, T32, T11, T15)
From the DPs we obtained the following set of size-change graphs: