0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 123 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 (⇒, 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
↳21 PiDP
↳22 UsableRulesProof (⇔, 0 ms)
↳23 PiDP
↳24 PiDPToQDPProof (⇒, 0 ms)
↳25 QDP
↳26 QDPSizeChangeProof (⇔, 0 ms)
↳27 YES
rotateA_in_ga(.(T16, T17), T7) → U1_ga(T16, T17, T7, pB_in_aagga(X40, X41, T17, T16, T7))
pB_in_aagga(T20, T21, T17, T16, T7) → U6_aagga(T20, T21, T17, T16, T7, appendD_in_aag(T20, T21, T17))
appendD_in_aag(.(T32, X89), X90, .(T32, T33)) → U3_aag(T32, X89, X90, T33, appendD_in_aag(X89, X90, T33))
appendD_in_aag([], T38, T38) → appendD_out_aag([], T38, T38)
U3_aag(T32, X89, X90, T33, appendD_out_aag(X89, X90, T33)) → appendD_out_aag(.(T32, X89), X90, .(T32, T33))
U6_aagga(T20, T21, T17, T16, T7, appendD_out_aag(T20, T21, T17)) → U7_aagga(T20, T21, T17, T16, T7, appendE_in_ggga(T21, T16, T20, T7))
appendE_in_ggga(.(T64, T65), T66, T67, .(T64, T69)) → U4_ggga(T64, T65, T66, T67, T69, appendE_in_ggga(T65, T66, T67, T69))
appendE_in_ggga([], T79, T80, .(T79, T80)) → appendE_out_ggga([], T79, T80, .(T79, T80))
U4_ggga(T64, T65, T66, T67, T69, appendE_out_ggga(T65, T66, T67, T69)) → appendE_out_ggga(.(T64, T65), T66, T67, .(T64, T69))
U7_aagga(T20, T21, T17, T16, T7, appendE_out_ggga(T21, T16, T20, T7)) → pB_out_aagga(T20, T21, T17, T16, T7)
U1_ga(T16, T17, T7, pB_out_aagga(X40, X41, T17, T16, T7)) → rotateA_out_ga(.(T16, T17), T7)
rotateA_in_ga(T86, T7) → U2_ga(T86, T7, appendC_in_ga(T86, T7))
appendC_in_ga(.(T102, T103), .(T102, T105)) → U5_ga(T102, T103, T105, appendC_in_ga(T103, T105))
appendC_in_ga([], []) → appendC_out_ga([], [])
U5_ga(T102, T103, T105, appendC_out_ga(T103, T105)) → appendC_out_ga(.(T102, T103), .(T102, T105))
U2_ga(T86, T7, appendC_out_ga(T86, T7)) → rotateA_out_ga(T86, T7)
ROTATEA_IN_GA(.(T16, T17), T7) → U1_GA(T16, T17, T7, pB_in_aagga(X40, X41, T17, T16, T7))
ROTATEA_IN_GA(.(T16, T17), T7) → PB_IN_AAGGA(X40, X41, T17, T16, T7)
PB_IN_AAGGA(T20, T21, T17, T16, T7) → U6_AAGGA(T20, T21, T17, T16, T7, appendD_in_aag(T20, T21, T17))
PB_IN_AAGGA(T20, T21, T17, T16, T7) → APPENDD_IN_AAG(T20, T21, T17)
APPENDD_IN_AAG(.(T32, X89), X90, .(T32, T33)) → U3_AAG(T32, X89, X90, T33, appendD_in_aag(X89, X90, T33))
APPENDD_IN_AAG(.(T32, X89), X90, .(T32, T33)) → APPENDD_IN_AAG(X89, X90, T33)
U6_AAGGA(T20, T21, T17, T16, T7, appendD_out_aag(T20, T21, T17)) → U7_AAGGA(T20, T21, T17, T16, T7, appendE_in_ggga(T21, T16, T20, T7))
U6_AAGGA(T20, T21, T17, T16, T7, appendD_out_aag(T20, T21, T17)) → APPENDE_IN_GGGA(T21, T16, T20, T7)
APPENDE_IN_GGGA(.(T64, T65), T66, T67, .(T64, T69)) → U4_GGGA(T64, T65, T66, T67, T69, appendE_in_ggga(T65, T66, T67, T69))
APPENDE_IN_GGGA(.(T64, T65), T66, T67, .(T64, T69)) → APPENDE_IN_GGGA(T65, T66, T67, T69)
ROTATEA_IN_GA(T86, T7) → U2_GA(T86, T7, appendC_in_ga(T86, T7))
ROTATEA_IN_GA(T86, T7) → APPENDC_IN_GA(T86, T7)
APPENDC_IN_GA(.(T102, T103), .(T102, T105)) → U5_GA(T102, T103, T105, appendC_in_ga(T103, T105))
APPENDC_IN_GA(.(T102, T103), .(T102, T105)) → APPENDC_IN_GA(T103, T105)
rotateA_in_ga(.(T16, T17), T7) → U1_ga(T16, T17, T7, pB_in_aagga(X40, X41, T17, T16, T7))
pB_in_aagga(T20, T21, T17, T16, T7) → U6_aagga(T20, T21, T17, T16, T7, appendD_in_aag(T20, T21, T17))
appendD_in_aag(.(T32, X89), X90, .(T32, T33)) → U3_aag(T32, X89, X90, T33, appendD_in_aag(X89, X90, T33))
appendD_in_aag([], T38, T38) → appendD_out_aag([], T38, T38)
U3_aag(T32, X89, X90, T33, appendD_out_aag(X89, X90, T33)) → appendD_out_aag(.(T32, X89), X90, .(T32, T33))
U6_aagga(T20, T21, T17, T16, T7, appendD_out_aag(T20, T21, T17)) → U7_aagga(T20, T21, T17, T16, T7, appendE_in_ggga(T21, T16, T20, T7))
appendE_in_ggga(.(T64, T65), T66, T67, .(T64, T69)) → U4_ggga(T64, T65, T66, T67, T69, appendE_in_ggga(T65, T66, T67, T69))
appendE_in_ggga([], T79, T80, .(T79, T80)) → appendE_out_ggga([], T79, T80, .(T79, T80))
U4_ggga(T64, T65, T66, T67, T69, appendE_out_ggga(T65, T66, T67, T69)) → appendE_out_ggga(.(T64, T65), T66, T67, .(T64, T69))
U7_aagga(T20, T21, T17, T16, T7, appendE_out_ggga(T21, T16, T20, T7)) → pB_out_aagga(T20, T21, T17, T16, T7)
U1_ga(T16, T17, T7, pB_out_aagga(X40, X41, T17, T16, T7)) → rotateA_out_ga(.(T16, T17), T7)
rotateA_in_ga(T86, T7) → U2_ga(T86, T7, appendC_in_ga(T86, T7))
appendC_in_ga(.(T102, T103), .(T102, T105)) → U5_ga(T102, T103, T105, appendC_in_ga(T103, T105))
appendC_in_ga([], []) → appendC_out_ga([], [])
U5_ga(T102, T103, T105, appendC_out_ga(T103, T105)) → appendC_out_ga(.(T102, T103), .(T102, T105))
U2_ga(T86, T7, appendC_out_ga(T86, T7)) → rotateA_out_ga(T86, T7)
ROTATEA_IN_GA(.(T16, T17), T7) → U1_GA(T16, T17, T7, pB_in_aagga(X40, X41, T17, T16, T7))
ROTATEA_IN_GA(.(T16, T17), T7) → PB_IN_AAGGA(X40, X41, T17, T16, T7)
PB_IN_AAGGA(T20, T21, T17, T16, T7) → U6_AAGGA(T20, T21, T17, T16, T7, appendD_in_aag(T20, T21, T17))
PB_IN_AAGGA(T20, T21, T17, T16, T7) → APPENDD_IN_AAG(T20, T21, T17)
APPENDD_IN_AAG(.(T32, X89), X90, .(T32, T33)) → U3_AAG(T32, X89, X90, T33, appendD_in_aag(X89, X90, T33))
APPENDD_IN_AAG(.(T32, X89), X90, .(T32, T33)) → APPENDD_IN_AAG(X89, X90, T33)
U6_AAGGA(T20, T21, T17, T16, T7, appendD_out_aag(T20, T21, T17)) → U7_AAGGA(T20, T21, T17, T16, T7, appendE_in_ggga(T21, T16, T20, T7))
U6_AAGGA(T20, T21, T17, T16, T7, appendD_out_aag(T20, T21, T17)) → APPENDE_IN_GGGA(T21, T16, T20, T7)
APPENDE_IN_GGGA(.(T64, T65), T66, T67, .(T64, T69)) → U4_GGGA(T64, T65, T66, T67, T69, appendE_in_ggga(T65, T66, T67, T69))
APPENDE_IN_GGGA(.(T64, T65), T66, T67, .(T64, T69)) → APPENDE_IN_GGGA(T65, T66, T67, T69)
ROTATEA_IN_GA(T86, T7) → U2_GA(T86, T7, appendC_in_ga(T86, T7))
ROTATEA_IN_GA(T86, T7) → APPENDC_IN_GA(T86, T7)
APPENDC_IN_GA(.(T102, T103), .(T102, T105)) → U5_GA(T102, T103, T105, appendC_in_ga(T103, T105))
APPENDC_IN_GA(.(T102, T103), .(T102, T105)) → APPENDC_IN_GA(T103, T105)
rotateA_in_ga(.(T16, T17), T7) → U1_ga(T16, T17, T7, pB_in_aagga(X40, X41, T17, T16, T7))
pB_in_aagga(T20, T21, T17, T16, T7) → U6_aagga(T20, T21, T17, T16, T7, appendD_in_aag(T20, T21, T17))
appendD_in_aag(.(T32, X89), X90, .(T32, T33)) → U3_aag(T32, X89, X90, T33, appendD_in_aag(X89, X90, T33))
appendD_in_aag([], T38, T38) → appendD_out_aag([], T38, T38)
U3_aag(T32, X89, X90, T33, appendD_out_aag(X89, X90, T33)) → appendD_out_aag(.(T32, X89), X90, .(T32, T33))
U6_aagga(T20, T21, T17, T16, T7, appendD_out_aag(T20, T21, T17)) → U7_aagga(T20, T21, T17, T16, T7, appendE_in_ggga(T21, T16, T20, T7))
appendE_in_ggga(.(T64, T65), T66, T67, .(T64, T69)) → U4_ggga(T64, T65, T66, T67, T69, appendE_in_ggga(T65, T66, T67, T69))
appendE_in_ggga([], T79, T80, .(T79, T80)) → appendE_out_ggga([], T79, T80, .(T79, T80))
U4_ggga(T64, T65, T66, T67, T69, appendE_out_ggga(T65, T66, T67, T69)) → appendE_out_ggga(.(T64, T65), T66, T67, .(T64, T69))
U7_aagga(T20, T21, T17, T16, T7, appendE_out_ggga(T21, T16, T20, T7)) → pB_out_aagga(T20, T21, T17, T16, T7)
U1_ga(T16, T17, T7, pB_out_aagga(X40, X41, T17, T16, T7)) → rotateA_out_ga(.(T16, T17), T7)
rotateA_in_ga(T86, T7) → U2_ga(T86, T7, appendC_in_ga(T86, T7))
appendC_in_ga(.(T102, T103), .(T102, T105)) → U5_ga(T102, T103, T105, appendC_in_ga(T103, T105))
appendC_in_ga([], []) → appendC_out_ga([], [])
U5_ga(T102, T103, T105, appendC_out_ga(T103, T105)) → appendC_out_ga(.(T102, T103), .(T102, T105))
U2_ga(T86, T7, appendC_out_ga(T86, T7)) → rotateA_out_ga(T86, T7)
APPENDC_IN_GA(.(T102, T103), .(T102, T105)) → APPENDC_IN_GA(T103, T105)
rotateA_in_ga(.(T16, T17), T7) → U1_ga(T16, T17, T7, pB_in_aagga(X40, X41, T17, T16, T7))
pB_in_aagga(T20, T21, T17, T16, T7) → U6_aagga(T20, T21, T17, T16, T7, appendD_in_aag(T20, T21, T17))
appendD_in_aag(.(T32, X89), X90, .(T32, T33)) → U3_aag(T32, X89, X90, T33, appendD_in_aag(X89, X90, T33))
appendD_in_aag([], T38, T38) → appendD_out_aag([], T38, T38)
U3_aag(T32, X89, X90, T33, appendD_out_aag(X89, X90, T33)) → appendD_out_aag(.(T32, X89), X90, .(T32, T33))
U6_aagga(T20, T21, T17, T16, T7, appendD_out_aag(T20, T21, T17)) → U7_aagga(T20, T21, T17, T16, T7, appendE_in_ggga(T21, T16, T20, T7))
appendE_in_ggga(.(T64, T65), T66, T67, .(T64, T69)) → U4_ggga(T64, T65, T66, T67, T69, appendE_in_ggga(T65, T66, T67, T69))
appendE_in_ggga([], T79, T80, .(T79, T80)) → appendE_out_ggga([], T79, T80, .(T79, T80))
U4_ggga(T64, T65, T66, T67, T69, appendE_out_ggga(T65, T66, T67, T69)) → appendE_out_ggga(.(T64, T65), T66, T67, .(T64, T69))
U7_aagga(T20, T21, T17, T16, T7, appendE_out_ggga(T21, T16, T20, T7)) → pB_out_aagga(T20, T21, T17, T16, T7)
U1_ga(T16, T17, T7, pB_out_aagga(X40, X41, T17, T16, T7)) → rotateA_out_ga(.(T16, T17), T7)
rotateA_in_ga(T86, T7) → U2_ga(T86, T7, appendC_in_ga(T86, T7))
appendC_in_ga(.(T102, T103), .(T102, T105)) → U5_ga(T102, T103, T105, appendC_in_ga(T103, T105))
appendC_in_ga([], []) → appendC_out_ga([], [])
U5_ga(T102, T103, T105, appendC_out_ga(T103, T105)) → appendC_out_ga(.(T102, T103), .(T102, T105))
U2_ga(T86, T7, appendC_out_ga(T86, T7)) → rotateA_out_ga(T86, T7)
APPENDC_IN_GA(.(T102, T103), .(T102, T105)) → APPENDC_IN_GA(T103, T105)
APPENDC_IN_GA(.(T102, T103)) → APPENDC_IN_GA(T103)
From the DPs we obtained the following set of size-change graphs:
APPENDE_IN_GGGA(.(T64, T65), T66, T67, .(T64, T69)) → APPENDE_IN_GGGA(T65, T66, T67, T69)
rotateA_in_ga(.(T16, T17), T7) → U1_ga(T16, T17, T7, pB_in_aagga(X40, X41, T17, T16, T7))
pB_in_aagga(T20, T21, T17, T16, T7) → U6_aagga(T20, T21, T17, T16, T7, appendD_in_aag(T20, T21, T17))
appendD_in_aag(.(T32, X89), X90, .(T32, T33)) → U3_aag(T32, X89, X90, T33, appendD_in_aag(X89, X90, T33))
appendD_in_aag([], T38, T38) → appendD_out_aag([], T38, T38)
U3_aag(T32, X89, X90, T33, appendD_out_aag(X89, X90, T33)) → appendD_out_aag(.(T32, X89), X90, .(T32, T33))
U6_aagga(T20, T21, T17, T16, T7, appendD_out_aag(T20, T21, T17)) → U7_aagga(T20, T21, T17, T16, T7, appendE_in_ggga(T21, T16, T20, T7))
appendE_in_ggga(.(T64, T65), T66, T67, .(T64, T69)) → U4_ggga(T64, T65, T66, T67, T69, appendE_in_ggga(T65, T66, T67, T69))
appendE_in_ggga([], T79, T80, .(T79, T80)) → appendE_out_ggga([], T79, T80, .(T79, T80))
U4_ggga(T64, T65, T66, T67, T69, appendE_out_ggga(T65, T66, T67, T69)) → appendE_out_ggga(.(T64, T65), T66, T67, .(T64, T69))
U7_aagga(T20, T21, T17, T16, T7, appendE_out_ggga(T21, T16, T20, T7)) → pB_out_aagga(T20, T21, T17, T16, T7)
U1_ga(T16, T17, T7, pB_out_aagga(X40, X41, T17, T16, T7)) → rotateA_out_ga(.(T16, T17), T7)
rotateA_in_ga(T86, T7) → U2_ga(T86, T7, appendC_in_ga(T86, T7))
appendC_in_ga(.(T102, T103), .(T102, T105)) → U5_ga(T102, T103, T105, appendC_in_ga(T103, T105))
appendC_in_ga([], []) → appendC_out_ga([], [])
U5_ga(T102, T103, T105, appendC_out_ga(T103, T105)) → appendC_out_ga(.(T102, T103), .(T102, T105))
U2_ga(T86, T7, appendC_out_ga(T86, T7)) → rotateA_out_ga(T86, T7)
APPENDE_IN_GGGA(.(T64, T65), T66, T67, .(T64, T69)) → APPENDE_IN_GGGA(T65, T66, T67, T69)
APPENDE_IN_GGGA(.(T64, T65), T66, T67) → APPENDE_IN_GGGA(T65, T66, T67)
From the DPs we obtained the following set of size-change graphs:
APPENDD_IN_AAG(.(T32, X89), X90, .(T32, T33)) → APPENDD_IN_AAG(X89, X90, T33)
rotateA_in_ga(.(T16, T17), T7) → U1_ga(T16, T17, T7, pB_in_aagga(X40, X41, T17, T16, T7))
pB_in_aagga(T20, T21, T17, T16, T7) → U6_aagga(T20, T21, T17, T16, T7, appendD_in_aag(T20, T21, T17))
appendD_in_aag(.(T32, X89), X90, .(T32, T33)) → U3_aag(T32, X89, X90, T33, appendD_in_aag(X89, X90, T33))
appendD_in_aag([], T38, T38) → appendD_out_aag([], T38, T38)
U3_aag(T32, X89, X90, T33, appendD_out_aag(X89, X90, T33)) → appendD_out_aag(.(T32, X89), X90, .(T32, T33))
U6_aagga(T20, T21, T17, T16, T7, appendD_out_aag(T20, T21, T17)) → U7_aagga(T20, T21, T17, T16, T7, appendE_in_ggga(T21, T16, T20, T7))
appendE_in_ggga(.(T64, T65), T66, T67, .(T64, T69)) → U4_ggga(T64, T65, T66, T67, T69, appendE_in_ggga(T65, T66, T67, T69))
appendE_in_ggga([], T79, T80, .(T79, T80)) → appendE_out_ggga([], T79, T80, .(T79, T80))
U4_ggga(T64, T65, T66, T67, T69, appendE_out_ggga(T65, T66, T67, T69)) → appendE_out_ggga(.(T64, T65), T66, T67, .(T64, T69))
U7_aagga(T20, T21, T17, T16, T7, appendE_out_ggga(T21, T16, T20, T7)) → pB_out_aagga(T20, T21, T17, T16, T7)
U1_ga(T16, T17, T7, pB_out_aagga(X40, X41, T17, T16, T7)) → rotateA_out_ga(.(T16, T17), T7)
rotateA_in_ga(T86, T7) → U2_ga(T86, T7, appendC_in_ga(T86, T7))
appendC_in_ga(.(T102, T103), .(T102, T105)) → U5_ga(T102, T103, T105, appendC_in_ga(T103, T105))
appendC_in_ga([], []) → appendC_out_ga([], [])
U5_ga(T102, T103, T105, appendC_out_ga(T103, T105)) → appendC_out_ga(.(T102, T103), .(T102, T105))
U2_ga(T86, T7, appendC_out_ga(T86, T7)) → rotateA_out_ga(T86, T7)
APPENDD_IN_AAG(.(T32, X89), X90, .(T32, T33)) → APPENDD_IN_AAG(X89, X90, T33)
APPENDD_IN_AAG(.(T32, T33)) → APPENDD_IN_AAG(T33)
From the DPs we obtained the following set of size-change graphs: