0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 115 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 32 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 3 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇒, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
maxA_in_gaa(s(T13), 0, s(T13)) → maxA_out_gaa(s(T13), 0, s(T13))
maxA_in_gaa(s(T23), s(T24), s(T23)) → U1_gaa(T23, T24, lessB_in_ag(T24, T23))
lessB_in_ag(0, s(T31)) → lessB_out_ag(0, s(T31))
lessB_in_ag(s(T38), s(T37)) → U4_ag(T38, T37, lessB_in_ag(T38, T37))
U4_ag(T38, T37, lessB_out_ag(T38, T37)) → lessB_out_ag(s(T38), s(T37))
U1_gaa(T23, T24, lessB_out_ag(T24, T23)) → maxA_out_gaa(s(T23), s(T24), s(T23))
maxA_in_gaa(0, T54, T54) → maxA_out_gaa(0, T54, T54)
maxA_in_gaa(s(T59), T61, T61) → U2_gaa(T59, T61, lessC_in_ga(T59, T61))
lessC_in_ga(0, s(T68)) → lessC_out_ga(0, s(T68))
lessC_in_ga(s(T73), s(T75)) → U5_ga(T73, T75, lessC_in_ga(T73, T75))
U5_ga(T73, T75, lessC_out_ga(T73, T75)) → lessC_out_ga(s(T73), s(T75))
U2_gaa(T59, T61, lessC_out_ga(T59, T61)) → maxA_out_gaa(s(T59), T61, T61)
maxA_in_gaa(s(T92), T94, T94) → U3_gaa(T92, T94, lessC_in_ga(T92, T94))
U3_gaa(T92, T94, lessC_out_ga(T92, T94)) → maxA_out_gaa(s(T92), T94, T94)
MAXA_IN_GAA(s(T23), s(T24), s(T23)) → U1_GAA(T23, T24, lessB_in_ag(T24, T23))
MAXA_IN_GAA(s(T23), s(T24), s(T23)) → LESSB_IN_AG(T24, T23)
LESSB_IN_AG(s(T38), s(T37)) → U4_AG(T38, T37, lessB_in_ag(T38, T37))
LESSB_IN_AG(s(T38), s(T37)) → LESSB_IN_AG(T38, T37)
MAXA_IN_GAA(s(T59), T61, T61) → U2_GAA(T59, T61, lessC_in_ga(T59, T61))
MAXA_IN_GAA(s(T59), T61, T61) → LESSC_IN_GA(T59, T61)
LESSC_IN_GA(s(T73), s(T75)) → U5_GA(T73, T75, lessC_in_ga(T73, T75))
LESSC_IN_GA(s(T73), s(T75)) → LESSC_IN_GA(T73, T75)
MAXA_IN_GAA(s(T92), T94, T94) → U3_GAA(T92, T94, lessC_in_ga(T92, T94))
maxA_in_gaa(s(T13), 0, s(T13)) → maxA_out_gaa(s(T13), 0, s(T13))
maxA_in_gaa(s(T23), s(T24), s(T23)) → U1_gaa(T23, T24, lessB_in_ag(T24, T23))
lessB_in_ag(0, s(T31)) → lessB_out_ag(0, s(T31))
lessB_in_ag(s(T38), s(T37)) → U4_ag(T38, T37, lessB_in_ag(T38, T37))
U4_ag(T38, T37, lessB_out_ag(T38, T37)) → lessB_out_ag(s(T38), s(T37))
U1_gaa(T23, T24, lessB_out_ag(T24, T23)) → maxA_out_gaa(s(T23), s(T24), s(T23))
maxA_in_gaa(0, T54, T54) → maxA_out_gaa(0, T54, T54)
maxA_in_gaa(s(T59), T61, T61) → U2_gaa(T59, T61, lessC_in_ga(T59, T61))
lessC_in_ga(0, s(T68)) → lessC_out_ga(0, s(T68))
lessC_in_ga(s(T73), s(T75)) → U5_ga(T73, T75, lessC_in_ga(T73, T75))
U5_ga(T73, T75, lessC_out_ga(T73, T75)) → lessC_out_ga(s(T73), s(T75))
U2_gaa(T59, T61, lessC_out_ga(T59, T61)) → maxA_out_gaa(s(T59), T61, T61)
maxA_in_gaa(s(T92), T94, T94) → U3_gaa(T92, T94, lessC_in_ga(T92, T94))
U3_gaa(T92, T94, lessC_out_ga(T92, T94)) → maxA_out_gaa(s(T92), T94, T94)
MAXA_IN_GAA(s(T23), s(T24), s(T23)) → U1_GAA(T23, T24, lessB_in_ag(T24, T23))
MAXA_IN_GAA(s(T23), s(T24), s(T23)) → LESSB_IN_AG(T24, T23)
LESSB_IN_AG(s(T38), s(T37)) → U4_AG(T38, T37, lessB_in_ag(T38, T37))
LESSB_IN_AG(s(T38), s(T37)) → LESSB_IN_AG(T38, T37)
MAXA_IN_GAA(s(T59), T61, T61) → U2_GAA(T59, T61, lessC_in_ga(T59, T61))
MAXA_IN_GAA(s(T59), T61, T61) → LESSC_IN_GA(T59, T61)
LESSC_IN_GA(s(T73), s(T75)) → U5_GA(T73, T75, lessC_in_ga(T73, T75))
LESSC_IN_GA(s(T73), s(T75)) → LESSC_IN_GA(T73, T75)
MAXA_IN_GAA(s(T92), T94, T94) → U3_GAA(T92, T94, lessC_in_ga(T92, T94))
maxA_in_gaa(s(T13), 0, s(T13)) → maxA_out_gaa(s(T13), 0, s(T13))
maxA_in_gaa(s(T23), s(T24), s(T23)) → U1_gaa(T23, T24, lessB_in_ag(T24, T23))
lessB_in_ag(0, s(T31)) → lessB_out_ag(0, s(T31))
lessB_in_ag(s(T38), s(T37)) → U4_ag(T38, T37, lessB_in_ag(T38, T37))
U4_ag(T38, T37, lessB_out_ag(T38, T37)) → lessB_out_ag(s(T38), s(T37))
U1_gaa(T23, T24, lessB_out_ag(T24, T23)) → maxA_out_gaa(s(T23), s(T24), s(T23))
maxA_in_gaa(0, T54, T54) → maxA_out_gaa(0, T54, T54)
maxA_in_gaa(s(T59), T61, T61) → U2_gaa(T59, T61, lessC_in_ga(T59, T61))
lessC_in_ga(0, s(T68)) → lessC_out_ga(0, s(T68))
lessC_in_ga(s(T73), s(T75)) → U5_ga(T73, T75, lessC_in_ga(T73, T75))
U5_ga(T73, T75, lessC_out_ga(T73, T75)) → lessC_out_ga(s(T73), s(T75))
U2_gaa(T59, T61, lessC_out_ga(T59, T61)) → maxA_out_gaa(s(T59), T61, T61)
maxA_in_gaa(s(T92), T94, T94) → U3_gaa(T92, T94, lessC_in_ga(T92, T94))
U3_gaa(T92, T94, lessC_out_ga(T92, T94)) → maxA_out_gaa(s(T92), T94, T94)
LESSC_IN_GA(s(T73), s(T75)) → LESSC_IN_GA(T73, T75)
maxA_in_gaa(s(T13), 0, s(T13)) → maxA_out_gaa(s(T13), 0, s(T13))
maxA_in_gaa(s(T23), s(T24), s(T23)) → U1_gaa(T23, T24, lessB_in_ag(T24, T23))
lessB_in_ag(0, s(T31)) → lessB_out_ag(0, s(T31))
lessB_in_ag(s(T38), s(T37)) → U4_ag(T38, T37, lessB_in_ag(T38, T37))
U4_ag(T38, T37, lessB_out_ag(T38, T37)) → lessB_out_ag(s(T38), s(T37))
U1_gaa(T23, T24, lessB_out_ag(T24, T23)) → maxA_out_gaa(s(T23), s(T24), s(T23))
maxA_in_gaa(0, T54, T54) → maxA_out_gaa(0, T54, T54)
maxA_in_gaa(s(T59), T61, T61) → U2_gaa(T59, T61, lessC_in_ga(T59, T61))
lessC_in_ga(0, s(T68)) → lessC_out_ga(0, s(T68))
lessC_in_ga(s(T73), s(T75)) → U5_ga(T73, T75, lessC_in_ga(T73, T75))
U5_ga(T73, T75, lessC_out_ga(T73, T75)) → lessC_out_ga(s(T73), s(T75))
U2_gaa(T59, T61, lessC_out_ga(T59, T61)) → maxA_out_gaa(s(T59), T61, T61)
maxA_in_gaa(s(T92), T94, T94) → U3_gaa(T92, T94, lessC_in_ga(T92, T94))
U3_gaa(T92, T94, lessC_out_ga(T92, T94)) → maxA_out_gaa(s(T92), T94, T94)
LESSC_IN_GA(s(T73), s(T75)) → LESSC_IN_GA(T73, T75)
LESSC_IN_GA(s(T73)) → LESSC_IN_GA(T73)
From the DPs we obtained the following set of size-change graphs:
LESSB_IN_AG(s(T38), s(T37)) → LESSB_IN_AG(T38, T37)
maxA_in_gaa(s(T13), 0, s(T13)) → maxA_out_gaa(s(T13), 0, s(T13))
maxA_in_gaa(s(T23), s(T24), s(T23)) → U1_gaa(T23, T24, lessB_in_ag(T24, T23))
lessB_in_ag(0, s(T31)) → lessB_out_ag(0, s(T31))
lessB_in_ag(s(T38), s(T37)) → U4_ag(T38, T37, lessB_in_ag(T38, T37))
U4_ag(T38, T37, lessB_out_ag(T38, T37)) → lessB_out_ag(s(T38), s(T37))
U1_gaa(T23, T24, lessB_out_ag(T24, T23)) → maxA_out_gaa(s(T23), s(T24), s(T23))
maxA_in_gaa(0, T54, T54) → maxA_out_gaa(0, T54, T54)
maxA_in_gaa(s(T59), T61, T61) → U2_gaa(T59, T61, lessC_in_ga(T59, T61))
lessC_in_ga(0, s(T68)) → lessC_out_ga(0, s(T68))
lessC_in_ga(s(T73), s(T75)) → U5_ga(T73, T75, lessC_in_ga(T73, T75))
U5_ga(T73, T75, lessC_out_ga(T73, T75)) → lessC_out_ga(s(T73), s(T75))
U2_gaa(T59, T61, lessC_out_ga(T59, T61)) → maxA_out_gaa(s(T59), T61, T61)
maxA_in_gaa(s(T92), T94, T94) → U3_gaa(T92, T94, lessC_in_ga(T92, T94))
U3_gaa(T92, T94, lessC_out_ga(T92, T94)) → maxA_out_gaa(s(T92), T94, T94)
LESSB_IN_AG(s(T38), s(T37)) → LESSB_IN_AG(T38, T37)
LESSB_IN_AG(s(T37)) → LESSB_IN_AG(T37)
From the DPs we obtained the following set of size-change graphs: