0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 85 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 41 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 0 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 8 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
sublistC_in_ag([], T16) → sublistC_out_ag([], T16)
sublistC_in_ag(T7, .(T29, T30)) → U3_ag(T7, T29, T30, appendA_in_aag(X56, X57, T30))
appendA_in_aag([], T45, T45) → appendA_out_aag([], T45, T45)
appendA_in_aag(.(T50, X93), X94, .(T50, T51)) → U1_aag(T50, X93, X94, T51, appendA_in_aag(X93, X94, T51))
U1_aag(T50, X93, X94, T51, appendA_out_aag(X93, X94, T51)) → appendA_out_aag(.(T50, X93), X94, .(T50, T51))
U3_ag(T7, T29, T30, appendA_out_aag(X56, X57, T30)) → sublistC_out_ag(T7, .(T29, T30))
sublistC_in_ag(.(T72, T73), .(T72, T30)) → U4_ag(T72, T73, T30, appendA_in_aag(T73, T39, T30))
U4_ag(T72, T73, T30, appendA_out_aag(T73, T39, T30)) → sublistC_out_ag(.(T72, T73), .(T72, T30))
sublistC_in_ag(T86, .(T84, T30)) → U5_ag(T86, T84, T30, appendA_in_aag(T85, T39, T30))
U5_ag(T86, T84, T30, appendA_out_aag(T85, T39, T30)) → U6_ag(T86, T84, T30, appendB_in_aag(X123, T86, T85))
appendB_in_aag([], T93, T93) → appendB_out_aag([], T93, T93)
appendB_in_aag(.(T101, X148), T103, .(T101, T102)) → U2_aag(T101, X148, T103, T102, appendB_in_aag(X148, T103, T102))
U2_aag(T101, X148, T103, T102, appendB_out_aag(X148, T103, T102)) → appendB_out_aag(.(T101, X148), T103, .(T101, T102))
U6_ag(T86, T84, T30, appendB_out_aag(X123, T86, T85)) → sublistC_out_ag(T86, .(T84, T30))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
sublistC_in_ag([], T16) → sublistC_out_ag([], T16)
sublistC_in_ag(T7, .(T29, T30)) → U3_ag(T7, T29, T30, appendA_in_aag(X56, X57, T30))
appendA_in_aag([], T45, T45) → appendA_out_aag([], T45, T45)
appendA_in_aag(.(T50, X93), X94, .(T50, T51)) → U1_aag(T50, X93, X94, T51, appendA_in_aag(X93, X94, T51))
U1_aag(T50, X93, X94, T51, appendA_out_aag(X93, X94, T51)) → appendA_out_aag(.(T50, X93), X94, .(T50, T51))
U3_ag(T7, T29, T30, appendA_out_aag(X56, X57, T30)) → sublistC_out_ag(T7, .(T29, T30))
sublistC_in_ag(.(T72, T73), .(T72, T30)) → U4_ag(T72, T73, T30, appendA_in_aag(T73, T39, T30))
U4_ag(T72, T73, T30, appendA_out_aag(T73, T39, T30)) → sublistC_out_ag(.(T72, T73), .(T72, T30))
sublistC_in_ag(T86, .(T84, T30)) → U5_ag(T86, T84, T30, appendA_in_aag(T85, T39, T30))
U5_ag(T86, T84, T30, appendA_out_aag(T85, T39, T30)) → U6_ag(T86, T84, T30, appendB_in_aag(X123, T86, T85))
appendB_in_aag([], T93, T93) → appendB_out_aag([], T93, T93)
appendB_in_aag(.(T101, X148), T103, .(T101, T102)) → U2_aag(T101, X148, T103, T102, appendB_in_aag(X148, T103, T102))
U2_aag(T101, X148, T103, T102, appendB_out_aag(X148, T103, T102)) → appendB_out_aag(.(T101, X148), T103, .(T101, T102))
U6_ag(T86, T84, T30, appendB_out_aag(X123, T86, T85)) → sublistC_out_ag(T86, .(T84, T30))
SUBLISTC_IN_AG(T7, .(T29, T30)) → U3_AG(T7, T29, T30, appendA_in_aag(X56, X57, T30))
SUBLISTC_IN_AG(T7, .(T29, T30)) → APPENDA_IN_AAG(X56, X57, T30)
APPENDA_IN_AAG(.(T50, X93), X94, .(T50, T51)) → U1_AAG(T50, X93, X94, T51, appendA_in_aag(X93, X94, T51))
APPENDA_IN_AAG(.(T50, X93), X94, .(T50, T51)) → APPENDA_IN_AAG(X93, X94, T51)
SUBLISTC_IN_AG(.(T72, T73), .(T72, T30)) → U4_AG(T72, T73, T30, appendA_in_aag(T73, T39, T30))
SUBLISTC_IN_AG(.(T72, T73), .(T72, T30)) → APPENDA_IN_AAG(T73, T39, T30)
SUBLISTC_IN_AG(T86, .(T84, T30)) → U5_AG(T86, T84, T30, appendA_in_aag(T85, T39, T30))
U5_AG(T86, T84, T30, appendA_out_aag(T85, T39, T30)) → U6_AG(T86, T84, T30, appendB_in_aag(X123, T86, T85))
U5_AG(T86, T84, T30, appendA_out_aag(T85, T39, T30)) → APPENDB_IN_AAG(X123, T86, T85)
APPENDB_IN_AAG(.(T101, X148), T103, .(T101, T102)) → U2_AAG(T101, X148, T103, T102, appendB_in_aag(X148, T103, T102))
APPENDB_IN_AAG(.(T101, X148), T103, .(T101, T102)) → APPENDB_IN_AAG(X148, T103, T102)
sublistC_in_ag([], T16) → sublistC_out_ag([], T16)
sublistC_in_ag(T7, .(T29, T30)) → U3_ag(T7, T29, T30, appendA_in_aag(X56, X57, T30))
appendA_in_aag([], T45, T45) → appendA_out_aag([], T45, T45)
appendA_in_aag(.(T50, X93), X94, .(T50, T51)) → U1_aag(T50, X93, X94, T51, appendA_in_aag(X93, X94, T51))
U1_aag(T50, X93, X94, T51, appendA_out_aag(X93, X94, T51)) → appendA_out_aag(.(T50, X93), X94, .(T50, T51))
U3_ag(T7, T29, T30, appendA_out_aag(X56, X57, T30)) → sublistC_out_ag(T7, .(T29, T30))
sublistC_in_ag(.(T72, T73), .(T72, T30)) → U4_ag(T72, T73, T30, appendA_in_aag(T73, T39, T30))
U4_ag(T72, T73, T30, appendA_out_aag(T73, T39, T30)) → sublistC_out_ag(.(T72, T73), .(T72, T30))
sublistC_in_ag(T86, .(T84, T30)) → U5_ag(T86, T84, T30, appendA_in_aag(T85, T39, T30))
U5_ag(T86, T84, T30, appendA_out_aag(T85, T39, T30)) → U6_ag(T86, T84, T30, appendB_in_aag(X123, T86, T85))
appendB_in_aag([], T93, T93) → appendB_out_aag([], T93, T93)
appendB_in_aag(.(T101, X148), T103, .(T101, T102)) → U2_aag(T101, X148, T103, T102, appendB_in_aag(X148, T103, T102))
U2_aag(T101, X148, T103, T102, appendB_out_aag(X148, T103, T102)) → appendB_out_aag(.(T101, X148), T103, .(T101, T102))
U6_ag(T86, T84, T30, appendB_out_aag(X123, T86, T85)) → sublistC_out_ag(T86, .(T84, T30))
SUBLISTC_IN_AG(T7, .(T29, T30)) → U3_AG(T7, T29, T30, appendA_in_aag(X56, X57, T30))
SUBLISTC_IN_AG(T7, .(T29, T30)) → APPENDA_IN_AAG(X56, X57, T30)
APPENDA_IN_AAG(.(T50, X93), X94, .(T50, T51)) → U1_AAG(T50, X93, X94, T51, appendA_in_aag(X93, X94, T51))
APPENDA_IN_AAG(.(T50, X93), X94, .(T50, T51)) → APPENDA_IN_AAG(X93, X94, T51)
SUBLISTC_IN_AG(.(T72, T73), .(T72, T30)) → U4_AG(T72, T73, T30, appendA_in_aag(T73, T39, T30))
SUBLISTC_IN_AG(.(T72, T73), .(T72, T30)) → APPENDA_IN_AAG(T73, T39, T30)
SUBLISTC_IN_AG(T86, .(T84, T30)) → U5_AG(T86, T84, T30, appendA_in_aag(T85, T39, T30))
U5_AG(T86, T84, T30, appendA_out_aag(T85, T39, T30)) → U6_AG(T86, T84, T30, appendB_in_aag(X123, T86, T85))
U5_AG(T86, T84, T30, appendA_out_aag(T85, T39, T30)) → APPENDB_IN_AAG(X123, T86, T85)
APPENDB_IN_AAG(.(T101, X148), T103, .(T101, T102)) → U2_AAG(T101, X148, T103, T102, appendB_in_aag(X148, T103, T102))
APPENDB_IN_AAG(.(T101, X148), T103, .(T101, T102)) → APPENDB_IN_AAG(X148, T103, T102)
sublistC_in_ag([], T16) → sublistC_out_ag([], T16)
sublistC_in_ag(T7, .(T29, T30)) → U3_ag(T7, T29, T30, appendA_in_aag(X56, X57, T30))
appendA_in_aag([], T45, T45) → appendA_out_aag([], T45, T45)
appendA_in_aag(.(T50, X93), X94, .(T50, T51)) → U1_aag(T50, X93, X94, T51, appendA_in_aag(X93, X94, T51))
U1_aag(T50, X93, X94, T51, appendA_out_aag(X93, X94, T51)) → appendA_out_aag(.(T50, X93), X94, .(T50, T51))
U3_ag(T7, T29, T30, appendA_out_aag(X56, X57, T30)) → sublistC_out_ag(T7, .(T29, T30))
sublistC_in_ag(.(T72, T73), .(T72, T30)) → U4_ag(T72, T73, T30, appendA_in_aag(T73, T39, T30))
U4_ag(T72, T73, T30, appendA_out_aag(T73, T39, T30)) → sublistC_out_ag(.(T72, T73), .(T72, T30))
sublistC_in_ag(T86, .(T84, T30)) → U5_ag(T86, T84, T30, appendA_in_aag(T85, T39, T30))
U5_ag(T86, T84, T30, appendA_out_aag(T85, T39, T30)) → U6_ag(T86, T84, T30, appendB_in_aag(X123, T86, T85))
appendB_in_aag([], T93, T93) → appendB_out_aag([], T93, T93)
appendB_in_aag(.(T101, X148), T103, .(T101, T102)) → U2_aag(T101, X148, T103, T102, appendB_in_aag(X148, T103, T102))
U2_aag(T101, X148, T103, T102, appendB_out_aag(X148, T103, T102)) → appendB_out_aag(.(T101, X148), T103, .(T101, T102))
U6_ag(T86, T84, T30, appendB_out_aag(X123, T86, T85)) → sublistC_out_ag(T86, .(T84, T30))
APPENDB_IN_AAG(.(T101, X148), T103, .(T101, T102)) → APPENDB_IN_AAG(X148, T103, T102)
sublistC_in_ag([], T16) → sublistC_out_ag([], T16)
sublistC_in_ag(T7, .(T29, T30)) → U3_ag(T7, T29, T30, appendA_in_aag(X56, X57, T30))
appendA_in_aag([], T45, T45) → appendA_out_aag([], T45, T45)
appendA_in_aag(.(T50, X93), X94, .(T50, T51)) → U1_aag(T50, X93, X94, T51, appendA_in_aag(X93, X94, T51))
U1_aag(T50, X93, X94, T51, appendA_out_aag(X93, X94, T51)) → appendA_out_aag(.(T50, X93), X94, .(T50, T51))
U3_ag(T7, T29, T30, appendA_out_aag(X56, X57, T30)) → sublistC_out_ag(T7, .(T29, T30))
sublistC_in_ag(.(T72, T73), .(T72, T30)) → U4_ag(T72, T73, T30, appendA_in_aag(T73, T39, T30))
U4_ag(T72, T73, T30, appendA_out_aag(T73, T39, T30)) → sublistC_out_ag(.(T72, T73), .(T72, T30))
sublistC_in_ag(T86, .(T84, T30)) → U5_ag(T86, T84, T30, appendA_in_aag(T85, T39, T30))
U5_ag(T86, T84, T30, appendA_out_aag(T85, T39, T30)) → U6_ag(T86, T84, T30, appendB_in_aag(X123, T86, T85))
appendB_in_aag([], T93, T93) → appendB_out_aag([], T93, T93)
appendB_in_aag(.(T101, X148), T103, .(T101, T102)) → U2_aag(T101, X148, T103, T102, appendB_in_aag(X148, T103, T102))
U2_aag(T101, X148, T103, T102, appendB_out_aag(X148, T103, T102)) → appendB_out_aag(.(T101, X148), T103, .(T101, T102))
U6_ag(T86, T84, T30, appendB_out_aag(X123, T86, T85)) → sublistC_out_ag(T86, .(T84, T30))
APPENDB_IN_AAG(.(T101, X148), T103, .(T101, T102)) → APPENDB_IN_AAG(X148, T103, T102)
APPENDB_IN_AAG(.(T101, T102)) → APPENDB_IN_AAG(T102)
From the DPs we obtained the following set of size-change graphs:
APPENDA_IN_AAG(.(T50, X93), X94, .(T50, T51)) → APPENDA_IN_AAG(X93, X94, T51)
sublistC_in_ag([], T16) → sublistC_out_ag([], T16)
sublistC_in_ag(T7, .(T29, T30)) → U3_ag(T7, T29, T30, appendA_in_aag(X56, X57, T30))
appendA_in_aag([], T45, T45) → appendA_out_aag([], T45, T45)
appendA_in_aag(.(T50, X93), X94, .(T50, T51)) → U1_aag(T50, X93, X94, T51, appendA_in_aag(X93, X94, T51))
U1_aag(T50, X93, X94, T51, appendA_out_aag(X93, X94, T51)) → appendA_out_aag(.(T50, X93), X94, .(T50, T51))
U3_ag(T7, T29, T30, appendA_out_aag(X56, X57, T30)) → sublistC_out_ag(T7, .(T29, T30))
sublistC_in_ag(.(T72, T73), .(T72, T30)) → U4_ag(T72, T73, T30, appendA_in_aag(T73, T39, T30))
U4_ag(T72, T73, T30, appendA_out_aag(T73, T39, T30)) → sublistC_out_ag(.(T72, T73), .(T72, T30))
sublistC_in_ag(T86, .(T84, T30)) → U5_ag(T86, T84, T30, appendA_in_aag(T85, T39, T30))
U5_ag(T86, T84, T30, appendA_out_aag(T85, T39, T30)) → U6_ag(T86, T84, T30, appendB_in_aag(X123, T86, T85))
appendB_in_aag([], T93, T93) → appendB_out_aag([], T93, T93)
appendB_in_aag(.(T101, X148), T103, .(T101, T102)) → U2_aag(T101, X148, T103, T102, appendB_in_aag(X148, T103, T102))
U2_aag(T101, X148, T103, T102, appendB_out_aag(X148, T103, T102)) → appendB_out_aag(.(T101, X148), T103, .(T101, T102))
U6_ag(T86, T84, T30, appendB_out_aag(X123, T86, T85)) → sublistC_out_ag(T86, .(T84, T30))
APPENDA_IN_AAG(.(T50, X93), X94, .(T50, T51)) → APPENDA_IN_AAG(X93, X94, T51)
APPENDA_IN_AAG(.(T50, T51)) → APPENDA_IN_AAG(T51)
From the DPs we obtained the following set of size-change graphs: