0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 64 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 21 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 PiDP
↳7 UsableRulesProof (⇔, 0 ms)
↳8 PiDP
↳9 PiDPToQDPProof (⇒, 12 ms)
↳10 QDP
↳11 QDPSizeChangeProof (⇔, 0 ms)
↳12 YES
len1A_in_ga([], 0) → len1A_out_ga([], 0)
len1A_in_ga(.(T6, []), s(0)) → len1A_out_ga(.(T6, []), s(0))
len1A_in_ga(.(T6, .(T17, T18)), T9) → U1_ga(T6, T17, T18, T9, pB_in_gaaa(T18, X27, X28, T9))
pB_in_gaaa(T18, T19, X28, T9) → U3_gaaa(T18, T19, X28, T9, len1C_in_ga(T18, T19))
len1C_in_ga([], 0) → len1C_out_ga([], 0)
len1C_in_ga(.(T24, T25), X42) → U2_ga(T24, T25, X42, pD_in_gaa(T25, X41, X42))
pD_in_gaa(T25, T26, X42) → U5_gaa(T25, T26, X42, len1C_in_ga(T25, T26))
U5_gaa(T25, T26, X42, len1C_out_ga(T25, T26)) → U6_gaa(T25, T26, X42, eqF_in_ag(X42, T26))
eqF_in_ag(s(T29), T29) → eqF_out_ag(s(T29), T29)
U6_gaa(T25, T26, X42, eqF_out_ag(X42, T26)) → pD_out_gaa(T25, T26, X42)
U2_ga(T24, T25, X42, pD_out_gaa(T25, X41, X42)) → len1C_out_ga(.(T24, T25), X42)
U3_gaaa(T18, T19, X28, T9, len1C_out_ga(T18, T19)) → U4_gaaa(T18, T19, X28, T9, pE_in_aga(X28, T19, T9))
pE_in_aga(s(T38), T38, s(s(T38))) → pE_out_aga(s(T38), T38, s(s(T38)))
U4_gaaa(T18, T19, X28, T9, pE_out_aga(X28, T19, T9)) → pB_out_gaaa(T18, T19, X28, T9)
U1_ga(T6, T17, T18, T9, pB_out_gaaa(T18, X27, X28, T9)) → len1A_out_ga(.(T6, .(T17, T18)), T9)
LEN1A_IN_GA(.(T6, .(T17, T18)), T9) → U1_GA(T6, T17, T18, T9, pB_in_gaaa(T18, X27, X28, T9))
LEN1A_IN_GA(.(T6, .(T17, T18)), T9) → PB_IN_GAAA(T18, X27, X28, T9)
PB_IN_GAAA(T18, T19, X28, T9) → U3_GAAA(T18, T19, X28, T9, len1C_in_ga(T18, T19))
PB_IN_GAAA(T18, T19, X28, T9) → LEN1C_IN_GA(T18, T19)
LEN1C_IN_GA(.(T24, T25), X42) → U2_GA(T24, T25, X42, pD_in_gaa(T25, X41, X42))
LEN1C_IN_GA(.(T24, T25), X42) → PD_IN_GAA(T25, X41, X42)
PD_IN_GAA(T25, T26, X42) → U5_GAA(T25, T26, X42, len1C_in_ga(T25, T26))
PD_IN_GAA(T25, T26, X42) → LEN1C_IN_GA(T25, T26)
U5_GAA(T25, T26, X42, len1C_out_ga(T25, T26)) → U6_GAA(T25, T26, X42, eqF_in_ag(X42, T26))
U5_GAA(T25, T26, X42, len1C_out_ga(T25, T26)) → EQF_IN_AG(X42, T26)
U3_GAAA(T18, T19, X28, T9, len1C_out_ga(T18, T19)) → U4_GAAA(T18, T19, X28, T9, pE_in_aga(X28, T19, T9))
U3_GAAA(T18, T19, X28, T9, len1C_out_ga(T18, T19)) → PE_IN_AGA(X28, T19, T9)
len1A_in_ga([], 0) → len1A_out_ga([], 0)
len1A_in_ga(.(T6, []), s(0)) → len1A_out_ga(.(T6, []), s(0))
len1A_in_ga(.(T6, .(T17, T18)), T9) → U1_ga(T6, T17, T18, T9, pB_in_gaaa(T18, X27, X28, T9))
pB_in_gaaa(T18, T19, X28, T9) → U3_gaaa(T18, T19, X28, T9, len1C_in_ga(T18, T19))
len1C_in_ga([], 0) → len1C_out_ga([], 0)
len1C_in_ga(.(T24, T25), X42) → U2_ga(T24, T25, X42, pD_in_gaa(T25, X41, X42))
pD_in_gaa(T25, T26, X42) → U5_gaa(T25, T26, X42, len1C_in_ga(T25, T26))
U5_gaa(T25, T26, X42, len1C_out_ga(T25, T26)) → U6_gaa(T25, T26, X42, eqF_in_ag(X42, T26))
eqF_in_ag(s(T29), T29) → eqF_out_ag(s(T29), T29)
U6_gaa(T25, T26, X42, eqF_out_ag(X42, T26)) → pD_out_gaa(T25, T26, X42)
U2_ga(T24, T25, X42, pD_out_gaa(T25, X41, X42)) → len1C_out_ga(.(T24, T25), X42)
U3_gaaa(T18, T19, X28, T9, len1C_out_ga(T18, T19)) → U4_gaaa(T18, T19, X28, T9, pE_in_aga(X28, T19, T9))
pE_in_aga(s(T38), T38, s(s(T38))) → pE_out_aga(s(T38), T38, s(s(T38)))
U4_gaaa(T18, T19, X28, T9, pE_out_aga(X28, T19, T9)) → pB_out_gaaa(T18, T19, X28, T9)
U1_ga(T6, T17, T18, T9, pB_out_gaaa(T18, X27, X28, T9)) → len1A_out_ga(.(T6, .(T17, T18)), T9)
LEN1A_IN_GA(.(T6, .(T17, T18)), T9) → U1_GA(T6, T17, T18, T9, pB_in_gaaa(T18, X27, X28, T9))
LEN1A_IN_GA(.(T6, .(T17, T18)), T9) → PB_IN_GAAA(T18, X27, X28, T9)
PB_IN_GAAA(T18, T19, X28, T9) → U3_GAAA(T18, T19, X28, T9, len1C_in_ga(T18, T19))
PB_IN_GAAA(T18, T19, X28, T9) → LEN1C_IN_GA(T18, T19)
LEN1C_IN_GA(.(T24, T25), X42) → U2_GA(T24, T25, X42, pD_in_gaa(T25, X41, X42))
LEN1C_IN_GA(.(T24, T25), X42) → PD_IN_GAA(T25, X41, X42)
PD_IN_GAA(T25, T26, X42) → U5_GAA(T25, T26, X42, len1C_in_ga(T25, T26))
PD_IN_GAA(T25, T26, X42) → LEN1C_IN_GA(T25, T26)
U5_GAA(T25, T26, X42, len1C_out_ga(T25, T26)) → U6_GAA(T25, T26, X42, eqF_in_ag(X42, T26))
U5_GAA(T25, T26, X42, len1C_out_ga(T25, T26)) → EQF_IN_AG(X42, T26)
U3_GAAA(T18, T19, X28, T9, len1C_out_ga(T18, T19)) → U4_GAAA(T18, T19, X28, T9, pE_in_aga(X28, T19, T9))
U3_GAAA(T18, T19, X28, T9, len1C_out_ga(T18, T19)) → PE_IN_AGA(X28, T19, T9)
len1A_in_ga([], 0) → len1A_out_ga([], 0)
len1A_in_ga(.(T6, []), s(0)) → len1A_out_ga(.(T6, []), s(0))
len1A_in_ga(.(T6, .(T17, T18)), T9) → U1_ga(T6, T17, T18, T9, pB_in_gaaa(T18, X27, X28, T9))
pB_in_gaaa(T18, T19, X28, T9) → U3_gaaa(T18, T19, X28, T9, len1C_in_ga(T18, T19))
len1C_in_ga([], 0) → len1C_out_ga([], 0)
len1C_in_ga(.(T24, T25), X42) → U2_ga(T24, T25, X42, pD_in_gaa(T25, X41, X42))
pD_in_gaa(T25, T26, X42) → U5_gaa(T25, T26, X42, len1C_in_ga(T25, T26))
U5_gaa(T25, T26, X42, len1C_out_ga(T25, T26)) → U6_gaa(T25, T26, X42, eqF_in_ag(X42, T26))
eqF_in_ag(s(T29), T29) → eqF_out_ag(s(T29), T29)
U6_gaa(T25, T26, X42, eqF_out_ag(X42, T26)) → pD_out_gaa(T25, T26, X42)
U2_ga(T24, T25, X42, pD_out_gaa(T25, X41, X42)) → len1C_out_ga(.(T24, T25), X42)
U3_gaaa(T18, T19, X28, T9, len1C_out_ga(T18, T19)) → U4_gaaa(T18, T19, X28, T9, pE_in_aga(X28, T19, T9))
pE_in_aga(s(T38), T38, s(s(T38))) → pE_out_aga(s(T38), T38, s(s(T38)))
U4_gaaa(T18, T19, X28, T9, pE_out_aga(X28, T19, T9)) → pB_out_gaaa(T18, T19, X28, T9)
U1_ga(T6, T17, T18, T9, pB_out_gaaa(T18, X27, X28, T9)) → len1A_out_ga(.(T6, .(T17, T18)), T9)
LEN1C_IN_GA(.(T24, T25), X42) → PD_IN_GAA(T25, X41, X42)
PD_IN_GAA(T25, T26, X42) → LEN1C_IN_GA(T25, T26)
len1A_in_ga([], 0) → len1A_out_ga([], 0)
len1A_in_ga(.(T6, []), s(0)) → len1A_out_ga(.(T6, []), s(0))
len1A_in_ga(.(T6, .(T17, T18)), T9) → U1_ga(T6, T17, T18, T9, pB_in_gaaa(T18, X27, X28, T9))
pB_in_gaaa(T18, T19, X28, T9) → U3_gaaa(T18, T19, X28, T9, len1C_in_ga(T18, T19))
len1C_in_ga([], 0) → len1C_out_ga([], 0)
len1C_in_ga(.(T24, T25), X42) → U2_ga(T24, T25, X42, pD_in_gaa(T25, X41, X42))
pD_in_gaa(T25, T26, X42) → U5_gaa(T25, T26, X42, len1C_in_ga(T25, T26))
U5_gaa(T25, T26, X42, len1C_out_ga(T25, T26)) → U6_gaa(T25, T26, X42, eqF_in_ag(X42, T26))
eqF_in_ag(s(T29), T29) → eqF_out_ag(s(T29), T29)
U6_gaa(T25, T26, X42, eqF_out_ag(X42, T26)) → pD_out_gaa(T25, T26, X42)
U2_ga(T24, T25, X42, pD_out_gaa(T25, X41, X42)) → len1C_out_ga(.(T24, T25), X42)
U3_gaaa(T18, T19, X28, T9, len1C_out_ga(T18, T19)) → U4_gaaa(T18, T19, X28, T9, pE_in_aga(X28, T19, T9))
pE_in_aga(s(T38), T38, s(s(T38))) → pE_out_aga(s(T38), T38, s(s(T38)))
U4_gaaa(T18, T19, X28, T9, pE_out_aga(X28, T19, T9)) → pB_out_gaaa(T18, T19, X28, T9)
U1_ga(T6, T17, T18, T9, pB_out_gaaa(T18, X27, X28, T9)) → len1A_out_ga(.(T6, .(T17, T18)), T9)
LEN1C_IN_GA(.(T24, T25), X42) → PD_IN_GAA(T25, X41, X42)
PD_IN_GAA(T25, T26, X42) → LEN1C_IN_GA(T25, T26)
LEN1C_IN_GA(.(T24, T25)) → PD_IN_GAA(T25)
PD_IN_GAA(T25) → LEN1C_IN_GA(T25)
From the DPs we obtained the following set of size-change graphs: