0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 137 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 57 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 0 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, append1C_in_aag(T37, T38, T29))
append1C_in_aag([], T44, T44) → append1C_out_aag([], T44, T44)
append1C_in_aag(.(T49, X93), X94, .(T49, T50)) → U2_aag(T49, X93, X94, T50, append1C_in_aag(X93, X94, T50))
U2_aag(T49, X93, X94, T50, append1C_out_aag(X93, X94, T50)) → append1C_out_aag(.(T49, X93), X94, .(T49, T50))
U5_aagagg(T37, T38, T29, X9, T5, T28, append1C_out_aag(T37, T38, T29)) → U6_aagagg(T37, T38, T29, X9, T5, T28, append2E_in_aggg(X9, T5, T28, T37))
append2E_in_aggg([], .(T71, T72), T71, T72) → append2E_out_aggg([], .(T71, T72), T71, T72)
append2E_in_aggg(.(T82, X123), T81, T82, T83) → U4_aggg(T82, X123, T81, T83, append2D_in_agg(X123, T81, T83))
append2D_in_agg([], T90, T90) → append2D_out_agg([], T90, T90)
append2D_in_agg(.(T98, X148), T97, .(T98, T99)) → U3_agg(T98, X148, T97, T99, append2D_in_agg(X148, T97, T99))
U3_agg(T98, X148, T97, T99, append2D_out_agg(X148, T97, T99)) → append2D_out_agg(.(T98, X148), T97, .(T98, T99))
U4_aggg(T82, X123, T81, T83, append2D_out_agg(X123, T81, T83)) → append2E_out_aggg(.(T82, X123), T81, T82, T83)
U6_aagagg(T37, T38, T29, X9, T5, T28, append2E_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, append1C_in_aag(T37, T38, T29))
PB_IN_AAGAGG(T37, T38, T29, X9, T5, T28) → APPEND1C_IN_AAG(T37, T38, T29)
APPEND1C_IN_AAG(.(T49, X93), X94, .(T49, T50)) → U2_AAG(T49, X93, X94, T50, append1C_in_aag(X93, X94, T50))
APPEND1C_IN_AAG(.(T49, X93), X94, .(T49, T50)) → APPEND1C_IN_AAG(X93, X94, T50)
U5_AAGAGG(T37, T38, T29, X9, T5, T28, append1C_out_aag(T37, T38, T29)) → U6_AAGAGG(T37, T38, T29, X9, T5, T28, append2E_in_aggg(X9, T5, T28, T37))
U5_AAGAGG(T37, T38, T29, X9, T5, T28, append1C_out_aag(T37, T38, T29)) → APPEND2E_IN_AGGG(X9, T5, T28, T37)
APPEND2E_IN_AGGG(.(T82, X123), T81, T82, T83) → U4_AGGG(T82, X123, T81, T83, append2D_in_agg(X123, T81, T83))
APPEND2E_IN_AGGG(.(T82, X123), T81, T82, T83) → APPEND2D_IN_AGG(X123, T81, T83)
APPEND2D_IN_AGG(.(T98, X148), T97, .(T98, T99)) → U3_AGG(T98, X148, T97, T99, append2D_in_agg(X148, T97, T99))
APPEND2D_IN_AGG(.(T98, X148), T97, .(T98, T99)) → APPEND2D_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, append1C_in_aag(T37, T38, T29))
append1C_in_aag([], T44, T44) → append1C_out_aag([], T44, T44)
append1C_in_aag(.(T49, X93), X94, .(T49, T50)) → U2_aag(T49, X93, X94, T50, append1C_in_aag(X93, X94, T50))
U2_aag(T49, X93, X94, T50, append1C_out_aag(X93, X94, T50)) → append1C_out_aag(.(T49, X93), X94, .(T49, T50))
U5_aagagg(T37, T38, T29, X9, T5, T28, append1C_out_aag(T37, T38, T29)) → U6_aagagg(T37, T38, T29, X9, T5, T28, append2E_in_aggg(X9, T5, T28, T37))
append2E_in_aggg([], .(T71, T72), T71, T72) → append2E_out_aggg([], .(T71, T72), T71, T72)
append2E_in_aggg(.(T82, X123), T81, T82, T83) → U4_aggg(T82, X123, T81, T83, append2D_in_agg(X123, T81, T83))
append2D_in_agg([], T90, T90) → append2D_out_agg([], T90, T90)
append2D_in_agg(.(T98, X148), T97, .(T98, T99)) → U3_agg(T98, X148, T97, T99, append2D_in_agg(X148, T97, T99))
U3_agg(T98, X148, T97, T99, append2D_out_agg(X148, T97, T99)) → append2D_out_agg(.(T98, X148), T97, .(T98, T99))
U4_aggg(T82, X123, T81, T83, append2D_out_agg(X123, T81, T83)) → append2E_out_aggg(.(T82, X123), T81, T82, T83)
U6_aagagg(T37, T38, T29, X9, T5, T28, append2E_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, append1C_in_aag(T37, T38, T29))
PB_IN_AAGAGG(T37, T38, T29, X9, T5, T28) → APPEND1C_IN_AAG(T37, T38, T29)
APPEND1C_IN_AAG(.(T49, X93), X94, .(T49, T50)) → U2_AAG(T49, X93, X94, T50, append1C_in_aag(X93, X94, T50))
APPEND1C_IN_AAG(.(T49, X93), X94, .(T49, T50)) → APPEND1C_IN_AAG(X93, X94, T50)
U5_AAGAGG(T37, T38, T29, X9, T5, T28, append1C_out_aag(T37, T38, T29)) → U6_AAGAGG(T37, T38, T29, X9, T5, T28, append2E_in_aggg(X9, T5, T28, T37))
U5_AAGAGG(T37, T38, T29, X9, T5, T28, append1C_out_aag(T37, T38, T29)) → APPEND2E_IN_AGGG(X9, T5, T28, T37)
APPEND2E_IN_AGGG(.(T82, X123), T81, T82, T83) → U4_AGGG(T82, X123, T81, T83, append2D_in_agg(X123, T81, T83))
APPEND2E_IN_AGGG(.(T82, X123), T81, T82, T83) → APPEND2D_IN_AGG(X123, T81, T83)
APPEND2D_IN_AGG(.(T98, X148), T97, .(T98, T99)) → U3_AGG(T98, X148, T97, T99, append2D_in_agg(X148, T97, T99))
APPEND2D_IN_AGG(.(T98, X148), T97, .(T98, T99)) → APPEND2D_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, append1C_in_aag(T37, T38, T29))
append1C_in_aag([], T44, T44) → append1C_out_aag([], T44, T44)
append1C_in_aag(.(T49, X93), X94, .(T49, T50)) → U2_aag(T49, X93, X94, T50, append1C_in_aag(X93, X94, T50))
U2_aag(T49, X93, X94, T50, append1C_out_aag(X93, X94, T50)) → append1C_out_aag(.(T49, X93), X94, .(T49, T50))
U5_aagagg(T37, T38, T29, X9, T5, T28, append1C_out_aag(T37, T38, T29)) → U6_aagagg(T37, T38, T29, X9, T5, T28, append2E_in_aggg(X9, T5, T28, T37))
append2E_in_aggg([], .(T71, T72), T71, T72) → append2E_out_aggg([], .(T71, T72), T71, T72)
append2E_in_aggg(.(T82, X123), T81, T82, T83) → U4_aggg(T82, X123, T81, T83, append2D_in_agg(X123, T81, T83))
append2D_in_agg([], T90, T90) → append2D_out_agg([], T90, T90)
append2D_in_agg(.(T98, X148), T97, .(T98, T99)) → U3_agg(T98, X148, T97, T99, append2D_in_agg(X148, T97, T99))
U3_agg(T98, X148, T97, T99, append2D_out_agg(X148, T97, T99)) → append2D_out_agg(.(T98, X148), T97, .(T98, T99))
U4_aggg(T82, X123, T81, T83, append2D_out_agg(X123, T81, T83)) → append2E_out_aggg(.(T82, X123), T81, T82, T83)
U6_aagagg(T37, T38, T29, X9, T5, T28, append2E_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))
APPEND2D_IN_AGG(.(T98, X148), T97, .(T98, T99)) → APPEND2D_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, append1C_in_aag(T37, T38, T29))
append1C_in_aag([], T44, T44) → append1C_out_aag([], T44, T44)
append1C_in_aag(.(T49, X93), X94, .(T49, T50)) → U2_aag(T49, X93, X94, T50, append1C_in_aag(X93, X94, T50))
U2_aag(T49, X93, X94, T50, append1C_out_aag(X93, X94, T50)) → append1C_out_aag(.(T49, X93), X94, .(T49, T50))
U5_aagagg(T37, T38, T29, X9, T5, T28, append1C_out_aag(T37, T38, T29)) → U6_aagagg(T37, T38, T29, X9, T5, T28, append2E_in_aggg(X9, T5, T28, T37))
append2E_in_aggg([], .(T71, T72), T71, T72) → append2E_out_aggg([], .(T71, T72), T71, T72)
append2E_in_aggg(.(T82, X123), T81, T82, T83) → U4_aggg(T82, X123, T81, T83, append2D_in_agg(X123, T81, T83))
append2D_in_agg([], T90, T90) → append2D_out_agg([], T90, T90)
append2D_in_agg(.(T98, X148), T97, .(T98, T99)) → U3_agg(T98, X148, T97, T99, append2D_in_agg(X148, T97, T99))
U3_agg(T98, X148, T97, T99, append2D_out_agg(X148, T97, T99)) → append2D_out_agg(.(T98, X148), T97, .(T98, T99))
U4_aggg(T82, X123, T81, T83, append2D_out_agg(X123, T81, T83)) → append2E_out_aggg(.(T82, X123), T81, T82, T83)
U6_aagagg(T37, T38, T29, X9, T5, T28, append2E_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))
APPEND2D_IN_AGG(.(T98, X148), T97, .(T98, T99)) → APPEND2D_IN_AGG(X148, T97, T99)
APPEND2D_IN_AGG(T97, .(T98, T99)) → APPEND2D_IN_AGG(T97, T99)
From the DPs we obtained the following set of size-change graphs:
APPEND1C_IN_AAG(.(T49, X93), X94, .(T49, T50)) → APPEND1C_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, append1C_in_aag(T37, T38, T29))
append1C_in_aag([], T44, T44) → append1C_out_aag([], T44, T44)
append1C_in_aag(.(T49, X93), X94, .(T49, T50)) → U2_aag(T49, X93, X94, T50, append1C_in_aag(X93, X94, T50))
U2_aag(T49, X93, X94, T50, append1C_out_aag(X93, X94, T50)) → append1C_out_aag(.(T49, X93), X94, .(T49, T50))
U5_aagagg(T37, T38, T29, X9, T5, T28, append1C_out_aag(T37, T38, T29)) → U6_aagagg(T37, T38, T29, X9, T5, T28, append2E_in_aggg(X9, T5, T28, T37))
append2E_in_aggg([], .(T71, T72), T71, T72) → append2E_out_aggg([], .(T71, T72), T71, T72)
append2E_in_aggg(.(T82, X123), T81, T82, T83) → U4_aggg(T82, X123, T81, T83, append2D_in_agg(X123, T81, T83))
append2D_in_agg([], T90, T90) → append2D_out_agg([], T90, T90)
append2D_in_agg(.(T98, X148), T97, .(T98, T99)) → U3_agg(T98, X148, T97, T99, append2D_in_agg(X148, T97, T99))
U3_agg(T98, X148, T97, T99, append2D_out_agg(X148, T97, T99)) → append2D_out_agg(.(T98, X148), T97, .(T98, T99))
U4_aggg(T82, X123, T81, T83, append2D_out_agg(X123, T81, T83)) → append2E_out_aggg(.(T82, X123), T81, T82, T83)
U6_aagagg(T37, T38, T29, X9, T5, T28, append2E_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))
APPEND1C_IN_AAG(.(T49, X93), X94, .(T49, T50)) → APPEND1C_IN_AAG(X93, X94, T50)
APPEND1C_IN_AAG(.(T49, T50)) → APPEND1C_IN_AAG(T50)
From the DPs we obtained the following set of size-change graphs: