0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 153 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 54 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 23 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_gg([], T15) → sublistA_out_gg([], T15)
sublistA_in_gg(T5, .(T28, T29)) → U1_gg(T5, T28, T29, pB_in_aagagg(X56, X57, T29, X9, T5, T28))
pB_in_aagagg(T37, T38, T29, X9, T5, T28) → U5_aagagg(T37, T38, T29, X9, T5, T28, appendC_in_aag(T37, T38, T29))
appendC_in_aag([], T44, T44) → appendC_out_aag([], T44, T44)
appendC_in_aag(.(T49, X93), X94, .(T49, T50)) → U2_aag(T49, X93, X94, T50, appendC_in_aag(X93, X94, T50))
U2_aag(T49, X93, X94, T50, appendC_out_aag(X93, X94, T50)) → appendC_out_aag(.(T49, X93), X94, .(T49, T50))
U5_aagagg(T37, T38, T29, X9, T5, T28, appendC_out_aag(T37, T38, T29)) → U6_aagagg(T37, T38, T29, X9, T5, T28, appendE_in_aggg(X9, T5, T28, T37))
appendE_in_aggg([], .(T71, T72), T71, T72) → appendE_out_aggg([], .(T71, T72), T71, T72)
appendE_in_aggg(.(T82, X123), T81, T82, T83) → U4_aggg(T82, X123, T81, T83, appendD_in_agg(X123, T81, T83))
appendD_in_agg([], T90, T90) → appendD_out_agg([], T90, T90)
appendD_in_agg(.(T98, X148), T97, .(T98, T99)) → U3_agg(T98, X148, T97, T99, appendD_in_agg(X148, T97, T99))
U3_agg(T98, X148, T97, T99, appendD_out_agg(X148, T97, T99)) → appendD_out_agg(.(T98, X148), T97, .(T98, T99))
U4_aggg(T82, X123, T81, T83, appendD_out_agg(X123, T81, T83)) → appendE_out_aggg(.(T82, X123), T81, T82, T83)
U6_aagagg(T37, T38, T29, X9, T5, T28, appendE_out_aggg(X9, T5, T28, T37)) → pB_out_aagagg(T37, T38, T29, X9, T5, T28)
U1_gg(T5, T28, T29, pB_out_aagagg(X56, X57, T29, X9, T5, T28)) → sublistA_out_gg(T5, .(T28, T29))
SUBLISTA_IN_GG(T5, .(T28, T29)) → U1_GG(T5, T28, T29, pB_in_aagagg(X56, X57, T29, X9, T5, T28))
SUBLISTA_IN_GG(T5, .(T28, T29)) → PB_IN_AAGAGG(X56, X57, T29, X9, T5, T28)
PB_IN_AAGAGG(T37, T38, T29, X9, T5, T28) → U5_AAGAGG(T37, T38, T29, X9, T5, T28, appendC_in_aag(T37, T38, T29))
PB_IN_AAGAGG(T37, T38, T29, X9, T5, T28) → APPENDC_IN_AAG(T37, T38, T29)
APPENDC_IN_AAG(.(T49, X93), X94, .(T49, T50)) → U2_AAG(T49, X93, X94, T50, appendC_in_aag(X93, X94, T50))
APPENDC_IN_AAG(.(T49, X93), X94, .(T49, T50)) → APPENDC_IN_AAG(X93, X94, T50)
U5_AAGAGG(T37, T38, T29, X9, T5, T28, appendC_out_aag(T37, T38, T29)) → U6_AAGAGG(T37, T38, T29, X9, T5, T28, appendE_in_aggg(X9, T5, T28, T37))
U5_AAGAGG(T37, T38, T29, X9, T5, T28, appendC_out_aag(T37, T38, T29)) → APPENDE_IN_AGGG(X9, T5, T28, T37)
APPENDE_IN_AGGG(.(T82, X123), T81, T82, T83) → U4_AGGG(T82, X123, T81, T83, appendD_in_agg(X123, T81, T83))
APPENDE_IN_AGGG(.(T82, X123), T81, T82, T83) → APPENDD_IN_AGG(X123, T81, T83)
APPENDD_IN_AGG(.(T98, X148), T97, .(T98, T99)) → U3_AGG(T98, X148, T97, T99, appendD_in_agg(X148, T97, T99))
APPENDD_IN_AGG(.(T98, X148), T97, .(T98, T99)) → APPENDD_IN_AGG(X148, T97, T99)
sublistA_in_gg([], T15) → sublistA_out_gg([], T15)
sublistA_in_gg(T5, .(T28, T29)) → U1_gg(T5, T28, T29, pB_in_aagagg(X56, X57, T29, X9, T5, T28))
pB_in_aagagg(T37, T38, T29, X9, T5, T28) → U5_aagagg(T37, T38, T29, X9, T5, T28, appendC_in_aag(T37, T38, T29))
appendC_in_aag([], T44, T44) → appendC_out_aag([], T44, T44)
appendC_in_aag(.(T49, X93), X94, .(T49, T50)) → U2_aag(T49, X93, X94, T50, appendC_in_aag(X93, X94, T50))
U2_aag(T49, X93, X94, T50, appendC_out_aag(X93, X94, T50)) → appendC_out_aag(.(T49, X93), X94, .(T49, T50))
U5_aagagg(T37, T38, T29, X9, T5, T28, appendC_out_aag(T37, T38, T29)) → U6_aagagg(T37, T38, T29, X9, T5, T28, appendE_in_aggg(X9, T5, T28, T37))
appendE_in_aggg([], .(T71, T72), T71, T72) → appendE_out_aggg([], .(T71, T72), T71, T72)
appendE_in_aggg(.(T82, X123), T81, T82, T83) → U4_aggg(T82, X123, T81, T83, appendD_in_agg(X123, T81, T83))
appendD_in_agg([], T90, T90) → appendD_out_agg([], T90, T90)
appendD_in_agg(.(T98, X148), T97, .(T98, T99)) → U3_agg(T98, X148, T97, T99, appendD_in_agg(X148, T97, T99))
U3_agg(T98, X148, T97, T99, appendD_out_agg(X148, T97, T99)) → appendD_out_agg(.(T98, X148), T97, .(T98, T99))
U4_aggg(T82, X123, T81, T83, appendD_out_agg(X123, T81, T83)) → appendE_out_aggg(.(T82, X123), T81, T82, T83)
U6_aagagg(T37, T38, T29, X9, T5, T28, appendE_out_aggg(X9, T5, T28, T37)) → pB_out_aagagg(T37, T38, T29, X9, T5, T28)
U1_gg(T5, T28, T29, pB_out_aagagg(X56, X57, T29, X9, T5, T28)) → sublistA_out_gg(T5, .(T28, T29))
SUBLISTA_IN_GG(T5, .(T28, T29)) → U1_GG(T5, T28, T29, pB_in_aagagg(X56, X57, T29, X9, T5, T28))
SUBLISTA_IN_GG(T5, .(T28, T29)) → PB_IN_AAGAGG(X56, X57, T29, X9, T5, T28)
PB_IN_AAGAGG(T37, T38, T29, X9, T5, T28) → U5_AAGAGG(T37, T38, T29, X9, T5, T28, appendC_in_aag(T37, T38, T29))
PB_IN_AAGAGG(T37, T38, T29, X9, T5, T28) → APPENDC_IN_AAG(T37, T38, T29)
APPENDC_IN_AAG(.(T49, X93), X94, .(T49, T50)) → U2_AAG(T49, X93, X94, T50, appendC_in_aag(X93, X94, T50))
APPENDC_IN_AAG(.(T49, X93), X94, .(T49, T50)) → APPENDC_IN_AAG(X93, X94, T50)
U5_AAGAGG(T37, T38, T29, X9, T5, T28, appendC_out_aag(T37, T38, T29)) → U6_AAGAGG(T37, T38, T29, X9, T5, T28, appendE_in_aggg(X9, T5, T28, T37))
U5_AAGAGG(T37, T38, T29, X9, T5, T28, appendC_out_aag(T37, T38, T29)) → APPENDE_IN_AGGG(X9, T5, T28, T37)
APPENDE_IN_AGGG(.(T82, X123), T81, T82, T83) → U4_AGGG(T82, X123, T81, T83, appendD_in_agg(X123, T81, T83))
APPENDE_IN_AGGG(.(T82, X123), T81, T82, T83) → APPENDD_IN_AGG(X123, T81, T83)
APPENDD_IN_AGG(.(T98, X148), T97, .(T98, T99)) → U3_AGG(T98, X148, T97, T99, appendD_in_agg(X148, T97, T99))
APPENDD_IN_AGG(.(T98, X148), T97, .(T98, T99)) → APPENDD_IN_AGG(X148, T97, T99)
sublistA_in_gg([], T15) → sublistA_out_gg([], T15)
sublistA_in_gg(T5, .(T28, T29)) → U1_gg(T5, T28, T29, pB_in_aagagg(X56, X57, T29, X9, T5, T28))
pB_in_aagagg(T37, T38, T29, X9, T5, T28) → U5_aagagg(T37, T38, T29, X9, T5, T28, appendC_in_aag(T37, T38, T29))
appendC_in_aag([], T44, T44) → appendC_out_aag([], T44, T44)
appendC_in_aag(.(T49, X93), X94, .(T49, T50)) → U2_aag(T49, X93, X94, T50, appendC_in_aag(X93, X94, T50))
U2_aag(T49, X93, X94, T50, appendC_out_aag(X93, X94, T50)) → appendC_out_aag(.(T49, X93), X94, .(T49, T50))
U5_aagagg(T37, T38, T29, X9, T5, T28, appendC_out_aag(T37, T38, T29)) → U6_aagagg(T37, T38, T29, X9, T5, T28, appendE_in_aggg(X9, T5, T28, T37))
appendE_in_aggg([], .(T71, T72), T71, T72) → appendE_out_aggg([], .(T71, T72), T71, T72)
appendE_in_aggg(.(T82, X123), T81, T82, T83) → U4_aggg(T82, X123, T81, T83, appendD_in_agg(X123, T81, T83))
appendD_in_agg([], T90, T90) → appendD_out_agg([], T90, T90)
appendD_in_agg(.(T98, X148), T97, .(T98, T99)) → U3_agg(T98, X148, T97, T99, appendD_in_agg(X148, T97, T99))
U3_agg(T98, X148, T97, T99, appendD_out_agg(X148, T97, T99)) → appendD_out_agg(.(T98, X148), T97, .(T98, T99))
U4_aggg(T82, X123, T81, T83, appendD_out_agg(X123, T81, T83)) → appendE_out_aggg(.(T82, X123), T81, T82, T83)
U6_aagagg(T37, T38, T29, X9, T5, T28, appendE_out_aggg(X9, T5, T28, T37)) → pB_out_aagagg(T37, T38, T29, X9, T5, T28)
U1_gg(T5, T28, T29, pB_out_aagagg(X56, X57, T29, X9, T5, T28)) → sublistA_out_gg(T5, .(T28, T29))
APPENDD_IN_AGG(.(T98, X148), T97, .(T98, T99)) → APPENDD_IN_AGG(X148, T97, T99)
sublistA_in_gg([], T15) → sublistA_out_gg([], T15)
sublistA_in_gg(T5, .(T28, T29)) → U1_gg(T5, T28, T29, pB_in_aagagg(X56, X57, T29, X9, T5, T28))
pB_in_aagagg(T37, T38, T29, X9, T5, T28) → U5_aagagg(T37, T38, T29, X9, T5, T28, appendC_in_aag(T37, T38, T29))
appendC_in_aag([], T44, T44) → appendC_out_aag([], T44, T44)
appendC_in_aag(.(T49, X93), X94, .(T49, T50)) → U2_aag(T49, X93, X94, T50, appendC_in_aag(X93, X94, T50))
U2_aag(T49, X93, X94, T50, appendC_out_aag(X93, X94, T50)) → appendC_out_aag(.(T49, X93), X94, .(T49, T50))
U5_aagagg(T37, T38, T29, X9, T5, T28, appendC_out_aag(T37, T38, T29)) → U6_aagagg(T37, T38, T29, X9, T5, T28, appendE_in_aggg(X9, T5, T28, T37))
appendE_in_aggg([], .(T71, T72), T71, T72) → appendE_out_aggg([], .(T71, T72), T71, T72)
appendE_in_aggg(.(T82, X123), T81, T82, T83) → U4_aggg(T82, X123, T81, T83, appendD_in_agg(X123, T81, T83))
appendD_in_agg([], T90, T90) → appendD_out_agg([], T90, T90)
appendD_in_agg(.(T98, X148), T97, .(T98, T99)) → U3_agg(T98, X148, T97, T99, appendD_in_agg(X148, T97, T99))
U3_agg(T98, X148, T97, T99, appendD_out_agg(X148, T97, T99)) → appendD_out_agg(.(T98, X148), T97, .(T98, T99))
U4_aggg(T82, X123, T81, T83, appendD_out_agg(X123, T81, T83)) → appendE_out_aggg(.(T82, X123), T81, T82, T83)
U6_aagagg(T37, T38, T29, X9, T5, T28, appendE_out_aggg(X9, T5, T28, T37)) → pB_out_aagagg(T37, T38, T29, X9, T5, T28)
U1_gg(T5, T28, T29, pB_out_aagagg(X56, X57, T29, X9, T5, T28)) → sublistA_out_gg(T5, .(T28, T29))
APPENDD_IN_AGG(.(T98, X148), T97, .(T98, T99)) → APPENDD_IN_AGG(X148, T97, T99)
APPENDD_IN_AGG(T97, .(T98, T99)) → APPENDD_IN_AGG(T97, T99)
From the DPs we obtained the following set of size-change graphs:
APPENDC_IN_AAG(.(T49, X93), X94, .(T49, T50)) → APPENDC_IN_AAG(X93, X94, T50)
sublistA_in_gg([], T15) → sublistA_out_gg([], T15)
sublistA_in_gg(T5, .(T28, T29)) → U1_gg(T5, T28, T29, pB_in_aagagg(X56, X57, T29, X9, T5, T28))
pB_in_aagagg(T37, T38, T29, X9, T5, T28) → U5_aagagg(T37, T38, T29, X9, T5, T28, appendC_in_aag(T37, T38, T29))
appendC_in_aag([], T44, T44) → appendC_out_aag([], T44, T44)
appendC_in_aag(.(T49, X93), X94, .(T49, T50)) → U2_aag(T49, X93, X94, T50, appendC_in_aag(X93, X94, T50))
U2_aag(T49, X93, X94, T50, appendC_out_aag(X93, X94, T50)) → appendC_out_aag(.(T49, X93), X94, .(T49, T50))
U5_aagagg(T37, T38, T29, X9, T5, T28, appendC_out_aag(T37, T38, T29)) → U6_aagagg(T37, T38, T29, X9, T5, T28, appendE_in_aggg(X9, T5, T28, T37))
appendE_in_aggg([], .(T71, T72), T71, T72) → appendE_out_aggg([], .(T71, T72), T71, T72)
appendE_in_aggg(.(T82, X123), T81, T82, T83) → U4_aggg(T82, X123, T81, T83, appendD_in_agg(X123, T81, T83))
appendD_in_agg([], T90, T90) → appendD_out_agg([], T90, T90)
appendD_in_agg(.(T98, X148), T97, .(T98, T99)) → U3_agg(T98, X148, T97, T99, appendD_in_agg(X148, T97, T99))
U3_agg(T98, X148, T97, T99, appendD_out_agg(X148, T97, T99)) → appendD_out_agg(.(T98, X148), T97, .(T98, T99))
U4_aggg(T82, X123, T81, T83, appendD_out_agg(X123, T81, T83)) → appendE_out_aggg(.(T82, X123), T81, T82, T83)
U6_aagagg(T37, T38, T29, X9, T5, T28, appendE_out_aggg(X9, T5, T28, T37)) → pB_out_aagagg(T37, T38, T29, X9, T5, T28)
U1_gg(T5, T28, T29, pB_out_aagagg(X56, X57, T29, X9, T5, T28)) → sublistA_out_gg(T5, .(T28, T29))
APPENDC_IN_AAG(.(T49, X93), X94, .(T49, T50)) → APPENDC_IN_AAG(X93, X94, T50)
APPENDC_IN_AAG(.(T49, T50)) → APPENDC_IN_AAG(T50)
From the DPs we obtained the following set of size-change graphs: