0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 95 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 12 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 PiDP
↳7 UsableRulesProof (⇔, 0 ms)
↳8 PiDP
↳9 PiDPToQDPProof (⇒, 28 ms)
↳10 QDP
↳11 QDPSizeChangeProof (⇔, 0 ms)
↳12 YES
selectA_in_gga(T6, .(T6, T7), T7) → selectA_out_gga(T6, .(T6, T7), T7)
selectA_in_gga(T23, .(T23, .(T23, T24)), .(T23, T24)) → selectA_out_gga(T23, .(T23, .(T23, T24)), .(T23, T24))
selectA_in_gga(T33, .(T33, .(T34, T35)), .(T33, .(T34, T37))) → U1_gga(T33, T34, T35, T37, selectA_in_gga(T33, T35, T37))
selectA_in_gga(T59, .(T47, .(T59, T60)), .(T47, T60)) → selectA_out_gga(T59, .(T47, .(T59, T60)), .(T47, T60))
selectA_in_gga(T69, .(T47, .(T70, T71)), .(T47, .(T70, T73))) → U2_gga(T69, T47, T70, T71, T73, selectA_in_gga(T69, T71, T73))
U2_gga(T69, T47, T70, T71, T73, selectA_out_gga(T69, T71, T73)) → selectA_out_gga(T69, .(T47, .(T70, T71)), .(T47, .(T70, T73)))
U1_gga(T33, T34, T35, T37, selectA_out_gga(T33, T35, T37)) → selectA_out_gga(T33, .(T33, .(T34, T35)), .(T33, .(T34, T37)))
SELECTA_IN_GGA(T33, .(T33, .(T34, T35)), .(T33, .(T34, T37))) → U1_GGA(T33, T34, T35, T37, selectA_in_gga(T33, T35, T37))
SELECTA_IN_GGA(T33, .(T33, .(T34, T35)), .(T33, .(T34, T37))) → SELECTA_IN_GGA(T33, T35, T37)
SELECTA_IN_GGA(T69, .(T47, .(T70, T71)), .(T47, .(T70, T73))) → U2_GGA(T69, T47, T70, T71, T73, selectA_in_gga(T69, T71, T73))
SELECTA_IN_GGA(T69, .(T47, .(T70, T71)), .(T47, .(T70, T73))) → SELECTA_IN_GGA(T69, T71, T73)
selectA_in_gga(T6, .(T6, T7), T7) → selectA_out_gga(T6, .(T6, T7), T7)
selectA_in_gga(T23, .(T23, .(T23, T24)), .(T23, T24)) → selectA_out_gga(T23, .(T23, .(T23, T24)), .(T23, T24))
selectA_in_gga(T33, .(T33, .(T34, T35)), .(T33, .(T34, T37))) → U1_gga(T33, T34, T35, T37, selectA_in_gga(T33, T35, T37))
selectA_in_gga(T59, .(T47, .(T59, T60)), .(T47, T60)) → selectA_out_gga(T59, .(T47, .(T59, T60)), .(T47, T60))
selectA_in_gga(T69, .(T47, .(T70, T71)), .(T47, .(T70, T73))) → U2_gga(T69, T47, T70, T71, T73, selectA_in_gga(T69, T71, T73))
U2_gga(T69, T47, T70, T71, T73, selectA_out_gga(T69, T71, T73)) → selectA_out_gga(T69, .(T47, .(T70, T71)), .(T47, .(T70, T73)))
U1_gga(T33, T34, T35, T37, selectA_out_gga(T33, T35, T37)) → selectA_out_gga(T33, .(T33, .(T34, T35)), .(T33, .(T34, T37)))
SELECTA_IN_GGA(T33, .(T33, .(T34, T35)), .(T33, .(T34, T37))) → U1_GGA(T33, T34, T35, T37, selectA_in_gga(T33, T35, T37))
SELECTA_IN_GGA(T33, .(T33, .(T34, T35)), .(T33, .(T34, T37))) → SELECTA_IN_GGA(T33, T35, T37)
SELECTA_IN_GGA(T69, .(T47, .(T70, T71)), .(T47, .(T70, T73))) → U2_GGA(T69, T47, T70, T71, T73, selectA_in_gga(T69, T71, T73))
SELECTA_IN_GGA(T69, .(T47, .(T70, T71)), .(T47, .(T70, T73))) → SELECTA_IN_GGA(T69, T71, T73)
selectA_in_gga(T6, .(T6, T7), T7) → selectA_out_gga(T6, .(T6, T7), T7)
selectA_in_gga(T23, .(T23, .(T23, T24)), .(T23, T24)) → selectA_out_gga(T23, .(T23, .(T23, T24)), .(T23, T24))
selectA_in_gga(T33, .(T33, .(T34, T35)), .(T33, .(T34, T37))) → U1_gga(T33, T34, T35, T37, selectA_in_gga(T33, T35, T37))
selectA_in_gga(T59, .(T47, .(T59, T60)), .(T47, T60)) → selectA_out_gga(T59, .(T47, .(T59, T60)), .(T47, T60))
selectA_in_gga(T69, .(T47, .(T70, T71)), .(T47, .(T70, T73))) → U2_gga(T69, T47, T70, T71, T73, selectA_in_gga(T69, T71, T73))
U2_gga(T69, T47, T70, T71, T73, selectA_out_gga(T69, T71, T73)) → selectA_out_gga(T69, .(T47, .(T70, T71)), .(T47, .(T70, T73)))
U1_gga(T33, T34, T35, T37, selectA_out_gga(T33, T35, T37)) → selectA_out_gga(T33, .(T33, .(T34, T35)), .(T33, .(T34, T37)))
SELECTA_IN_GGA(T69, .(T47, .(T70, T71)), .(T47, .(T70, T73))) → SELECTA_IN_GGA(T69, T71, T73)
SELECTA_IN_GGA(T33, .(T33, .(T34, T35)), .(T33, .(T34, T37))) → SELECTA_IN_GGA(T33, T35, T37)
selectA_in_gga(T6, .(T6, T7), T7) → selectA_out_gga(T6, .(T6, T7), T7)
selectA_in_gga(T23, .(T23, .(T23, T24)), .(T23, T24)) → selectA_out_gga(T23, .(T23, .(T23, T24)), .(T23, T24))
selectA_in_gga(T33, .(T33, .(T34, T35)), .(T33, .(T34, T37))) → U1_gga(T33, T34, T35, T37, selectA_in_gga(T33, T35, T37))
selectA_in_gga(T59, .(T47, .(T59, T60)), .(T47, T60)) → selectA_out_gga(T59, .(T47, .(T59, T60)), .(T47, T60))
selectA_in_gga(T69, .(T47, .(T70, T71)), .(T47, .(T70, T73))) → U2_gga(T69, T47, T70, T71, T73, selectA_in_gga(T69, T71, T73))
U2_gga(T69, T47, T70, T71, T73, selectA_out_gga(T69, T71, T73)) → selectA_out_gga(T69, .(T47, .(T70, T71)), .(T47, .(T70, T73)))
U1_gga(T33, T34, T35, T37, selectA_out_gga(T33, T35, T37)) → selectA_out_gga(T33, .(T33, .(T34, T35)), .(T33, .(T34, T37)))
SELECTA_IN_GGA(T69, .(T47, .(T70, T71)), .(T47, .(T70, T73))) → SELECTA_IN_GGA(T69, T71, T73)
SELECTA_IN_GGA(T33, .(T33, .(T34, T35)), .(T33, .(T34, T37))) → SELECTA_IN_GGA(T33, T35, T37)
SELECTA_IN_GGA(T69, .(T47, .(T70, T71))) → SELECTA_IN_GGA(T69, T71)
SELECTA_IN_GGA(T33, .(T33, .(T34, T35))) → SELECTA_IN_GGA(T33, T35)
From the DPs we obtained the following set of size-change graphs: