0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 154 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 42 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 27 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇒, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
sublistA_in_ag([], T16) → sublistA_out_ag([], T16)
sublistA_in_ag(T7, .(T29, T30)) → U1_ag(T7, T29, T30, pB_in_aagaag(X56, X57, T30, X9, T7, T29))
pB_in_aagaag(T38, T39, T30, X9, T7, T29) → U5_aagaag(T38, T39, T30, X9, T7, T29, appendC_in_aag(T38, T39, T30))
appendC_in_aag([], T45, T45) → appendC_out_aag([], T45, T45)
appendC_in_aag(.(T50, X93), X94, .(T50, T51)) → U2_aag(T50, X93, X94, T51, appendC_in_aag(X93, X94, T51))
U2_aag(T50, X93, X94, T51, appendC_out_aag(X93, X94, T51)) → appendC_out_aag(.(T50, X93), X94, .(T50, T51))
U5_aagaag(T38, T39, T30, X9, T7, T29, appendC_out_aag(T38, T39, T30)) → U6_aagaag(T38, T39, T30, X9, T7, T29, appendE_in_aagg(X9, T7, T29, T38))
appendE_in_aagg([], .(T72, T73), T72, T73) → appendE_out_aagg([], .(T72, T73), T72, T73)
appendE_in_aagg(.(T84, X123), T86, T84, T85) → U4_aagg(T84, X123, T86, T85, appendD_in_aag(X123, T86, T85))
appendD_in_aag([], T93, T93) → appendD_out_aag([], T93, T93)
appendD_in_aag(.(T101, X148), T103, .(T101, T102)) → U3_aag(T101, X148, T103, T102, appendD_in_aag(X148, T103, T102))
U3_aag(T101, X148, T103, T102, appendD_out_aag(X148, T103, T102)) → appendD_out_aag(.(T101, X148), T103, .(T101, T102))
U4_aagg(T84, X123, T86, T85, appendD_out_aag(X123, T86, T85)) → appendE_out_aagg(.(T84, X123), T86, T84, T85)
U6_aagaag(T38, T39, T30, X9, T7, T29, appendE_out_aagg(X9, T7, T29, T38)) → pB_out_aagaag(T38, T39, T30, X9, T7, T29)
U1_ag(T7, T29, T30, pB_out_aagaag(X56, X57, T30, X9, T7, T29)) → sublistA_out_ag(T7, .(T29, T30))
SUBLISTA_IN_AG(T7, .(T29, T30)) → U1_AG(T7, T29, T30, pB_in_aagaag(X56, X57, T30, X9, T7, T29))
SUBLISTA_IN_AG(T7, .(T29, T30)) → PB_IN_AAGAAG(X56, X57, T30, X9, T7, T29)
PB_IN_AAGAAG(T38, T39, T30, X9, T7, T29) → U5_AAGAAG(T38, T39, T30, X9, T7, T29, appendC_in_aag(T38, T39, T30))
PB_IN_AAGAAG(T38, T39, T30, X9, T7, T29) → APPENDC_IN_AAG(T38, T39, T30)
APPENDC_IN_AAG(.(T50, X93), X94, .(T50, T51)) → U2_AAG(T50, X93, X94, T51, appendC_in_aag(X93, X94, T51))
APPENDC_IN_AAG(.(T50, X93), X94, .(T50, T51)) → APPENDC_IN_AAG(X93, X94, T51)
U5_AAGAAG(T38, T39, T30, X9, T7, T29, appendC_out_aag(T38, T39, T30)) → U6_AAGAAG(T38, T39, T30, X9, T7, T29, appendE_in_aagg(X9, T7, T29, T38))
U5_AAGAAG(T38, T39, T30, X9, T7, T29, appendC_out_aag(T38, T39, T30)) → APPENDE_IN_AAGG(X9, T7, T29, T38)
APPENDE_IN_AAGG(.(T84, X123), T86, T84, T85) → U4_AAGG(T84, X123, T86, T85, appendD_in_aag(X123, T86, T85))
APPENDE_IN_AAGG(.(T84, X123), T86, T84, T85) → APPENDD_IN_AAG(X123, T86, T85)
APPENDD_IN_AAG(.(T101, X148), T103, .(T101, T102)) → U3_AAG(T101, X148, T103, T102, appendD_in_aag(X148, T103, T102))
APPENDD_IN_AAG(.(T101, X148), T103, .(T101, T102)) → APPENDD_IN_AAG(X148, T103, T102)
sublistA_in_ag([], T16) → sublistA_out_ag([], T16)
sublistA_in_ag(T7, .(T29, T30)) → U1_ag(T7, T29, T30, pB_in_aagaag(X56, X57, T30, X9, T7, T29))
pB_in_aagaag(T38, T39, T30, X9, T7, T29) → U5_aagaag(T38, T39, T30, X9, T7, T29, appendC_in_aag(T38, T39, T30))
appendC_in_aag([], T45, T45) → appendC_out_aag([], T45, T45)
appendC_in_aag(.(T50, X93), X94, .(T50, T51)) → U2_aag(T50, X93, X94, T51, appendC_in_aag(X93, X94, T51))
U2_aag(T50, X93, X94, T51, appendC_out_aag(X93, X94, T51)) → appendC_out_aag(.(T50, X93), X94, .(T50, T51))
U5_aagaag(T38, T39, T30, X9, T7, T29, appendC_out_aag(T38, T39, T30)) → U6_aagaag(T38, T39, T30, X9, T7, T29, appendE_in_aagg(X9, T7, T29, T38))
appendE_in_aagg([], .(T72, T73), T72, T73) → appendE_out_aagg([], .(T72, T73), T72, T73)
appendE_in_aagg(.(T84, X123), T86, T84, T85) → U4_aagg(T84, X123, T86, T85, appendD_in_aag(X123, T86, T85))
appendD_in_aag([], T93, T93) → appendD_out_aag([], T93, T93)
appendD_in_aag(.(T101, X148), T103, .(T101, T102)) → U3_aag(T101, X148, T103, T102, appendD_in_aag(X148, T103, T102))
U3_aag(T101, X148, T103, T102, appendD_out_aag(X148, T103, T102)) → appendD_out_aag(.(T101, X148), T103, .(T101, T102))
U4_aagg(T84, X123, T86, T85, appendD_out_aag(X123, T86, T85)) → appendE_out_aagg(.(T84, X123), T86, T84, T85)
U6_aagaag(T38, T39, T30, X9, T7, T29, appendE_out_aagg(X9, T7, T29, T38)) → pB_out_aagaag(T38, T39, T30, X9, T7, T29)
U1_ag(T7, T29, T30, pB_out_aagaag(X56, X57, T30, X9, T7, T29)) → sublistA_out_ag(T7, .(T29, T30))
SUBLISTA_IN_AG(T7, .(T29, T30)) → U1_AG(T7, T29, T30, pB_in_aagaag(X56, X57, T30, X9, T7, T29))
SUBLISTA_IN_AG(T7, .(T29, T30)) → PB_IN_AAGAAG(X56, X57, T30, X9, T7, T29)
PB_IN_AAGAAG(T38, T39, T30, X9, T7, T29) → U5_AAGAAG(T38, T39, T30, X9, T7, T29, appendC_in_aag(T38, T39, T30))
PB_IN_AAGAAG(T38, T39, T30, X9, T7, T29) → APPENDC_IN_AAG(T38, T39, T30)
APPENDC_IN_AAG(.(T50, X93), X94, .(T50, T51)) → U2_AAG(T50, X93, X94, T51, appendC_in_aag(X93, X94, T51))
APPENDC_IN_AAG(.(T50, X93), X94, .(T50, T51)) → APPENDC_IN_AAG(X93, X94, T51)
U5_AAGAAG(T38, T39, T30, X9, T7, T29, appendC_out_aag(T38, T39, T30)) → U6_AAGAAG(T38, T39, T30, X9, T7, T29, appendE_in_aagg(X9, T7, T29, T38))
U5_AAGAAG(T38, T39, T30, X9, T7, T29, appendC_out_aag(T38, T39, T30)) → APPENDE_IN_AAGG(X9, T7, T29, T38)
APPENDE_IN_AAGG(.(T84, X123), T86, T84, T85) → U4_AAGG(T84, X123, T86, T85, appendD_in_aag(X123, T86, T85))
APPENDE_IN_AAGG(.(T84, X123), T86, T84, T85) → APPENDD_IN_AAG(X123, T86, T85)
APPENDD_IN_AAG(.(T101, X148), T103, .(T101, T102)) → U3_AAG(T101, X148, T103, T102, appendD_in_aag(X148, T103, T102))
APPENDD_IN_AAG(.(T101, X148), T103, .(T101, T102)) → APPENDD_IN_AAG(X148, T103, T102)
sublistA_in_ag([], T16) → sublistA_out_ag([], T16)
sublistA_in_ag(T7, .(T29, T30)) → U1_ag(T7, T29, T30, pB_in_aagaag(X56, X57, T30, X9, T7, T29))
pB_in_aagaag(T38, T39, T30, X9, T7, T29) → U5_aagaag(T38, T39, T30, X9, T7, T29, appendC_in_aag(T38, T39, T30))
appendC_in_aag([], T45, T45) → appendC_out_aag([], T45, T45)
appendC_in_aag(.(T50, X93), X94, .(T50, T51)) → U2_aag(T50, X93, X94, T51, appendC_in_aag(X93, X94, T51))
U2_aag(T50, X93, X94, T51, appendC_out_aag(X93, X94, T51)) → appendC_out_aag(.(T50, X93), X94, .(T50, T51))
U5_aagaag(T38, T39, T30, X9, T7, T29, appendC_out_aag(T38, T39, T30)) → U6_aagaag(T38, T39, T30, X9, T7, T29, appendE_in_aagg(X9, T7, T29, T38))
appendE_in_aagg([], .(T72, T73), T72, T73) → appendE_out_aagg([], .(T72, T73), T72, T73)
appendE_in_aagg(.(T84, X123), T86, T84, T85) → U4_aagg(T84, X123, T86, T85, appendD_in_aag(X123, T86, T85))
appendD_in_aag([], T93, T93) → appendD_out_aag([], T93, T93)
appendD_in_aag(.(T101, X148), T103, .(T101, T102)) → U3_aag(T101, X148, T103, T102, appendD_in_aag(X148, T103, T102))
U3_aag(T101, X148, T103, T102, appendD_out_aag(X148, T103, T102)) → appendD_out_aag(.(T101, X148), T103, .(T101, T102))
U4_aagg(T84, X123, T86, T85, appendD_out_aag(X123, T86, T85)) → appendE_out_aagg(.(T84, X123), T86, T84, T85)
U6_aagaag(T38, T39, T30, X9, T7, T29, appendE_out_aagg(X9, T7, T29, T38)) → pB_out_aagaag(T38, T39, T30, X9, T7, T29)
U1_ag(T7, T29, T30, pB_out_aagaag(X56, X57, T30, X9, T7, T29)) → sublistA_out_ag(T7, .(T29, T30))
APPENDD_IN_AAG(.(T101, X148), T103, .(T101, T102)) → APPENDD_IN_AAG(X148, T103, T102)
sublistA_in_ag([], T16) → sublistA_out_ag([], T16)
sublistA_in_ag(T7, .(T29, T30)) → U1_ag(T7, T29, T30, pB_in_aagaag(X56, X57, T30, X9, T7, T29))
pB_in_aagaag(T38, T39, T30, X9, T7, T29) → U5_aagaag(T38, T39, T30, X9, T7, T29, appendC_in_aag(T38, T39, T30))
appendC_in_aag([], T45, T45) → appendC_out_aag([], T45, T45)
appendC_in_aag(.(T50, X93), X94, .(T50, T51)) → U2_aag(T50, X93, X94, T51, appendC_in_aag(X93, X94, T51))
U2_aag(T50, X93, X94, T51, appendC_out_aag(X93, X94, T51)) → appendC_out_aag(.(T50, X93), X94, .(T50, T51))
U5_aagaag(T38, T39, T30, X9, T7, T29, appendC_out_aag(T38, T39, T30)) → U6_aagaag(T38, T39, T30, X9, T7, T29, appendE_in_aagg(X9, T7, T29, T38))
appendE_in_aagg([], .(T72, T73), T72, T73) → appendE_out_aagg([], .(T72, T73), T72, T73)
appendE_in_aagg(.(T84, X123), T86, T84, T85) → U4_aagg(T84, X123, T86, T85, appendD_in_aag(X123, T86, T85))
appendD_in_aag([], T93, T93) → appendD_out_aag([], T93, T93)
appendD_in_aag(.(T101, X148), T103, .(T101, T102)) → U3_aag(T101, X148, T103, T102, appendD_in_aag(X148, T103, T102))
U3_aag(T101, X148, T103, T102, appendD_out_aag(X148, T103, T102)) → appendD_out_aag(.(T101, X148), T103, .(T101, T102))
U4_aagg(T84, X123, T86, T85, appendD_out_aag(X123, T86, T85)) → appendE_out_aagg(.(T84, X123), T86, T84, T85)
U6_aagaag(T38, T39, T30, X9, T7, T29, appendE_out_aagg(X9, T7, T29, T38)) → pB_out_aagaag(T38, T39, T30, X9, T7, T29)
U1_ag(T7, T29, T30, pB_out_aagaag(X56, X57, T30, X9, T7, T29)) → sublistA_out_ag(T7, .(T29, T30))
APPENDD_IN_AAG(.(T101, X148), T103, .(T101, T102)) → APPENDD_IN_AAG(X148, T103, T102)
APPENDD_IN_AAG(.(T101, T102)) → APPENDD_IN_AAG(T102)
From the DPs we obtained the following set of size-change graphs:
APPENDC_IN_AAG(.(T50, X93), X94, .(T50, T51)) → APPENDC_IN_AAG(X93, X94, T51)
sublistA_in_ag([], T16) → sublistA_out_ag([], T16)
sublistA_in_ag(T7, .(T29, T30)) → U1_ag(T7, T29, T30, pB_in_aagaag(X56, X57, T30, X9, T7, T29))
pB_in_aagaag(T38, T39, T30, X9, T7, T29) → U5_aagaag(T38, T39, T30, X9, T7, T29, appendC_in_aag(T38, T39, T30))
appendC_in_aag([], T45, T45) → appendC_out_aag([], T45, T45)
appendC_in_aag(.(T50, X93), X94, .(T50, T51)) → U2_aag(T50, X93, X94, T51, appendC_in_aag(X93, X94, T51))
U2_aag(T50, X93, X94, T51, appendC_out_aag(X93, X94, T51)) → appendC_out_aag(.(T50, X93), X94, .(T50, T51))
U5_aagaag(T38, T39, T30, X9, T7, T29, appendC_out_aag(T38, T39, T30)) → U6_aagaag(T38, T39, T30, X9, T7, T29, appendE_in_aagg(X9, T7, T29, T38))
appendE_in_aagg([], .(T72, T73), T72, T73) → appendE_out_aagg([], .(T72, T73), T72, T73)
appendE_in_aagg(.(T84, X123), T86, T84, T85) → U4_aagg(T84, X123, T86, T85, appendD_in_aag(X123, T86, T85))
appendD_in_aag([], T93, T93) → appendD_out_aag([], T93, T93)
appendD_in_aag(.(T101, X148), T103, .(T101, T102)) → U3_aag(T101, X148, T103, T102, appendD_in_aag(X148, T103, T102))
U3_aag(T101, X148, T103, T102, appendD_out_aag(X148, T103, T102)) → appendD_out_aag(.(T101, X148), T103, .(T101, T102))
U4_aagg(T84, X123, T86, T85, appendD_out_aag(X123, T86, T85)) → appendE_out_aagg(.(T84, X123), T86, T84, T85)
U6_aagaag(T38, T39, T30, X9, T7, T29, appendE_out_aagg(X9, T7, T29, T38)) → pB_out_aagaag(T38, T39, T30, X9, T7, T29)
U1_ag(T7, T29, T30, pB_out_aagaag(X56, X57, T30, X9, T7, T29)) → sublistA_out_ag(T7, .(T29, T30))
APPENDC_IN_AAG(.(T50, X93), X94, .(T50, T51)) → APPENDC_IN_AAG(X93, X94, T51)
APPENDC_IN_AAG(.(T50, T51)) → APPENDC_IN_AAG(T51)
From the DPs we obtained the following set of size-change graphs: