0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 63 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 37 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 15 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
append3A_in_ggga([], T18, T11, T13) → U1_ggga(T18, T11, T13, appendB_in_gga(T18, T11, T13))
appendB_in_gga([], T25, T25) → appendB_out_gga([], T25, T25)
appendB_in_gga(.(T34, T35), T36, .(T34, T38)) → U3_gga(T34, T35, T36, T38, appendB_in_gga(T35, T36, T38))
U3_gga(T34, T35, T36, T38, appendB_out_gga(T35, T36, T38)) → appendB_out_gga(.(T34, T35), T36, .(T34, T38))
U1_ggga(T18, T11, T13, appendB_out_gga(T18, T11, T13)) → append3A_out_ggga([], T18, T11, T13)
append3A_in_ggga(.(T47, T48), T49, T11, T13) → U2_ggga(T47, T48, T49, T11, T13, pC_in_ggagga(T48, T49, X50, T47, T11, T13))
pC_in_ggagga(T48, T49, T52, T47, T11, T13) → U5_ggagga(T48, T49, T52, T47, T11, T13, appendD_in_gga(T48, T49, T52))
appendD_in_gga([], T59, T59) → appendD_out_gga([], T59, T59)
appendD_in_gga(.(T66, T67), T68, .(T66, X74)) → U4_gga(T66, T67, T68, X74, appendD_in_gga(T67, T68, X74))
U4_gga(T66, T67, T68, X74, appendD_out_gga(T67, T68, X74)) → appendD_out_gga(.(T66, T67), T68, .(T66, X74))
U5_ggagga(T48, T49, T52, T47, T11, T13, appendD_out_gga(T48, T49, T52)) → U6_ggagga(T48, T49, T52, T47, T11, T13, appendB_in_gga(.(T47, T52), T11, T13))
U6_ggagga(T48, T49, T52, T47, T11, T13, appendB_out_gga(.(T47, T52), T11, T13)) → pC_out_ggagga(T48, T49, T52, T47, T11, T13)
U2_ggga(T47, T48, T49, T11, T13, pC_out_ggagga(T48, T49, X50, T47, T11, T13)) → append3A_out_ggga(.(T47, T48), T49, T11, T13)
APPEND3A_IN_GGGA([], T18, T11, T13) → U1_GGGA(T18, T11, T13, appendB_in_gga(T18, T11, T13))
APPEND3A_IN_GGGA([], T18, T11, T13) → APPENDB_IN_GGA(T18, T11, T13)
APPENDB_IN_GGA(.(T34, T35), T36, .(T34, T38)) → U3_GGA(T34, T35, T36, T38, appendB_in_gga(T35, T36, T38))
APPENDB_IN_GGA(.(T34, T35), T36, .(T34, T38)) → APPENDB_IN_GGA(T35, T36, T38)
APPEND3A_IN_GGGA(.(T47, T48), T49, T11, T13) → U2_GGGA(T47, T48, T49, T11, T13, pC_in_ggagga(T48, T49, X50, T47, T11, T13))
APPEND3A_IN_GGGA(.(T47, T48), T49, T11, T13) → PC_IN_GGAGGA(T48, T49, X50, T47, T11, T13)
PC_IN_GGAGGA(T48, T49, T52, T47, T11, T13) → U5_GGAGGA(T48, T49, T52, T47, T11, T13, appendD_in_gga(T48, T49, T52))
PC_IN_GGAGGA(T48, T49, T52, T47, T11, T13) → APPENDD_IN_GGA(T48, T49, T52)
APPENDD_IN_GGA(.(T66, T67), T68, .(T66, X74)) → U4_GGA(T66, T67, T68, X74, appendD_in_gga(T67, T68, X74))
APPENDD_IN_GGA(.(T66, T67), T68, .(T66, X74)) → APPENDD_IN_GGA(T67, T68, X74)
U5_GGAGGA(T48, T49, T52, T47, T11, T13, appendD_out_gga(T48, T49, T52)) → U6_GGAGGA(T48, T49, T52, T47, T11, T13, appendB_in_gga(.(T47, T52), T11, T13))
U5_GGAGGA(T48, T49, T52, T47, T11, T13, appendD_out_gga(T48, T49, T52)) → APPENDB_IN_GGA(.(T47, T52), T11, T13)
append3A_in_ggga([], T18, T11, T13) → U1_ggga(T18, T11, T13, appendB_in_gga(T18, T11, T13))
appendB_in_gga([], T25, T25) → appendB_out_gga([], T25, T25)
appendB_in_gga(.(T34, T35), T36, .(T34, T38)) → U3_gga(T34, T35, T36, T38, appendB_in_gga(T35, T36, T38))
U3_gga(T34, T35, T36, T38, appendB_out_gga(T35, T36, T38)) → appendB_out_gga(.(T34, T35), T36, .(T34, T38))
U1_ggga(T18, T11, T13, appendB_out_gga(T18, T11, T13)) → append3A_out_ggga([], T18, T11, T13)
append3A_in_ggga(.(T47, T48), T49, T11, T13) → U2_ggga(T47, T48, T49, T11, T13, pC_in_ggagga(T48, T49, X50, T47, T11, T13))
pC_in_ggagga(T48, T49, T52, T47, T11, T13) → U5_ggagga(T48, T49, T52, T47, T11, T13, appendD_in_gga(T48, T49, T52))
appendD_in_gga([], T59, T59) → appendD_out_gga([], T59, T59)
appendD_in_gga(.(T66, T67), T68, .(T66, X74)) → U4_gga(T66, T67, T68, X74, appendD_in_gga(T67, T68, X74))
U4_gga(T66, T67, T68, X74, appendD_out_gga(T67, T68, X74)) → appendD_out_gga(.(T66, T67), T68, .(T66, X74))
U5_ggagga(T48, T49, T52, T47, T11, T13, appendD_out_gga(T48, T49, T52)) → U6_ggagga(T48, T49, T52, T47, T11, T13, appendB_in_gga(.(T47, T52), T11, T13))
U6_ggagga(T48, T49, T52, T47, T11, T13, appendB_out_gga(.(T47, T52), T11, T13)) → pC_out_ggagga(T48, T49, T52, T47, T11, T13)
U2_ggga(T47, T48, T49, T11, T13, pC_out_ggagga(T48, T49, X50, T47, T11, T13)) → append3A_out_ggga(.(T47, T48), T49, T11, T13)
APPEND3A_IN_GGGA([], T18, T11, T13) → U1_GGGA(T18, T11, T13, appendB_in_gga(T18, T11, T13))
APPEND3A_IN_GGGA([], T18, T11, T13) → APPENDB_IN_GGA(T18, T11, T13)
APPENDB_IN_GGA(.(T34, T35), T36, .(T34, T38)) → U3_GGA(T34, T35, T36, T38, appendB_in_gga(T35, T36, T38))
APPENDB_IN_GGA(.(T34, T35), T36, .(T34, T38)) → APPENDB_IN_GGA(T35, T36, T38)
APPEND3A_IN_GGGA(.(T47, T48), T49, T11, T13) → U2_GGGA(T47, T48, T49, T11, T13, pC_in_ggagga(T48, T49, X50, T47, T11, T13))
APPEND3A_IN_GGGA(.(T47, T48), T49, T11, T13) → PC_IN_GGAGGA(T48, T49, X50, T47, T11, T13)
PC_IN_GGAGGA(T48, T49, T52, T47, T11, T13) → U5_GGAGGA(T48, T49, T52, T47, T11, T13, appendD_in_gga(T48, T49, T52))
PC_IN_GGAGGA(T48, T49, T52, T47, T11, T13) → APPENDD_IN_GGA(T48, T49, T52)
APPENDD_IN_GGA(.(T66, T67), T68, .(T66, X74)) → U4_GGA(T66, T67, T68, X74, appendD_in_gga(T67, T68, X74))
APPENDD_IN_GGA(.(T66, T67), T68, .(T66, X74)) → APPENDD_IN_GGA(T67, T68, X74)
U5_GGAGGA(T48, T49, T52, T47, T11, T13, appendD_out_gga(T48, T49, T52)) → U6_GGAGGA(T48, T49, T52, T47, T11, T13, appendB_in_gga(.(T47, T52), T11, T13))
U5_GGAGGA(T48, T49, T52, T47, T11, T13, appendD_out_gga(T48, T49, T52)) → APPENDB_IN_GGA(.(T47, T52), T11, T13)
append3A_in_ggga([], T18, T11, T13) → U1_ggga(T18, T11, T13, appendB_in_gga(T18, T11, T13))
appendB_in_gga([], T25, T25) → appendB_out_gga([], T25, T25)
appendB_in_gga(.(T34, T35), T36, .(T34, T38)) → U3_gga(T34, T35, T36, T38, appendB_in_gga(T35, T36, T38))
U3_gga(T34, T35, T36, T38, appendB_out_gga(T35, T36, T38)) → appendB_out_gga(.(T34, T35), T36, .(T34, T38))
U1_ggga(T18, T11, T13, appendB_out_gga(T18, T11, T13)) → append3A_out_ggga([], T18, T11, T13)
append3A_in_ggga(.(T47, T48), T49, T11, T13) → U2_ggga(T47, T48, T49, T11, T13, pC_in_ggagga(T48, T49, X50, T47, T11, T13))
pC_in_ggagga(T48, T49, T52, T47, T11, T13) → U5_ggagga(T48, T49, T52, T47, T11, T13, appendD_in_gga(T48, T49, T52))
appendD_in_gga([], T59, T59) → appendD_out_gga([], T59, T59)
appendD_in_gga(.(T66, T67), T68, .(T66, X74)) → U4_gga(T66, T67, T68, X74, appendD_in_gga(T67, T68, X74))
U4_gga(T66, T67, T68, X74, appendD_out_gga(T67, T68, X74)) → appendD_out_gga(.(T66, T67), T68, .(T66, X74))
U5_ggagga(T48, T49, T52, T47, T11, T13, appendD_out_gga(T48, T49, T52)) → U6_ggagga(T48, T49, T52, T47, T11, T13, appendB_in_gga(.(T47, T52), T11, T13))
U6_ggagga(T48, T49, T52, T47, T11, T13, appendB_out_gga(.(T47, T52), T11, T13)) → pC_out_ggagga(T48, T49, T52, T47, T11, T13)
U2_ggga(T47, T48, T49, T11, T13, pC_out_ggagga(T48, T49, X50, T47, T11, T13)) → append3A_out_ggga(.(T47, T48), T49, T11, T13)
APPENDD_IN_GGA(.(T66, T67), T68, .(T66, X74)) → APPENDD_IN_GGA(T67, T68, X74)
append3A_in_ggga([], T18, T11, T13) → U1_ggga(T18, T11, T13, appendB_in_gga(T18, T11, T13))
appendB_in_gga([], T25, T25) → appendB_out_gga([], T25, T25)
appendB_in_gga(.(T34, T35), T36, .(T34, T38)) → U3_gga(T34, T35, T36, T38, appendB_in_gga(T35, T36, T38))
U3_gga(T34, T35, T36, T38, appendB_out_gga(T35, T36, T38)) → appendB_out_gga(.(T34, T35), T36, .(T34, T38))
U1_ggga(T18, T11, T13, appendB_out_gga(T18, T11, T13)) → append3A_out_ggga([], T18, T11, T13)
append3A_in_ggga(.(T47, T48), T49, T11, T13) → U2_ggga(T47, T48, T49, T11, T13, pC_in_ggagga(T48, T49, X50, T47, T11, T13))
pC_in_ggagga(T48, T49, T52, T47, T11, T13) → U5_ggagga(T48, T49, T52, T47, T11, T13, appendD_in_gga(T48, T49, T52))
appendD_in_gga([], T59, T59) → appendD_out_gga([], T59, T59)
appendD_in_gga(.(T66, T67), T68, .(T66, X74)) → U4_gga(T66, T67, T68, X74, appendD_in_gga(T67, T68, X74))
U4_gga(T66, T67, T68, X74, appendD_out_gga(T67, T68, X74)) → appendD_out_gga(.(T66, T67), T68, .(T66, X74))
U5_ggagga(T48, T49, T52, T47, T11, T13, appendD_out_gga(T48, T49, T52)) → U6_ggagga(T48, T49, T52, T47, T11, T13, appendB_in_gga(.(T47, T52), T11, T13))
U6_ggagga(T48, T49, T52, T47, T11, T13, appendB_out_gga(.(T47, T52), T11, T13)) → pC_out_ggagga(T48, T49, T52, T47, T11, T13)
U2_ggga(T47, T48, T49, T11, T13, pC_out_ggagga(T48, T49, X50, T47, T11, T13)) → append3A_out_ggga(.(T47, T48), T49, T11, T13)
APPENDD_IN_GGA(.(T66, T67), T68, .(T66, X74)) → APPENDD_IN_GGA(T67, T68, X74)
APPENDD_IN_GGA(.(T66, T67), T68) → APPENDD_IN_GGA(T67, T68)
From the DPs we obtained the following set of size-change graphs:
APPENDB_IN_GGA(.(T34, T35), T36, .(T34, T38)) → APPENDB_IN_GGA(T35, T36, T38)
append3A_in_ggga([], T18, T11, T13) → U1_ggga(T18, T11, T13, appendB_in_gga(T18, T11, T13))
appendB_in_gga([], T25, T25) → appendB_out_gga([], T25, T25)
appendB_in_gga(.(T34, T35), T36, .(T34, T38)) → U3_gga(T34, T35, T36, T38, appendB_in_gga(T35, T36, T38))
U3_gga(T34, T35, T36, T38, appendB_out_gga(T35, T36, T38)) → appendB_out_gga(.(T34, T35), T36, .(T34, T38))
U1_ggga(T18, T11, T13, appendB_out_gga(T18, T11, T13)) → append3A_out_ggga([], T18, T11, T13)
append3A_in_ggga(.(T47, T48), T49, T11, T13) → U2_ggga(T47, T48, T49, T11, T13, pC_in_ggagga(T48, T49, X50, T47, T11, T13))
pC_in_ggagga(T48, T49, T52, T47, T11, T13) → U5_ggagga(T48, T49, T52, T47, T11, T13, appendD_in_gga(T48, T49, T52))
appendD_in_gga([], T59, T59) → appendD_out_gga([], T59, T59)
appendD_in_gga(.(T66, T67), T68, .(T66, X74)) → U4_gga(T66, T67, T68, X74, appendD_in_gga(T67, T68, X74))
U4_gga(T66, T67, T68, X74, appendD_out_gga(T67, T68, X74)) → appendD_out_gga(.(T66, T67), T68, .(T66, X74))
U5_ggagga(T48, T49, T52, T47, T11, T13, appendD_out_gga(T48, T49, T52)) → U6_ggagga(T48, T49, T52, T47, T11, T13, appendB_in_gga(.(T47, T52), T11, T13))
U6_ggagga(T48, T49, T52, T47, T11, T13, appendB_out_gga(.(T47, T52), T11, T13)) → pC_out_ggagga(T48, T49, T52, T47, T11, T13)
U2_ggga(T47, T48, T49, T11, T13, pC_out_ggagga(T48, T49, X50, T47, T11, T13)) → append3A_out_ggga(.(T47, T48), T49, T11, T13)
APPENDB_IN_GGA(.(T34, T35), T36, .(T34, T38)) → APPENDB_IN_GGA(T35, T36, T38)
APPENDB_IN_GGA(.(T34, T35), T36) → APPENDB_IN_GGA(T35, T36)
From the DPs we obtained the following set of size-change graphs: