0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 109 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 0 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 PiDP
↳7 UsableRulesProof (⇔, 0 ms)
↳8 PiDP
↳9 PiDPToQDPProof (⇒, 11 ms)
↳10 QDP
↳11 QDPSizeChangeProof (⇔, 0 ms)
↳12 YES
maxA_in_aag(s(T13), 0, s(T13)) → maxA_out_aag(s(T13), 0, s(T13))
maxA_in_aag(s(T23), s(T24), s(T23)) → U1_aag(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_aag(T23, T24, lessB_out_ag(T24, T23)) → maxA_out_aag(s(T23), s(T24), s(T23))
maxA_in_aag(T47, T46, T46) → U2_aag(T47, T46, lessB_in_ag(T47, s(T46)))
U2_aag(T47, T46, lessB_out_ag(T47, s(T46))) → maxA_out_aag(T47, T46, T46)
maxA_in_aag(0, T59, T59) → maxA_out_aag(0, T59, T59)
maxA_in_aag(s(T66), T65, T65) → U3_aag(T66, T65, lessB_in_ag(T66, T65))
U3_aag(T66, T65, lessB_out_ag(T66, T65)) → maxA_out_aag(s(T66), T65, T65)
MAXA_IN_AAG(s(T23), s(T24), s(T23)) → U1_AAG(T23, T24, lessB_in_ag(T24, T23))
MAXA_IN_AAG(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_AAG(T47, T46, T46) → U2_AAG(T47, T46, lessB_in_ag(T47, s(T46)))
MAXA_IN_AAG(T47, T46, T46) → LESSB_IN_AG(T47, s(T46))
MAXA_IN_AAG(s(T66), T65, T65) → U3_AAG(T66, T65, lessB_in_ag(T66, T65))
MAXA_IN_AAG(s(T66), T65, T65) → LESSB_IN_AG(T66, T65)
maxA_in_aag(s(T13), 0, s(T13)) → maxA_out_aag(s(T13), 0, s(T13))
maxA_in_aag(s(T23), s(T24), s(T23)) → U1_aag(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_aag(T23, T24, lessB_out_ag(T24, T23)) → maxA_out_aag(s(T23), s(T24), s(T23))
maxA_in_aag(T47, T46, T46) → U2_aag(T47, T46, lessB_in_ag(T47, s(T46)))
U2_aag(T47, T46, lessB_out_ag(T47, s(T46))) → maxA_out_aag(T47, T46, T46)
maxA_in_aag(0, T59, T59) → maxA_out_aag(0, T59, T59)
maxA_in_aag(s(T66), T65, T65) → U3_aag(T66, T65, lessB_in_ag(T66, T65))
U3_aag(T66, T65, lessB_out_ag(T66, T65)) → maxA_out_aag(s(T66), T65, T65)
MAXA_IN_AAG(s(T23), s(T24), s(T23)) → U1_AAG(T23, T24, lessB_in_ag(T24, T23))
MAXA_IN_AAG(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_AAG(T47, T46, T46) → U2_AAG(T47, T46, lessB_in_ag(T47, s(T46)))
MAXA_IN_AAG(T47, T46, T46) → LESSB_IN_AG(T47, s(T46))
MAXA_IN_AAG(s(T66), T65, T65) → U3_AAG(T66, T65, lessB_in_ag(T66, T65))
MAXA_IN_AAG(s(T66), T65, T65) → LESSB_IN_AG(T66, T65)
maxA_in_aag(s(T13), 0, s(T13)) → maxA_out_aag(s(T13), 0, s(T13))
maxA_in_aag(s(T23), s(T24), s(T23)) → U1_aag(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_aag(T23, T24, lessB_out_ag(T24, T23)) → maxA_out_aag(s(T23), s(T24), s(T23))
maxA_in_aag(T47, T46, T46) → U2_aag(T47, T46, lessB_in_ag(T47, s(T46)))
U2_aag(T47, T46, lessB_out_ag(T47, s(T46))) → maxA_out_aag(T47, T46, T46)
maxA_in_aag(0, T59, T59) → maxA_out_aag(0, T59, T59)
maxA_in_aag(s(T66), T65, T65) → U3_aag(T66, T65, lessB_in_ag(T66, T65))
U3_aag(T66, T65, lessB_out_ag(T66, T65)) → maxA_out_aag(s(T66), T65, T65)
LESSB_IN_AG(s(T38), s(T37)) → LESSB_IN_AG(T38, T37)
maxA_in_aag(s(T13), 0, s(T13)) → maxA_out_aag(s(T13), 0, s(T13))
maxA_in_aag(s(T23), s(T24), s(T23)) → U1_aag(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_aag(T23, T24, lessB_out_ag(T24, T23)) → maxA_out_aag(s(T23), s(T24), s(T23))
maxA_in_aag(T47, T46, T46) → U2_aag(T47, T46, lessB_in_ag(T47, s(T46)))
U2_aag(T47, T46, lessB_out_ag(T47, s(T46))) → maxA_out_aag(T47, T46, T46)
maxA_in_aag(0, T59, T59) → maxA_out_aag(0, T59, T59)
maxA_in_aag(s(T66), T65, T65) → U3_aag(T66, T65, lessB_in_ag(T66, T65))
U3_aag(T66, T65, lessB_out_ag(T66, T65)) → maxA_out_aag(s(T66), T65, T65)
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: