0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 0 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 9 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 0 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 PiDP
↳9 UsableRulesProof (⇔, 0 ms)
↳10 PiDP
↳11 PiDPToQDPProof (⇒, 7 ms)
↳12 QDP
↳13 QDPSizeChangeProof (⇔, 0 ms)
↳14 YES
sumB_in_gag([], [], []) → sumB_out_gag([], [], [])
sumB_in_gag(.(T10, T11), .(T16, T17), .(T14, T15)) → U3_gag(T10, T11, T16, T17, T14, T15, pA_in_gaggag(T10, T16, T14, T11, T17, T15))
pA_in_gaggag(0, T22, T22, T11, T23, T15) → U1_gaggag(T22, T11, T23, T15, sumB_in_gag(T11, T23, T15))
U1_gaggag(T22, T11, T23, T15, sumB_out_gag(T11, T23, T15)) → pA_out_gaggag(0, T22, T22, T11, T23, T15)
pA_in_gaggag(s(T30), T33, s(T32), T11, T34, T15) → U2_gaggag(T30, T33, T32, T11, T34, T15, pA_in_gaggag(T30, T33, T32, T11, T34, T15))
U2_gaggag(T30, T33, T32, T11, T34, T15, pA_out_gaggag(T30, T33, T32, T11, T34, T15)) → pA_out_gaggag(s(T30), T33, s(T32), T11, T34, T15)
U3_gag(T10, T11, T16, T17, T14, T15, pA_out_gaggag(T10, T16, T14, T11, T17, T15)) → sumB_out_gag(.(T10, T11), .(T16, T17), .(T14, T15))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
sumB_in_gag([], [], []) → sumB_out_gag([], [], [])
sumB_in_gag(.(T10, T11), .(T16, T17), .(T14, T15)) → U3_gag(T10, T11, T16, T17, T14, T15, pA_in_gaggag(T10, T16, T14, T11, T17, T15))
pA_in_gaggag(0, T22, T22, T11, T23, T15) → U1_gaggag(T22, T11, T23, T15, sumB_in_gag(T11, T23, T15))
U1_gaggag(T22, T11, T23, T15, sumB_out_gag(T11, T23, T15)) → pA_out_gaggag(0, T22, T22, T11, T23, T15)
pA_in_gaggag(s(T30), T33, s(T32), T11, T34, T15) → U2_gaggag(T30, T33, T32, T11, T34, T15, pA_in_gaggag(T30, T33, T32, T11, T34, T15))
U2_gaggag(T30, T33, T32, T11, T34, T15, pA_out_gaggag(T30, T33, T32, T11, T34, T15)) → pA_out_gaggag(s(T30), T33, s(T32), T11, T34, T15)
U3_gag(T10, T11, T16, T17, T14, T15, pA_out_gaggag(T10, T16, T14, T11, T17, T15)) → sumB_out_gag(.(T10, T11), .(T16, T17), .(T14, T15))
SUMB_IN_GAG(.(T10, T11), .(T16, T17), .(T14, T15)) → U3_GAG(T10, T11, T16, T17, T14, T15, pA_in_gaggag(T10, T16, T14, T11, T17, T15))
SUMB_IN_GAG(.(T10, T11), .(T16, T17), .(T14, T15)) → PA_IN_GAGGAG(T10, T16, T14, T11, T17, T15)
PA_IN_GAGGAG(0, T22, T22, T11, T23, T15) → U1_GAGGAG(T22, T11, T23, T15, sumB_in_gag(T11, T23, T15))
PA_IN_GAGGAG(0, T22, T22, T11, T23, T15) → SUMB_IN_GAG(T11, T23, T15)
PA_IN_GAGGAG(s(T30), T33, s(T32), T11, T34, T15) → U2_GAGGAG(T30, T33, T32, T11, T34, T15, pA_in_gaggag(T30, T33, T32, T11, T34, T15))
PA_IN_GAGGAG(s(T30), T33, s(T32), T11, T34, T15) → PA_IN_GAGGAG(T30, T33, T32, T11, T34, T15)
sumB_in_gag([], [], []) → sumB_out_gag([], [], [])
sumB_in_gag(.(T10, T11), .(T16, T17), .(T14, T15)) → U3_gag(T10, T11, T16, T17, T14, T15, pA_in_gaggag(T10, T16, T14, T11, T17, T15))
pA_in_gaggag(0, T22, T22, T11, T23, T15) → U1_gaggag(T22, T11, T23, T15, sumB_in_gag(T11, T23, T15))
U1_gaggag(T22, T11, T23, T15, sumB_out_gag(T11, T23, T15)) → pA_out_gaggag(0, T22, T22, T11, T23, T15)
pA_in_gaggag(s(T30), T33, s(T32), T11, T34, T15) → U2_gaggag(T30, T33, T32, T11, T34, T15, pA_in_gaggag(T30, T33, T32, T11, T34, T15))
U2_gaggag(T30, T33, T32, T11, T34, T15, pA_out_gaggag(T30, T33, T32, T11, T34, T15)) → pA_out_gaggag(s(T30), T33, s(T32), T11, T34, T15)
U3_gag(T10, T11, T16, T17, T14, T15, pA_out_gaggag(T10, T16, T14, T11, T17, T15)) → sumB_out_gag(.(T10, T11), .(T16, T17), .(T14, T15))
SUMB_IN_GAG(.(T10, T11), .(T16, T17), .(T14, T15)) → U3_GAG(T10, T11, T16, T17, T14, T15, pA_in_gaggag(T10, T16, T14, T11, T17, T15))
SUMB_IN_GAG(.(T10, T11), .(T16, T17), .(T14, T15)) → PA_IN_GAGGAG(T10, T16, T14, T11, T17, T15)
PA_IN_GAGGAG(0, T22, T22, T11, T23, T15) → U1_GAGGAG(T22, T11, T23, T15, sumB_in_gag(T11, T23, T15))
PA_IN_GAGGAG(0, T22, T22, T11, T23, T15) → SUMB_IN_GAG(T11, T23, T15)
PA_IN_GAGGAG(s(T30), T33, s(T32), T11, T34, T15) → U2_GAGGAG(T30, T33, T32, T11, T34, T15, pA_in_gaggag(T30, T33, T32, T11, T34, T15))
PA_IN_GAGGAG(s(T30), T33, s(T32), T11, T34, T15) → PA_IN_GAGGAG(T30, T33, T32, T11, T34, T15)
sumB_in_gag([], [], []) → sumB_out_gag([], [], [])
sumB_in_gag(.(T10, T11), .(T16, T17), .(T14, T15)) → U3_gag(T10, T11, T16, T17, T14, T15, pA_in_gaggag(T10, T16, T14, T11, T17, T15))
pA_in_gaggag(0, T22, T22, T11, T23, T15) → U1_gaggag(T22, T11, T23, T15, sumB_in_gag(T11, T23, T15))
U1_gaggag(T22, T11, T23, T15, sumB_out_gag(T11, T23, T15)) → pA_out_gaggag(0, T22, T22, T11, T23, T15)
pA_in_gaggag(s(T30), T33, s(T32), T11, T34, T15) → U2_gaggag(T30, T33, T32, T11, T34, T15, pA_in_gaggag(T30, T33, T32, T11, T34, T15))
U2_gaggag(T30, T33, T32, T11, T34, T15, pA_out_gaggag(T30, T33, T32, T11, T34, T15)) → pA_out_gaggag(s(T30), T33, s(T32), T11, T34, T15)
U3_gag(T10, T11, T16, T17, T14, T15, pA_out_gaggag(T10, T16, T14, T11, T17, T15)) → sumB_out_gag(.(T10, T11), .(T16, T17), .(T14, T15))
SUMB_IN_GAG(.(T10, T11), .(T16, T17), .(T14, T15)) → PA_IN_GAGGAG(T10, T16, T14, T11, T17, T15)
PA_IN_GAGGAG(0, T22, T22, T11, T23, T15) → SUMB_IN_GAG(T11, T23, T15)
PA_IN_GAGGAG(s(T30), T33, s(T32), T11, T34, T15) → PA_IN_GAGGAG(T30, T33, T32, T11, T34, T15)
sumB_in_gag([], [], []) → sumB_out_gag([], [], [])
sumB_in_gag(.(T10, T11), .(T16, T17), .(T14, T15)) → U3_gag(T10, T11, T16, T17, T14, T15, pA_in_gaggag(T10, T16, T14, T11, T17, T15))
pA_in_gaggag(0, T22, T22, T11, T23, T15) → U1_gaggag(T22, T11, T23, T15, sumB_in_gag(T11, T23, T15))
U1_gaggag(T22, T11, T23, T15, sumB_out_gag(T11, T23, T15)) → pA_out_gaggag(0, T22, T22, T11, T23, T15)
pA_in_gaggag(s(T30), T33, s(T32), T11, T34, T15) → U2_gaggag(T30, T33, T32, T11, T34, T15, pA_in_gaggag(T30, T33, T32, T11, T34, T15))
U2_gaggag(T30, T33, T32, T11, T34, T15, pA_out_gaggag(T30, T33, T32, T11, T34, T15)) → pA_out_gaggag(s(T30), T33, s(T32), T11, T34, T15)
U3_gag(T10, T11, T16, T17, T14, T15, pA_out_gaggag(T10, T16, T14, T11, T17, T15)) → sumB_out_gag(.(T10, T11), .(T16, T17), .(T14, T15))
SUMB_IN_GAG(.(T10, T11), .(T16, T17), .(T14, T15)) → PA_IN_GAGGAG(T10, T16, T14, T11, T17, T15)
PA_IN_GAGGAG(0, T22, T22, T11, T23, T15) → SUMB_IN_GAG(T11, T23, T15)
PA_IN_GAGGAG(s(T30), T33, s(T32), T11, T34, T15) → PA_IN_GAGGAG(T30, T33, T32, T11, T34, T15)
SUMB_IN_GAG(.(T10, T11), .(T14, T15)) → PA_IN_GAGGAG(T10, T14, T11, T15)
PA_IN_GAGGAG(0, T22, T11, T15) → SUMB_IN_GAG(T11, T15)
PA_IN_GAGGAG(s(T30), s(T32), T11, T15) → PA_IN_GAGGAG(T30, T32, T11, T15)
From the DPs we obtained the following set of size-change graphs: