0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 54 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 7 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 PiDP
↳7 UsableRulesProof (⇔, 0 ms)
↳8 PiDP
↳9 PiDPToQDPProof (⇒, 24 ms)
↳10 QDP
↳11 QDPSizeChangeProof (⇔, 0 ms)
↳12 YES
append3A_in_aag([], T5, T5) → append3A_out_aag([], T5, T5)
append3A_in_aag(.(T10, []), T20, .(T10, T20)) → append3A_out_aag(.(T10, []), T20, .(T10, T20))
append3A_in_aag(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32))) → U1_aag(T10, T29, T33, T34, T32, append3A_in_aag(T33, T34, T32))
append3A_in_aag(.(T41, .(T60, T64)), T65, .(T41, .(T60, T63))) → U2_aag(T41, T60, T64, T65, T63, append3A_in_aag(T64, T65, T63))
U2_aag(T41, T60, T64, T65, T63, append3A_out_aag(T64, T65, T63)) → append3A_out_aag(.(T41, .(T60, T64)), T65, .(T41, .(T60, T63)))
U1_aag(T10, T29, T33, T34, T32, append3A_out_aag(T33, T34, T32)) → append3A_out_aag(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32)))
APPEND3A_IN_AAG(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32))) → U1_AAG(T10, T29, T33, T34, T32, append3A_in_aag(T33, T34, T32))
APPEND3A_IN_AAG(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32))) → APPEND3A_IN_AAG(T33, T34, T32)
APPEND3A_IN_AAG(.(T41, .(T60, T64)), T65, .(T41, .(T60, T63))) → U2_AAG(T41, T60, T64, T65, T63, append3A_in_aag(T64, T65, T63))
append3A_in_aag([], T5, T5) → append3A_out_aag([], T5, T5)
append3A_in_aag(.(T10, []), T20, .(T10, T20)) → append3A_out_aag(.(T10, []), T20, .(T10, T20))
append3A_in_aag(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32))) → U1_aag(T10, T29, T33, T34, T32, append3A_in_aag(T33, T34, T32))
append3A_in_aag(.(T41, .(T60, T64)), T65, .(T41, .(T60, T63))) → U2_aag(T41, T60, T64, T65, T63, append3A_in_aag(T64, T65, T63))
U2_aag(T41, T60, T64, T65, T63, append3A_out_aag(T64, T65, T63)) → append3A_out_aag(.(T41, .(T60, T64)), T65, .(T41, .(T60, T63)))
U1_aag(T10, T29, T33, T34, T32, append3A_out_aag(T33, T34, T32)) → append3A_out_aag(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32)))
APPEND3A_IN_AAG(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32))) → U1_AAG(T10, T29, T33, T34, T32, append3A_in_aag(T33, T34, T32))
APPEND3A_IN_AAG(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32))) → APPEND3A_IN_AAG(T33, T34, T32)
APPEND3A_IN_AAG(.(T41, .(T60, T64)), T65, .(T41, .(T60, T63))) → U2_AAG(T41, T60, T64, T65, T63, append3A_in_aag(T64, T65, T63))
append3A_in_aag([], T5, T5) → append3A_out_aag([], T5, T5)
append3A_in_aag(.(T10, []), T20, .(T10, T20)) → append3A_out_aag(.(T10, []), T20, .(T10, T20))
append3A_in_aag(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32))) → U1_aag(T10, T29, T33, T34, T32, append3A_in_aag(T33, T34, T32))
append3A_in_aag(.(T41, .(T60, T64)), T65, .(T41, .(T60, T63))) → U2_aag(T41, T60, T64, T65, T63, append3A_in_aag(T64, T65, T63))
U2_aag(T41, T60, T64, T65, T63, append3A_out_aag(T64, T65, T63)) → append3A_out_aag(.(T41, .(T60, T64)), T65, .(T41, .(T60, T63)))
U1_aag(T10, T29, T33, T34, T32, append3A_out_aag(T33, T34, T32)) → append3A_out_aag(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32)))
APPEND3A_IN_AAG(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32))) → APPEND3A_IN_AAG(T33, T34, T32)
append3A_in_aag([], T5, T5) → append3A_out_aag([], T5, T5)
append3A_in_aag(.(T10, []), T20, .(T10, T20)) → append3A_out_aag(.(T10, []), T20, .(T10, T20))
append3A_in_aag(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32))) → U1_aag(T10, T29, T33, T34, T32, append3A_in_aag(T33, T34, T32))
append3A_in_aag(.(T41, .(T60, T64)), T65, .(T41, .(T60, T63))) → U2_aag(T41, T60, T64, T65, T63, append3A_in_aag(T64, T65, T63))
U2_aag(T41, T60, T64, T65, T63, append3A_out_aag(T64, T65, T63)) → append3A_out_aag(.(T41, .(T60, T64)), T65, .(T41, .(T60, T63)))
U1_aag(T10, T29, T33, T34, T32, append3A_out_aag(T33, T34, T32)) → append3A_out_aag(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32)))
APPEND3A_IN_AAG(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32))) → APPEND3A_IN_AAG(T33, T34, T32)
APPEND3A_IN_AAG(.(T10, .(T29, T32))) → APPEND3A_IN_AAG(T32)
From the DPs we obtained the following set of size-change graphs: