0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 280 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 5 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 PiDP
↳7 UsableRulesProof (⇔, 0 ms)
↳8 PiDP
↳9 PiDPToQDPProof (⇒, 16 ms)
↳10 QDP
↳11 QDPSizeChangeProof (⇔, 0 ms)
↳12 YES
revA_in_ga([], []) → revA_out_ga([], [])
revA_in_ga(.(T24, []), .(T24, [])) → revA_out_ga(.(T24, []), .(T24, []))
revA_in_ga(.(T51, .(T50, [])), .(T50, .(T51, []))) → revA_out_ga(.(T51, .(T50, [])), .(T50, .(T51, [])))
revA_in_ga(.(T88, .(T87, .(T86, []))), .(T86, .(T87, .(T88, [])))) → revA_out_ga(.(T88, .(T87, .(T86, []))), .(T86, .(T87, .(T88, []))))
revA_in_ga(.(T135, .(T134, .(T133, .(T132, [])))), .(T132, .(T133, .(T134, .(T135, []))))) → revA_out_ga(.(T135, .(T134, .(T133, .(T132, [])))), .(T132, .(T133, .(T134, .(T135, [])))))
revA_in_ga(.(T192, .(T191, .(T190, .(T189, .(T188, []))))), .(T188, .(T189, .(T190, .(T191, .(T192, [])))))) → revA_out_ga(.(T192, .(T191, .(T190, .(T189, .(T188, []))))), .(T188, .(T189, .(T190, .(T191, .(T192, []))))))
revA_in_ga(.(T259, .(T258, .(T257, .(T256, .(T255, .(T254, [])))))), .(T254, .(T255, .(T256, .(T257, .(T258, .(T259, []))))))) → revA_out_ga(.(T259, .(T258, .(T257, .(T256, .(T255, .(T254, [])))))), .(T254, .(T255, .(T256, .(T257, .(T258, .(T259, [])))))))
revA_in_ga(.(T336, .(T335, .(T334, .(T333, .(T332, .(T331, .(T330, []))))))), .(T330, .(T331, .(T332, .(T333, .(T334, .(T335, .(T336, [])))))))) → revA_out_ga(.(T336, .(T335, .(T334, .(T333, .(T332, .(T331, .(T330, []))))))), .(T330, .(T331, .(T332, .(T333, .(T334, .(T335, .(T336, []))))))))
revA_in_ga(.(T365, .(T364, .(T363, .(T362, .(T361, .(T360, .(T359, .(T357, T358)))))))), T367) → U1_ga(T365, T364, T363, T362, T361, T360, T359, T357, T358, T367, r1B_in_ggga(T358, T357, .(T359, .(T360, .(T361, .(T362, .(T363, .(T364, .(T365, []))))))), T367))
r1B_in_ggga([], T397, T398, .(T397, T398)) → r1B_out_ggga([], T397, T398, .(T397, T398))
r1B_in_ggga(.(T409, T410), T411, T412, T414) → U2_ggga(T409, T410, T411, T412, T414, r1B_in_ggga(T410, T409, .(T411, T412), T414))
U2_ggga(T409, T410, T411, T412, T414, r1B_out_ggga(T410, T409, .(T411, T412), T414)) → r1B_out_ggga(.(T409, T410), T411, T412, T414)
U1_ga(T365, T364, T363, T362, T361, T360, T359, T357, T358, T367, r1B_out_ggga(T358, T357, .(T359, .(T360, .(T361, .(T362, .(T363, .(T364, .(T365, []))))))), T367)) → revA_out_ga(.(T365, .(T364, .(T363, .(T362, .(T361, .(T360, .(T359, .(T357, T358)))))))), T367)
REVA_IN_GA(.(T365, .(T364, .(T363, .(T362, .(T361, .(T360, .(T359, .(T357, T358)))))))), T367) → U1_GA(T365, T364, T363, T362, T361, T360, T359, T357, T358, T367, r1B_in_ggga(T358, T357, .(T359, .(T360, .(T361, .(T362, .(T363, .(T364, .(T365, []))))))), T367))
REVA_IN_GA(.(T365, .(T364, .(T363, .(T362, .(T361, .(T360, .(T359, .(T357, T358)))))))), T367) → R1B_IN_GGGA(T358, T357, .(T359, .(T360, .(T361, .(T362, .(T363, .(T364, .(T365, []))))))), T367)
R1B_IN_GGGA(.(T409, T410), T411, T412, T414) → U2_GGGA(T409, T410, T411, T412, T414, r1B_in_ggga(T410, T409, .(T411, T412), T414))
R1B_IN_GGGA(.(T409, T410), T411, T412, T414) → R1B_IN_GGGA(T410, T409, .(T411, T412), T414)
revA_in_ga([], []) → revA_out_ga([], [])
revA_in_ga(.(T24, []), .(T24, [])) → revA_out_ga(.(T24, []), .(T24, []))
revA_in_ga(.(T51, .(T50, [])), .(T50, .(T51, []))) → revA_out_ga(.(T51, .(T50, [])), .(T50, .(T51, [])))
revA_in_ga(.(T88, .(T87, .(T86, []))), .(T86, .(T87, .(T88, [])))) → revA_out_ga(.(T88, .(T87, .(T86, []))), .(T86, .(T87, .(T88, []))))
revA_in_ga(.(T135, .(T134, .(T133, .(T132, [])))), .(T132, .(T133, .(T134, .(T135, []))))) → revA_out_ga(.(T135, .(T134, .(T133, .(T132, [])))), .(T132, .(T133, .(T134, .(T135, [])))))
revA_in_ga(.(T192, .(T191, .(T190, .(T189, .(T188, []))))), .(T188, .(T189, .(T190, .(T191, .(T192, [])))))) → revA_out_ga(.(T192, .(T191, .(T190, .(T189, .(T188, []))))), .(T188, .(T189, .(T190, .(T191, .(T192, []))))))
revA_in_ga(.(T259, .(T258, .(T257, .(T256, .(T255, .(T254, [])))))), .(T254, .(T255, .(T256, .(T257, .(T258, .(T259, []))))))) → revA_out_ga(.(T259, .(T258, .(T257, .(T256, .(T255, .(T254, [])))))), .(T254, .(T255, .(T256, .(T257, .(T258, .(T259, [])))))))
revA_in_ga(.(T336, .(T335, .(T334, .(T333, .(T332, .(T331, .(T330, []))))))), .(T330, .(T331, .(T332, .(T333, .(T334, .(T335, .(T336, [])))))))) → revA_out_ga(.(T336, .(T335, .(T334, .(T333, .(T332, .(T331, .(T330, []))))))), .(T330, .(T331, .(T332, .(T333, .(T334, .(T335, .(T336, []))))))))
revA_in_ga(.(T365, .(T364, .(T363, .(T362, .(T361, .(T360, .(T359, .(T357, T358)))))))), T367) → U1_ga(T365, T364, T363, T362, T361, T360, T359, T357, T358, T367, r1B_in_ggga(T358, T357, .(T359, .(T360, .(T361, .(T362, .(T363, .(T364, .(T365, []))))))), T367))
r1B_in_ggga([], T397, T398, .(T397, T398)) → r1B_out_ggga([], T397, T398, .(T397, T398))
r1B_in_ggga(.(T409, T410), T411, T412, T414) → U2_ggga(T409, T410, T411, T412, T414, r1B_in_ggga(T410, T409, .(T411, T412), T414))
U2_ggga(T409, T410, T411, T412, T414, r1B_out_ggga(T410, T409, .(T411, T412), T414)) → r1B_out_ggga(.(T409, T410), T411, T412, T414)
U1_ga(T365, T364, T363, T362, T361, T360, T359, T357, T358, T367, r1B_out_ggga(T358, T357, .(T359, .(T360, .(T361, .(T362, .(T363, .(T364, .(T365, []))))))), T367)) → revA_out_ga(.(T365, .(T364, .(T363, .(T362, .(T361, .(T360, .(T359, .(T357, T358)))))))), T367)
REVA_IN_GA(.(T365, .(T364, .(T363, .(T362, .(T361, .(T360, .(T359, .(T357, T358)))))))), T367) → U1_GA(T365, T364, T363, T362, T361, T360, T359, T357, T358, T367, r1B_in_ggga(T358, T357, .(T359, .(T360, .(T361, .(T362, .(T363, .(T364, .(T365, []))))))), T367))
REVA_IN_GA(.(T365, .(T364, .(T363, .(T362, .(T361, .(T360, .(T359, .(T357, T358)))))))), T367) → R1B_IN_GGGA(T358, T357, .(T359, .(T360, .(T361, .(T362, .(T363, .(T364, .(T365, []))))))), T367)
R1B_IN_GGGA(.(T409, T410), T411, T412, T414) → U2_GGGA(T409, T410, T411, T412, T414, r1B_in_ggga(T410, T409, .(T411, T412), T414))
R1B_IN_GGGA(.(T409, T410), T411, T412, T414) → R1B_IN_GGGA(T410, T409, .(T411, T412), T414)
revA_in_ga([], []) → revA_out_ga([], [])
revA_in_ga(.(T24, []), .(T24, [])) → revA_out_ga(.(T24, []), .(T24, []))
revA_in_ga(.(T51, .(T50, [])), .(T50, .(T51, []))) → revA_out_ga(.(T51, .(T50, [])), .(T50, .(T51, [])))
revA_in_ga(.(T88, .(T87, .(T86, []))), .(T86, .(T87, .(T88, [])))) → revA_out_ga(.(T88, .(T87, .(T86, []))), .(T86, .(T87, .(T88, []))))
revA_in_ga(.(T135, .(T134, .(T133, .(T132, [])))), .(T132, .(T133, .(T134, .(T135, []))))) → revA_out_ga(.(T135, .(T134, .(T133, .(T132, [])))), .(T132, .(T133, .(T134, .(T135, [])))))
revA_in_ga(.(T192, .(T191, .(T190, .(T189, .(T188, []))))), .(T188, .(T189, .(T190, .(T191, .(T192, [])))))) → revA_out_ga(.(T192, .(T191, .(T190, .(T189, .(T188, []))))), .(T188, .(T189, .(T190, .(T191, .(T192, []))))))
revA_in_ga(.(T259, .(T258, .(T257, .(T256, .(T255, .(T254, [])))))), .(T254, .(T255, .(T256, .(T257, .(T258, .(T259, []))))))) → revA_out_ga(.(T259, .(T258, .(T257, .(T256, .(T255, .(T254, [])))))), .(T254, .(T255, .(T256, .(T257, .(T258, .(T259, [])))))))
revA_in_ga(.(T336, .(T335, .(T334, .(T333, .(T332, .(T331, .(T330, []))))))), .(T330, .(T331, .(T332, .(T333, .(T334, .(T335, .(T336, [])))))))) → revA_out_ga(.(T336, .(T335, .(T334, .(T333, .(T332, .(T331, .(T330, []))))))), .(T330, .(T331, .(T332, .(T333, .(T334, .(T335, .(T336, []))))))))
revA_in_ga(.(T365, .(T364, .(T363, .(T362, .(T361, .(T360, .(T359, .(T357, T358)))))))), T367) → U1_ga(T365, T364, T363, T362, T361, T360, T359, T357, T358, T367, r1B_in_ggga(T358, T357, .(T359, .(T360, .(T361, .(T362, .(T363, .(T364, .(T365, []))))))), T367))
r1B_in_ggga([], T397, T398, .(T397, T398)) → r1B_out_ggga([], T397, T398, .(T397, T398))
r1B_in_ggga(.(T409, T410), T411, T412, T414) → U2_ggga(T409, T410, T411, T412, T414, r1B_in_ggga(T410, T409, .(T411, T412), T414))
U2_ggga(T409, T410, T411, T412, T414, r1B_out_ggga(T410, T409, .(T411, T412), T414)) → r1B_out_ggga(.(T409, T410), T411, T412, T414)
U1_ga(T365, T364, T363, T362, T361, T360, T359, T357, T358, T367, r1B_out_ggga(T358, T357, .(T359, .(T360, .(T361, .(T362, .(T363, .(T364, .(T365, []))))))), T367)) → revA_out_ga(.(T365, .(T364, .(T363, .(T362, .(T361, .(T360, .(T359, .(T357, T358)))))))), T367)
R1B_IN_GGGA(.(T409, T410), T411, T412, T414) → R1B_IN_GGGA(T410, T409, .(T411, T412), T414)
revA_in_ga([], []) → revA_out_ga([], [])
revA_in_ga(.(T24, []), .(T24, [])) → revA_out_ga(.(T24, []), .(T24, []))
revA_in_ga(.(T51, .(T50, [])), .(T50, .(T51, []))) → revA_out_ga(.(T51, .(T50, [])), .(T50, .(T51, [])))
revA_in_ga(.(T88, .(T87, .(T86, []))), .(T86, .(T87, .(T88, [])))) → revA_out_ga(.(T88, .(T87, .(T86, []))), .(T86, .(T87, .(T88, []))))
revA_in_ga(.(T135, .(T134, .(T133, .(T132, [])))), .(T132, .(T133, .(T134, .(T135, []))))) → revA_out_ga(.(T135, .(T134, .(T133, .(T132, [])))), .(T132, .(T133, .(T134, .(T135, [])))))
revA_in_ga(.(T192, .(T191, .(T190, .(T189, .(T188, []))))), .(T188, .(T189, .(T190, .(T191, .(T192, [])))))) → revA_out_ga(.(T192, .(T191, .(T190, .(T189, .(T188, []))))), .(T188, .(T189, .(T190, .(T191, .(T192, []))))))
revA_in_ga(.(T259, .(T258, .(T257, .(T256, .(T255, .(T254, [])))))), .(T254, .(T255, .(T256, .(T257, .(T258, .(T259, []))))))) → revA_out_ga(.(T259, .(T258, .(T257, .(T256, .(T255, .(T254, [])))))), .(T254, .(T255, .(T256, .(T257, .(T258, .(T259, [])))))))
revA_in_ga(.(T336, .(T335, .(T334, .(T333, .(T332, .(T331, .(T330, []))))))), .(T330, .(T331, .(T332, .(T333, .(T334, .(T335, .(T336, [])))))))) → revA_out_ga(.(T336, .(T335, .(T334, .(T333, .(T332, .(T331, .(T330, []))))))), .(T330, .(T331, .(T332, .(T333, .(T334, .(T335, .(T336, []))))))))
revA_in_ga(.(T365, .(T364, .(T363, .(T362, .(T361, .(T360, .(T359, .(T357, T358)))))))), T367) → U1_ga(T365, T364, T363, T362, T361, T360, T359, T357, T358, T367, r1B_in_ggga(T358, T357, .(T359, .(T360, .(T361, .(T362, .(T363, .(T364, .(T365, []))))))), T367))
r1B_in_ggga([], T397, T398, .(T397, T398)) → r1B_out_ggga([], T397, T398, .(T397, T398))
r1B_in_ggga(.(T409, T410), T411, T412, T414) → U2_ggga(T409, T410, T411, T412, T414, r1B_in_ggga(T410, T409, .(T411, T412), T414))
U2_ggga(T409, T410, T411, T412, T414, r1B_out_ggga(T410, T409, .(T411, T412), T414)) → r1B_out_ggga(.(T409, T410), T411, T412, T414)
U1_ga(T365, T364, T363, T362, T361, T360, T359, T357, T358, T367, r1B_out_ggga(T358, T357, .(T359, .(T360, .(T361, .(T362, .(T363, .(T364, .(T365, []))))))), T367)) → revA_out_ga(.(T365, .(T364, .(T363, .(T362, .(T361, .(T360, .(T359, .(T357, T358)))))))), T367)
R1B_IN_GGGA(.(T409, T410), T411, T412, T414) → R1B_IN_GGGA(T410, T409, .(T411, T412), T414)
R1B_IN_GGGA(.(T409, T410), T411, T412) → R1B_IN_GGGA(T410, T409, .(T411, T412))
From the DPs we obtained the following set of size-change graphs: