0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 135 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 21 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 9 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
↳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, append2D_in_aag(T20, T21, T17))
append2D_in_aag(.(T32, X89), X90, .(T32, T33)) → U3_aag(T32, X89, X90, T33, append2D_in_aag(X89, X90, T33))
append2D_in_aag([], T38, T38) → append2D_out_aag([], T38, T38)
U3_aag(T32, X89, X90, T33, append2D_out_aag(X89, X90, T33)) → append2D_out_aag(.(T32, X89), X90, .(T32, T33))
U6_aagga(T20, T21, T17, T16, T7, append2D_out_aag(T20, T21, T17)) → U7_aagga(T20, T21, T17, T16, T7, append1E_in_ggga(T21, T16, T20, T7))
append1E_in_ggga(.(T64, T65), T66, T67, .(T64, T69)) → U4_ggga(T64, T65, T66, T67, T69, append1E_in_ggga(T65, T66, T67, T69))
append1E_in_ggga([], T79, T80, .(T79, T80)) → append1E_out_ggga([], T79, T80, .(T79, T80))
U4_ggga(T64, T65, T66, T67, T69, append1E_out_ggga(T65, T66, T67, T69)) → append1E_out_ggga(.(T64, T65), T66, T67, .(T64, T69))
U7_aagga(T20, T21, T17, T16, T7, append1E_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, append1C_in_ga(T86, T7))
append1C_in_ga(.(T102, T103), .(T102, T105)) → U5_ga(T102, T103, T105, append1C_in_ga(T103, T105))
append1C_in_ga([], []) → append1C_out_ga([], [])
U5_ga(T102, T103, T105, append1C_out_ga(T103, T105)) → append1C_out_ga(.(T102, T103), .(T102, T105))
U2_ga(T86, T7, append1C_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, append2D_in_aag(T20, T21, T17))
PB_IN_AAGGA(T20, T21, T17, T16, T7) → APPEND2D_IN_AAG(T20, T21, T17)
APPEND2D_IN_AAG(.(T32, X89), X90, .(T32, T33)) → U3_AAG(T32, X89, X90, T33, append2D_in_aag(X89, X90, T33))
APPEND2D_IN_AAG(.(T32, X89), X90, .(T32, T33)) → APPEND2D_IN_AAG(X89, X90, T33)
U6_AAGGA(T20, T21, T17, T16, T7, append2D_out_aag(T20, T21, T17)) → U7_AAGGA(T20, T21, T17, T16, T7, append1E_in_ggga(T21, T16, T20, T7))
U6_AAGGA(T20, T21, T17, T16, T7, append2D_out_aag(T20, T21, T17)) → APPEND1E_IN_GGGA(T21, T16, T20, T7)
APPEND1E_IN_GGGA(.(T64, T65), T66, T67, .(T64, T69)) → U4_GGGA(T64, T65, T66, T67, T69, append1E_in_ggga(T65, T66, T67, T69))
APPEND1E_IN_GGGA(.(T64, T65), T66, T67, .(T64, T69)) → APPEND1E_IN_GGGA(T65, T66, T67, T69)
ROTATEA_IN_GA(T86, T7) → U2_GA(T86, T7, append1C_in_ga(T86, T7))
ROTATEA_IN_GA(T86, T7) → APPEND1C_IN_GA(T86, T7)
APPEND1C_IN_GA(.(T102, T103), .(T102, T105)) → U5_GA(T102, T103, T105, append1C_in_ga(T103, T105))
APPEND1C_IN_GA(.(T102, T103), .(T102, T105)) → APPEND1C_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, append2D_in_aag(T20, T21, T17))
append2D_in_aag(.(T32, X89), X90, .(T32, T33)) → U3_aag(T32, X89, X90, T33, append2D_in_aag(X89, X90, T33))
append2D_in_aag([], T38, T38) → append2D_out_aag([], T38, T38)
U3_aag(T32, X89, X90, T33, append2D_out_aag(X89, X90, T33)) → append2D_out_aag(.(T32, X89), X90, .(T32, T33))
U6_aagga(T20, T21, T17, T16, T7, append2D_out_aag(T20, T21, T17)) → U7_aagga(T20, T21, T17, T16, T7, append1E_in_ggga(T21, T16, T20, T7))
append1E_in_ggga(.(T64, T65), T66, T67, .(T64, T69)) → U4_ggga(T64, T65, T66, T67, T69, append1E_in_ggga(T65, T66, T67, T69))
append1E_in_ggga([], T79, T80, .(T79, T80)) → append1E_out_ggga([], T79, T80, .(T79, T80))
U4_ggga(T64, T65, T66, T67, T69, append1E_out_ggga(T65, T66, T67, T69)) → append1E_out_ggga(.(T64, T65), T66, T67, .(T64, T69))
U7_aagga(T20, T21, T17, T16, T7, append1E_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, append1C_in_ga(T86, T7))
append1C_in_ga(.(T102, T103), .(T102, T105)) → U5_ga(T102, T103, T105, append1C_in_ga(T103, T105))
append1C_in_ga([], []) → append1C_out_ga([], [])
U5_ga(T102, T103, T105, append1C_out_ga(T103, T105)) → append1C_out_ga(.(T102, T103), .(T102, T105))
U2_ga(T86, T7, append1C_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, append2D_in_aag(T20, T21, T17))
PB_IN_AAGGA(T20, T21, T17, T16, T7) → APPEND2D_IN_AAG(T20, T21, T17)
APPEND2D_IN_AAG(.(T32, X89), X90, .(T32, T33)) → U3_AAG(T32, X89, X90, T33, append2D_in_aag(X89, X90, T33))
APPEND2D_IN_AAG(.(T32, X89), X90, .(T32, T33)) → APPEND2D_IN_AAG(X89, X90, T33)
U6_AAGGA(T20, T21, T17, T16, T7, append2D_out_aag(T20, T21, T17)) → U7_AAGGA(T20, T21, T17, T16, T7, append1E_in_ggga(T21, T16, T20, T7))
U6_AAGGA(T20, T21, T17, T16, T7, append2D_out_aag(T20, T21, T17)) → APPEND1E_IN_GGGA(T21, T16, T20, T7)
APPEND1E_IN_GGGA(.(T64, T65), T66, T67, .(T64, T69)) → U4_GGGA(T64, T65, T66, T67, T69, append1E_in_ggga(T65, T66, T67, T69))
APPEND1E_IN_GGGA(.(T64, T65), T66, T67, .(T64, T69)) → APPEND1E_IN_GGGA(T65, T66, T67, T69)
ROTATEA_IN_GA(T86, T7) → U2_GA(T86, T7, append1C_in_ga(T86, T7))
ROTATEA_IN_GA(T86, T7) → APPEND1C_IN_GA(T86, T7)
APPEND1C_IN_GA(.(T102, T103), .(T102, T105)) → U5_GA(T102, T103, T105, append1C_in_ga(T103, T105))
APPEND1C_IN_GA(.(T102, T103), .(T102, T105)) → APPEND1C_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, append2D_in_aag(T20, T21, T17))
append2D_in_aag(.(T32, X89), X90, .(T32, T33)) → U3_aag(T32, X89, X90, T33, append2D_in_aag(X89, X90, T33))
append2D_in_aag([], T38, T38) → append2D_out_aag([], T38, T38)
U3_aag(T32, X89, X90, T33, append2D_out_aag(X89, X90, T33)) → append2D_out_aag(.(T32, X89), X90, .(T32, T33))
U6_aagga(T20, T21, T17, T16, T7, append2D_out_aag(T20, T21, T17)) → U7_aagga(T20, T21, T17, T16, T7, append1E_in_ggga(T21, T16, T20, T7))
append1E_in_ggga(.(T64, T65), T66, T67, .(T64, T69)) → U4_ggga(T64, T65, T66, T67, T69, append1E_in_ggga(T65, T66, T67, T69))
append1E_in_ggga([], T79, T80, .(T79, T80)) → append1E_out_ggga([], T79, T80, .(T79, T80))
U4_ggga(T64, T65, T66, T67, T69, append1E_out_ggga(T65, T66, T67, T69)) → append1E_out_ggga(.(T64, T65), T66, T67, .(T64, T69))
U7_aagga(T20, T21, T17, T16, T7, append1E_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, append1C_in_ga(T86, T7))
append1C_in_ga(.(T102, T103), .(T102, T105)) → U5_ga(T102, T103, T105, append1C_in_ga(T103, T105))
append1C_in_ga([], []) → append1C_out_ga([], [])
U5_ga(T102, T103, T105, append1C_out_ga(T103, T105)) → append1C_out_ga(.(T102, T103), .(T102, T105))
U2_ga(T86, T7, append1C_out_ga(T86, T7)) → rotateA_out_ga(T86, T7)
APPEND1C_IN_GA(.(T102, T103), .(T102, T105)) → APPEND1C_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, append2D_in_aag(T20, T21, T17))
append2D_in_aag(.(T32, X89), X90, .(T32, T33)) → U3_aag(T32, X89, X90, T33, append2D_in_aag(X89, X90, T33))
append2D_in_aag([], T38, T38) → append2D_out_aag([], T38, T38)
U3_aag(T32, X89, X90, T33, append2D_out_aag(X89, X90, T33)) → append2D_out_aag(.(T32, X89), X90, .(T32, T33))
U6_aagga(T20, T21, T17, T16, T7, append2D_out_aag(T20, T21, T17)) → U7_aagga(T20, T21, T17, T16, T7, append1E_in_ggga(T21, T16, T20, T7))
append1E_in_ggga(.(T64, T65), T66, T67, .(T64, T69)) → U4_ggga(T64, T65, T66, T67, T69, append1E_in_ggga(T65, T66, T67, T69))
append1E_in_ggga([], T79, T80, .(T79, T80)) → append1E_out_ggga([], T79, T80, .(T79, T80))
U4_ggga(T64, T65, T66, T67, T69, append1E_out_ggga(T65, T66, T67, T69)) → append1E_out_ggga(.(T64, T65), T66, T67, .(T64, T69))
U7_aagga(T20, T21, T17, T16, T7, append1E_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, append1C_in_ga(T86, T7))
append1C_in_ga(.(T102, T103), .(T102, T105)) → U5_ga(T102, T103, T105, append1C_in_ga(T103, T105))
append1C_in_ga([], []) → append1C_out_ga([], [])
U5_ga(T102, T103, T105, append1C_out_ga(T103, T105)) → append1C_out_ga(.(T102, T103), .(T102, T105))
U2_ga(T86, T7, append1C_out_ga(T86, T7)) → rotateA_out_ga(T86, T7)
APPEND1C_IN_GA(.(T102, T103), .(T102, T105)) → APPEND1C_IN_GA(T103, T105)
APPEND1C_IN_GA(.(T102, T103)) → APPEND1C_IN_GA(T103)
From the DPs we obtained the following set of size-change graphs:
APPEND1E_IN_GGGA(.(T64, T65), T66, T67, .(T64, T69)) → APPEND1E_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, append2D_in_aag(T20, T21, T17))
append2D_in_aag(.(T32, X89), X90, .(T32, T33)) → U3_aag(T32, X89, X90, T33, append2D_in_aag(X89, X90, T33))
append2D_in_aag([], T38, T38) → append2D_out_aag([], T38, T38)
U3_aag(T32, X89, X90, T33, append2D_out_aag(X89, X90, T33)) → append2D_out_aag(.(T32, X89), X90, .(T32, T33))
U6_aagga(T20, T21, T17, T16, T7, append2D_out_aag(T20, T21, T17)) → U7_aagga(T20, T21, T17, T16, T7, append1E_in_ggga(T21, T16, T20, T7))
append1E_in_ggga(.(T64, T65), T66, T67, .(T64, T69)) → U4_ggga(T64, T65, T66, T67, T69, append1E_in_ggga(T65, T66, T67, T69))
append1E_in_ggga([], T79, T80, .(T79, T80)) → append1E_out_ggga([], T79, T80, .(T79, T80))
U4_ggga(T64, T65, T66, T67, T69, append1E_out_ggga(T65, T66, T67, T69)) → append1E_out_ggga(.(T64, T65), T66, T67, .(T64, T69))
U7_aagga(T20, T21, T17, T16, T7, append1E_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, append1C_in_ga(T86, T7))
append1C_in_ga(.(T102, T103), .(T102, T105)) → U5_ga(T102, T103, T105, append1C_in_ga(T103, T105))
append1C_in_ga([], []) → append1C_out_ga([], [])
U5_ga(T102, T103, T105, append1C_out_ga(T103, T105)) → append1C_out_ga(.(T102, T103), .(T102, T105))
U2_ga(T86, T7, append1C_out_ga(T86, T7)) → rotateA_out_ga(T86, T7)
APPEND1E_IN_GGGA(.(T64, T65), T66, T67, .(T64, T69)) → APPEND1E_IN_GGGA(T65, T66, T67, T69)
APPEND1E_IN_GGGA(.(T64, T65), T66, T67) → APPEND1E_IN_GGGA(T65, T66, T67)
From the DPs we obtained the following set of size-change graphs:
APPEND2D_IN_AAG(.(T32, X89), X90, .(T32, T33)) → APPEND2D_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, append2D_in_aag(T20, T21, T17))
append2D_in_aag(.(T32, X89), X90, .(T32, T33)) → U3_aag(T32, X89, X90, T33, append2D_in_aag(X89, X90, T33))
append2D_in_aag([], T38, T38) → append2D_out_aag([], T38, T38)
U3_aag(T32, X89, X90, T33, append2D_out_aag(X89, X90, T33)) → append2D_out_aag(.(T32, X89), X90, .(T32, T33))
U6_aagga(T20, T21, T17, T16, T7, append2D_out_aag(T20, T21, T17)) → U7_aagga(T20, T21, T17, T16, T7, append1E_in_ggga(T21, T16, T20, T7))
append1E_in_ggga(.(T64, T65), T66, T67, .(T64, T69)) → U4_ggga(T64, T65, T66, T67, T69, append1E_in_ggga(T65, T66, T67, T69))
append1E_in_ggga([], T79, T80, .(T79, T80)) → append1E_out_ggga([], T79, T80, .(T79, T80))
U4_ggga(T64, T65, T66, T67, T69, append1E_out_ggga(T65, T66, T67, T69)) → append1E_out_ggga(.(T64, T65), T66, T67, .(T64, T69))
U7_aagga(T20, T21, T17, T16, T7, append1E_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, append1C_in_ga(T86, T7))
append1C_in_ga(.(T102, T103), .(T102, T105)) → U5_ga(T102, T103, T105, append1C_in_ga(T103, T105))
append1C_in_ga([], []) → append1C_out_ga([], [])
U5_ga(T102, T103, T105, append1C_out_ga(T103, T105)) → append1C_out_ga(.(T102, T103), .(T102, T105))
U2_ga(T86, T7, append1C_out_ga(T86, T7)) → rotateA_out_ga(T86, T7)
APPEND2D_IN_AAG(.(T32, X89), X90, .(T32, T33)) → APPEND2D_IN_AAG(X89, X90, T33)
APPEND2D_IN_AAG(.(T32, T33)) → APPEND2D_IN_AAG(T33)
From the DPs we obtained the following set of size-change graphs: