0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 292 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 9 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 8 ms)
↳6 PiDP
↳7 UsableRulesProof (⇔, 0 ms)
↳8 PiDP
↳9 PiDPToQDPProof (⇒, 0 ms)
↳10 QDP
↳11 QDPSizeChangeProof (⇔, 3 ms)
↳12 YES
reverseA_in_ga([], []) → reverseA_out_ga([], [])
reverseA_in_ga(.(T36, []), .(T36, [])) → reverseA_out_ga(.(T36, []), .(T36, []))
reverseA_in_ga(.(T70, .(T69, [])), .(T69, .(T70, []))) → reverseA_out_ga(.(T70, .(T69, [])), .(T69, .(T70, [])))
reverseA_in_ga(.(T114, .(T113, .(T112, []))), .(T112, .(T113, .(T114, [])))) → reverseA_out_ga(.(T114, .(T113, .(T112, []))), .(T112, .(T113, .(T114, []))))
reverseA_in_ga(.(T168, .(T167, .(T166, .(T165, [])))), .(T165, .(T166, .(T167, .(T168, []))))) → reverseA_out_ga(.(T168, .(T167, .(T166, .(T165, [])))), .(T165, .(T166, .(T167, .(T168, [])))))
reverseA_in_ga(.(T232, .(T231, .(T230, .(T229, .(T228, []))))), .(T228, .(T229, .(T230, .(T231, .(T232, [])))))) → reverseA_out_ga(.(T232, .(T231, .(T230, .(T229, .(T228, []))))), .(T228, .(T229, .(T230, .(T231, .(T232, []))))))
reverseA_in_ga(.(T306, .(T305, .(T304, .(T303, .(T302, .(T301, [])))))), .(T301, .(T302, .(T303, .(T304, .(T305, .(T306, []))))))) → reverseA_out_ga(.(T306, .(T305, .(T304, .(T303, .(T302, .(T301, [])))))), .(T301, .(T302, .(T303, .(T304, .(T305, .(T306, [])))))))
reverseA_in_ga(.(T390, .(T389, .(T388, .(T387, .(T386, .(T385, .(T384, []))))))), .(T384, .(T385, .(T386, .(T387, .(T388, .(T389, .(T390, [])))))))) → reverseA_out_ga(.(T390, .(T389, .(T388, .(T387, .(T386, .(T385, .(T384, []))))))), .(T384, .(T385, .(T386, .(T387, .(T388, .(T389, .(T390, []))))))))
reverseA_in_ga(.(T420, .(T419, .(T418, .(T417, .(T416, .(T415, .(T414, .(T411, T412)))))))), T421) → U1_ga(T420, T419, T418, T417, T416, T415, T414, T411, T412, T421, revaccB_in_gagg(T412, T421, T411, .(T414, .(T415, .(T416, .(T417, .(T418, .(T419, .(T420, [])))))))))
revaccB_in_gagg([], .(T460, T461), T460, T461) → revaccB_out_gagg([], .(T460, T461), T460, T461)
revaccB_in_gagg(.(T472, T473), T477, T475, T476) → U2_gagg(T472, T473, T477, T475, T476, revaccB_in_gagg(T473, T477, T472, .(T475, T476)))
U2_gagg(T472, T473, T477, T475, T476, revaccB_out_gagg(T473, T477, T472, .(T475, T476))) → revaccB_out_gagg(.(T472, T473), T477, T475, T476)
U1_ga(T420, T419, T418, T417, T416, T415, T414, T411, T412, T421, revaccB_out_gagg(T412, T421, T411, .(T414, .(T415, .(T416, .(T417, .(T418, .(T419, .(T420, []))))))))) → reverseA_out_ga(.(T420, .(T419, .(T418, .(T417, .(T416, .(T415, .(T414, .(T411, T412)))))))), T421)
REVERSEA_IN_GA(.(T420, .(T419, .(T418, .(T417, .(T416, .(T415, .(T414, .(T411, T412)))))))), T421) → U1_GA(T420, T419, T418, T417, T416, T415, T414, T411, T412, T421, revaccB_in_gagg(T412, T421, T411, .(T414, .(T415, .(T416, .(T417, .(T418, .(T419, .(T420, [])))))))))
REVERSEA_IN_GA(.(T420, .(T419, .(T418, .(T417, .(T416, .(T415, .(T414, .(T411, T412)))))))), T421) → REVACCB_IN_GAGG(T412, T421, T411, .(T414, .(T415, .(T416, .(T417, .(T418, .(T419, .(T420, []))))))))
REVACCB_IN_GAGG(.(T472, T473), T477, T475, T476) → U2_GAGG(T472, T473, T477, T475, T476, revaccB_in_gagg(T473, T477, T472, .(T475, T476)))
REVACCB_IN_GAGG(.(T472, T473), T477, T475, T476) → REVACCB_IN_GAGG(T473, T477, T472, .(T475, T476))
reverseA_in_ga([], []) → reverseA_out_ga([], [])
reverseA_in_ga(.(T36, []), .(T36, [])) → reverseA_out_ga(.(T36, []), .(T36, []))
reverseA_in_ga(.(T70, .(T69, [])), .(T69, .(T70, []))) → reverseA_out_ga(.(T70, .(T69, [])), .(T69, .(T70, [])))
reverseA_in_ga(.(T114, .(T113, .(T112, []))), .(T112, .(T113, .(T114, [])))) → reverseA_out_ga(.(T114, .(T113, .(T112, []))), .(T112, .(T113, .(T114, []))))
reverseA_in_ga(.(T168, .(T167, .(T166, .(T165, [])))), .(T165, .(T166, .(T167, .(T168, []))))) → reverseA_out_ga(.(T168, .(T167, .(T166, .(T165, [])))), .(T165, .(T166, .(T167, .(T168, [])))))
reverseA_in_ga(.(T232, .(T231, .(T230, .(T229, .(T228, []))))), .(T228, .(T229, .(T230, .(T231, .(T232, [])))))) → reverseA_out_ga(.(T232, .(T231, .(T230, .(T229, .(T228, []))))), .(T228, .(T229, .(T230, .(T231, .(T232, []))))))
reverseA_in_ga(.(T306, .(T305, .(T304, .(T303, .(T302, .(T301, [])))))), .(T301, .(T302, .(T303, .(T304, .(T305, .(T306, []))))))) → reverseA_out_ga(.(T306, .(T305, .(T304, .(T303, .(T302, .(T301, [])))))), .(T301, .(T302, .(T303, .(T304, .(T305, .(T306, [])))))))
reverseA_in_ga(.(T390, .(T389, .(T388, .(T387, .(T386, .(T385, .(T384, []))))))), .(T384, .(T385, .(T386, .(T387, .(T388, .(T389, .(T390, [])))))))) → reverseA_out_ga(.(T390, .(T389, .(T388, .(T387, .(T386, .(T385, .(T384, []))))))), .(T384, .(T385, .(T386, .(T387, .(T388, .(T389, .(T390, []))))))))
reverseA_in_ga(.(T420, .(T419, .(T418, .(T417, .(T416, .(T415, .(T414, .(T411, T412)))))))), T421) → U1_ga(T420, T419, T418, T417, T416, T415, T414, T411, T412, T421, revaccB_in_gagg(T412, T421, T411, .(T414, .(T415, .(T416, .(T417, .(T418, .(T419, .(T420, [])))))))))
revaccB_in_gagg([], .(T460, T461), T460, T461) → revaccB_out_gagg([], .(T460, T461), T460, T461)
revaccB_in_gagg(.(T472, T473), T477, T475, T476) → U2_gagg(T472, T473, T477, T475, T476, revaccB_in_gagg(T473, T477, T472, .(T475, T476)))
U2_gagg(T472, T473, T477, T475, T476, revaccB_out_gagg(T473, T477, T472, .(T475, T476))) → revaccB_out_gagg(.(T472, T473), T477, T475, T476)
U1_ga(T420, T419, T418, T417, T416, T415, T414, T411, T412, T421, revaccB_out_gagg(T412, T421, T411, .(T414, .(T415, .(T416, .(T417, .(T418, .(T419, .(T420, []))))))))) → reverseA_out_ga(.(T420, .(T419, .(T418, .(T417, .(T416, .(T415, .(T414, .(T411, T412)))))))), T421)
REVERSEA_IN_GA(.(T420, .(T419, .(T418, .(T417, .(T416, .(T415, .(T414, .(T411, T412)))))))), T421) → U1_GA(T420, T419, T418, T417, T416, T415, T414, T411, T412, T421, revaccB_in_gagg(T412, T421, T411, .(T414, .(T415, .(T416, .(T417, .(T418, .(T419, .(T420, [])))))))))
REVERSEA_IN_GA(.(T420, .(T419, .(T418, .(T417, .(T416, .(T415, .(T414, .(T411, T412)))))))), T421) → REVACCB_IN_GAGG(T412, T421, T411, .(T414, .(T415, .(T416, .(T417, .(T418, .(T419, .(T420, []))))))))
REVACCB_IN_GAGG(.(T472, T473), T477, T475, T476) → U2_GAGG(T472, T473, T477, T475, T476, revaccB_in_gagg(T473, T477, T472, .(T475, T476)))
REVACCB_IN_GAGG(.(T472, T473), T477, T475, T476) → REVACCB_IN_GAGG(T473, T477, T472, .(T475, T476))
reverseA_in_ga([], []) → reverseA_out_ga([], [])
reverseA_in_ga(.(T36, []), .(T36, [])) → reverseA_out_ga(.(T36, []), .(T36, []))
reverseA_in_ga(.(T70, .(T69, [])), .(T69, .(T70, []))) → reverseA_out_ga(.(T70, .(T69, [])), .(T69, .(T70, [])))
reverseA_in_ga(.(T114, .(T113, .(T112, []))), .(T112, .(T113, .(T114, [])))) → reverseA_out_ga(.(T114, .(T113, .(T112, []))), .(T112, .(T113, .(T114, []))))
reverseA_in_ga(.(T168, .(T167, .(T166, .(T165, [])))), .(T165, .(T166, .(T167, .(T168, []))))) → reverseA_out_ga(.(T168, .(T167, .(T166, .(T165, [])))), .(T165, .(T166, .(T167, .(T168, [])))))
reverseA_in_ga(.(T232, .(T231, .(T230, .(T229, .(T228, []))))), .(T228, .(T229, .(T230, .(T231, .(T232, [])))))) → reverseA_out_ga(.(T232, .(T231, .(T230, .(T229, .(T228, []))))), .(T228, .(T229, .(T230, .(T231, .(T232, []))))))
reverseA_in_ga(.(T306, .(T305, .(T304, .(T303, .(T302, .(T301, [])))))), .(T301, .(T302, .(T303, .(T304, .(T305, .(T306, []))))))) → reverseA_out_ga(.(T306, .(T305, .(T304, .(T303, .(T302, .(T301, [])))))), .(T301, .(T302, .(T303, .(T304, .(T305, .(T306, [])))))))
reverseA_in_ga(.(T390, .(T389, .(T388, .(T387, .(T386, .(T385, .(T384, []))))))), .(T384, .(T385, .(T386, .(T387, .(T388, .(T389, .(T390, [])))))))) → reverseA_out_ga(.(T390, .(T389, .(T388, .(T387, .(T386, .(T385, .(T384, []))))))), .(T384, .(T385, .(T386, .(T387, .(T388, .(T389, .(T390, []))))))))
reverseA_in_ga(.(T420, .(T419, .(T418, .(T417, .(T416, .(T415, .(T414, .(T411, T412)))))))), T421) → U1_ga(T420, T419, T418, T417, T416, T415, T414, T411, T412, T421, revaccB_in_gagg(T412, T421, T411, .(T414, .(T415, .(T416, .(T417, .(T418, .(T419, .(T420, [])))))))))
revaccB_in_gagg([], .(T460, T461), T460, T461) → revaccB_out_gagg([], .(T460, T461), T460, T461)
revaccB_in_gagg(.(T472, T473), T477, T475, T476) → U2_gagg(T472, T473, T477, T475, T476, revaccB_in_gagg(T473, T477, T472, .(T475, T476)))
U2_gagg(T472, T473, T477, T475, T476, revaccB_out_gagg(T473, T477, T472, .(T475, T476))) → revaccB_out_gagg(.(T472, T473), T477, T475, T476)
U1_ga(T420, T419, T418, T417, T416, T415, T414, T411, T412, T421, revaccB_out_gagg(T412, T421, T411, .(T414, .(T415, .(T416, .(T417, .(T418, .(T419, .(T420, []))))))))) → reverseA_out_ga(.(T420, .(T419, .(T418, .(T417, .(T416, .(T415, .(T414, .(T411, T412)))))))), T421)
REVACCB_IN_GAGG(.(T472, T473), T477, T475, T476) → REVACCB_IN_GAGG(T473, T477, T472, .(T475, T476))
reverseA_in_ga([], []) → reverseA_out_ga([], [])
reverseA_in_ga(.(T36, []), .(T36, [])) → reverseA_out_ga(.(T36, []), .(T36, []))
reverseA_in_ga(.(T70, .(T69, [])), .(T69, .(T70, []))) → reverseA_out_ga(.(T70, .(T69, [])), .(T69, .(T70, [])))
reverseA_in_ga(.(T114, .(T113, .(T112, []))), .(T112, .(T113, .(T114, [])))) → reverseA_out_ga(.(T114, .(T113, .(T112, []))), .(T112, .(T113, .(T114, []))))
reverseA_in_ga(.(T168, .(T167, .(T166, .(T165, [])))), .(T165, .(T166, .(T167, .(T168, []))))) → reverseA_out_ga(.(T168, .(T167, .(T166, .(T165, [])))), .(T165, .(T166, .(T167, .(T168, [])))))
reverseA_in_ga(.(T232, .(T231, .(T230, .(T229, .(T228, []))))), .(T228, .(T229, .(T230, .(T231, .(T232, [])))))) → reverseA_out_ga(.(T232, .(T231, .(T230, .(T229, .(T228, []))))), .(T228, .(T229, .(T230, .(T231, .(T232, []))))))
reverseA_in_ga(.(T306, .(T305, .(T304, .(T303, .(T302, .(T301, [])))))), .(T301, .(T302, .(T303, .(T304, .(T305, .(T306, []))))))) → reverseA_out_ga(.(T306, .(T305, .(T304, .(T303, .(T302, .(T301, [])))))), .(T301, .(T302, .(T303, .(T304, .(T305, .(T306, [])))))))
reverseA_in_ga(.(T390, .(T389, .(T388, .(T387, .(T386, .(T385, .(T384, []))))))), .(T384, .(T385, .(T386, .(T387, .(T388, .(T389, .(T390, [])))))))) → reverseA_out_ga(.(T390, .(T389, .(T388, .(T387, .(T386, .(T385, .(T384, []))))))), .(T384, .(T385, .(T386, .(T387, .(T388, .(T389, .(T390, []))))))))
reverseA_in_ga(.(T420, .(T419, .(T418, .(T417, .(T416, .(T415, .(T414, .(T411, T412)))))))), T421) → U1_ga(T420, T419, T418, T417, T416, T415, T414, T411, T412, T421, revaccB_in_gagg(T412, T421, T411, .(T414, .(T415, .(T416, .(T417, .(T418, .(T419, .(T420, [])))))))))
revaccB_in_gagg([], .(T460, T461), T460, T461) → revaccB_out_gagg([], .(T460, T461), T460, T461)
revaccB_in_gagg(.(T472, T473), T477, T475, T476) → U2_gagg(T472, T473, T477, T475, T476, revaccB_in_gagg(T473, T477, T472, .(T475, T476)))
U2_gagg(T472, T473, T477, T475, T476, revaccB_out_gagg(T473, T477, T472, .(T475, T476))) → revaccB_out_gagg(.(T472, T473), T477, T475, T476)
U1_ga(T420, T419, T418, T417, T416, T415, T414, T411, T412, T421, revaccB_out_gagg(T412, T421, T411, .(T414, .(T415, .(T416, .(T417, .(T418, .(T419, .(T420, []))))))))) → reverseA_out_ga(.(T420, .(T419, .(T418, .(T417, .(T416, .(T415, .(T414, .(T411, T412)))))))), T421)
REVACCB_IN_GAGG(.(T472, T473), T477, T475, T476) → REVACCB_IN_GAGG(T473, T477, T472, .(T475, T476))
REVACCB_IN_GAGG(.(T472, T473), T475, T476) → REVACCB_IN_GAGG(T473, T472, .(T475, T476))
From the DPs we obtained the following set of size-change graphs: