0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 140 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 58 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 PiDP
↳7 UsableRulesProof (⇔, 0 ms)
↳8 PiDP
↳9 PiDPToQDPProof (⇒, 20 ms)
↳10 QDP
↳11 QDPSizeChangeProof (⇔, 0 ms)
↳12 YES
avgA_in_gag(s(s(T23)), T26, T25) → U1_gag(T23, T26, T25, avgA_in_gag(T23, s(s(T26)), T25))
avgA_in_gag(s(T42), s(s(T45)), s(T44)) → U2_gag(T42, T45, T44, avgA_in_gag(s(T42), T45, T44))
avgA_in_gag(s(0), 0, 0) → avgA_out_gag(s(0), 0, 0)
avgA_in_gag(s(0), s(0), s(0)) → avgA_out_gag(s(0), s(0), s(0))
avgA_in_gag(s(T61), s(s(s(T64))), s(T63)) → U3_gag(T61, T64, T63, avgA_in_gag(s(s(T61)), T64, T63))
avgA_in_gag(T101, s(s(s(T104))), s(T103)) → U4_gag(T101, T104, T103, avgA_in_gag(T101, s(T104), T103))
avgA_in_gag(T123, s(s(s(s(s(s(T126)))))), s(s(T125))) → U5_gag(T123, T126, T125, avgA_in_gag(s(s(T123)), T126, T125))
avgA_in_gag(0, s(s(0)), s(0)) → avgA_out_gag(0, s(s(0)), s(0))
avgA_in_gag(0, 0, 0) → avgA_out_gag(0, 0, 0)
avgA_in_gag(0, s(0), 0) → avgA_out_gag(0, s(0), 0)
U5_gag(T123, T126, T125, avgA_out_gag(s(s(T123)), T126, T125)) → avgA_out_gag(T123, s(s(s(s(s(s(T126)))))), s(s(T125)))
U4_gag(T101, T104, T103, avgA_out_gag(T101, s(T104), T103)) → avgA_out_gag(T101, s(s(s(T104))), s(T103))
U3_gag(T61, T64, T63, avgA_out_gag(s(s(T61)), T64, T63)) → avgA_out_gag(s(T61), s(s(s(T64))), s(T63))
U2_gag(T42, T45, T44, avgA_out_gag(s(T42), T45, T44)) → avgA_out_gag(s(T42), s(s(T45)), s(T44))
U1_gag(T23, T26, T25, avgA_out_gag(T23, s(s(T26)), T25)) → avgA_out_gag(s(s(T23)), T26, T25)
AVGA_IN_GAG(s(s(T23)), T26, T25) → U1_GAG(T23, T26, T25, avgA_in_gag(T23, s(s(T26)), T25))
AVGA_IN_GAG(s(s(T23)), T26, T25) → AVGA_IN_GAG(T23, s(s(T26)), T25)
AVGA_IN_GAG(s(T42), s(s(T45)), s(T44)) → U2_GAG(T42, T45, T44, avgA_in_gag(s(T42), T45, T44))
AVGA_IN_GAG(s(T42), s(s(T45)), s(T44)) → AVGA_IN_GAG(s(T42), T45, T44)
AVGA_IN_GAG(s(T61), s(s(s(T64))), s(T63)) → U3_GAG(T61, T64, T63, avgA_in_gag(s(s(T61)), T64, T63))
AVGA_IN_GAG(s(T61), s(s(s(T64))), s(T63)) → AVGA_IN_GAG(s(s(T61)), T64, T63)
AVGA_IN_GAG(T101, s(s(s(T104))), s(T103)) → U4_GAG(T101, T104, T103, avgA_in_gag(T101, s(T104), T103))
AVGA_IN_GAG(T101, s(s(s(T104))), s(T103)) → AVGA_IN_GAG(T101, s(T104), T103)
AVGA_IN_GAG(T123, s(s(s(s(s(s(T126)))))), s(s(T125))) → U5_GAG(T123, T126, T125, avgA_in_gag(s(s(T123)), T126, T125))
AVGA_IN_GAG(T123, s(s(s(s(s(s(T126)))))), s(s(T125))) → AVGA_IN_GAG(s(s(T123)), T126, T125)
avgA_in_gag(s(s(T23)), T26, T25) → U1_gag(T23, T26, T25, avgA_in_gag(T23, s(s(T26)), T25))
avgA_in_gag(s(T42), s(s(T45)), s(T44)) → U2_gag(T42, T45, T44, avgA_in_gag(s(T42), T45, T44))
avgA_in_gag(s(0), 0, 0) → avgA_out_gag(s(0), 0, 0)
avgA_in_gag(s(0), s(0), s(0)) → avgA_out_gag(s(0), s(0), s(0))
avgA_in_gag(s(T61), s(s(s(T64))), s(T63)) → U3_gag(T61, T64, T63, avgA_in_gag(s(s(T61)), T64, T63))
avgA_in_gag(T101, s(s(s(T104))), s(T103)) → U4_gag(T101, T104, T103, avgA_in_gag(T101, s(T104), T103))
avgA_in_gag(T123, s(s(s(s(s(s(T126)))))), s(s(T125))) → U5_gag(T123, T126, T125, avgA_in_gag(s(s(T123)), T126, T125))
avgA_in_gag(0, s(s(0)), s(0)) → avgA_out_gag(0, s(s(0)), s(0))
avgA_in_gag(0, 0, 0) → avgA_out_gag(0, 0, 0)
avgA_in_gag(0, s(0), 0) → avgA_out_gag(0, s(0), 0)
U5_gag(T123, T126, T125, avgA_out_gag(s(s(T123)), T126, T125)) → avgA_out_gag(T123, s(s(s(s(s(s(T126)))))), s(s(T125)))
U4_gag(T101, T104, T103, avgA_out_gag(T101, s(T104), T103)) → avgA_out_gag(T101, s(s(s(T104))), s(T103))
U3_gag(T61, T64, T63, avgA_out_gag(s(s(T61)), T64, T63)) → avgA_out_gag(s(T61), s(s(s(T64))), s(T63))
U2_gag(T42, T45, T44, avgA_out_gag(s(T42), T45, T44)) → avgA_out_gag(s(T42), s(s(T45)), s(T44))
U1_gag(T23, T26, T25, avgA_out_gag(T23, s(s(T26)), T25)) → avgA_out_gag(s(s(T23)), T26, T25)
AVGA_IN_GAG(s(s(T23)), T26, T25) → U1_GAG(T23, T26, T25, avgA_in_gag(T23, s(s(T26)), T25))
AVGA_IN_GAG(s(s(T23)), T26, T25) → AVGA_IN_GAG(T23, s(s(T26)), T25)
AVGA_IN_GAG(s(T42), s(s(T45)), s(T44)) → U2_GAG(T42, T45, T44, avgA_in_gag(s(T42), T45, T44))
AVGA_IN_GAG(s(T42), s(s(T45)), s(T44)) → AVGA_IN_GAG(s(T42), T45, T44)
AVGA_IN_GAG(s(T61), s(s(s(T64))), s(T63)) → U3_GAG(T61, T64, T63, avgA_in_gag(s(s(T61)), T64, T63))
AVGA_IN_GAG(s(T61), s(s(s(T64))), s(T63)) → AVGA_IN_GAG(s(s(T61)), T64, T63)
AVGA_IN_GAG(T101, s(s(s(T104))), s(T103)) → U4_GAG(T101, T104, T103, avgA_in_gag(T101, s(T104), T103))
AVGA_IN_GAG(T101, s(s(s(T104))), s(T103)) → AVGA_IN_GAG(T101, s(T104), T103)
AVGA_IN_GAG(T123, s(s(s(s(s(s(T126)))))), s(s(T125))) → U5_GAG(T123, T126, T125, avgA_in_gag(s(s(T123)), T126, T125))
AVGA_IN_GAG(T123, s(s(s(s(s(s(T126)))))), s(s(T125))) → AVGA_IN_GAG(s(s(T123)), T126, T125)
avgA_in_gag(s(s(T23)), T26, T25) → U1_gag(T23, T26, T25, avgA_in_gag(T23, s(s(T26)), T25))
avgA_in_gag(s(T42), s(s(T45)), s(T44)) → U2_gag(T42, T45, T44, avgA_in_gag(s(T42), T45, T44))
avgA_in_gag(s(0), 0, 0) → avgA_out_gag(s(0), 0, 0)
avgA_in_gag(s(0), s(0), s(0)) → avgA_out_gag(s(0), s(0), s(0))
avgA_in_gag(s(T61), s(s(s(T64))), s(T63)) → U3_gag(T61, T64, T63, avgA_in_gag(s(s(T61)), T64, T63))
avgA_in_gag(T101, s(s(s(T104))), s(T103)) → U4_gag(T101, T104, T103, avgA_in_gag(T101, s(T104), T103))
avgA_in_gag(T123, s(s(s(s(s(s(T126)))))), s(s(T125))) → U5_gag(T123, T126, T125, avgA_in_gag(s(s(T123)), T126, T125))
avgA_in_gag(0, s(s(0)), s(0)) → avgA_out_gag(0, s(s(0)), s(0))
avgA_in_gag(0, 0, 0) → avgA_out_gag(0, 0, 0)
avgA_in_gag(0, s(0), 0) → avgA_out_gag(0, s(0), 0)
U5_gag(T123, T126, T125, avgA_out_gag(s(s(T123)), T126, T125)) → avgA_out_gag(T123, s(s(s(s(s(s(T126)))))), s(s(T125)))
U4_gag(T101, T104, T103, avgA_out_gag(T101, s(T104), T103)) → avgA_out_gag(T101, s(s(s(T104))), s(T103))
U3_gag(T61, T64, T63, avgA_out_gag(s(s(T61)), T64, T63)) → avgA_out_gag(s(T61), s(s(s(T64))), s(T63))
U2_gag(T42, T45, T44, avgA_out_gag(s(T42), T45, T44)) → avgA_out_gag(s(T42), s(s(T45)), s(T44))
U1_gag(T23, T26, T25, avgA_out_gag(T23, s(s(T26)), T25)) → avgA_out_gag(s(s(T23)), T26, T25)
AVGA_IN_GAG(s(T42), s(s(T45)), s(T44)) → AVGA_IN_GAG(s(T42), T45, T44)
AVGA_IN_GAG(s(s(T23)), T26, T25) → AVGA_IN_GAG(T23, s(s(T26)), T25)
AVGA_IN_GAG(s(T61), s(s(s(T64))), s(T63)) → AVGA_IN_GAG(s(s(T61)), T64, T63)
AVGA_IN_GAG(T101, s(s(s(T104))), s(T103)) → AVGA_IN_GAG(T101, s(T104), T103)
AVGA_IN_GAG(T123, s(s(s(s(s(s(T126)))))), s(s(T125))) → AVGA_IN_GAG(s(s(T123)), T126, T125)
avgA_in_gag(s(s(T23)), T26, T25) → U1_gag(T23, T26, T25, avgA_in_gag(T23, s(s(T26)), T25))
avgA_in_gag(s(T42), s(s(T45)), s(T44)) → U2_gag(T42, T45, T44, avgA_in_gag(s(T42), T45, T44))
avgA_in_gag(s(0), 0, 0) → avgA_out_gag(s(0), 0, 0)
avgA_in_gag(s(0), s(0), s(0)) → avgA_out_gag(s(0), s(0), s(0))
avgA_in_gag(s(T61), s(s(s(T64))), s(T63)) → U3_gag(T61, T64, T63, avgA_in_gag(s(s(T61)), T64, T63))
avgA_in_gag(T101, s(s(s(T104))), s(T103)) → U4_gag(T101, T104, T103, avgA_in_gag(T101, s(T104), T103))
avgA_in_gag(T123, s(s(s(s(s(s(T126)))))), s(s(T125))) → U5_gag(T123, T126, T125, avgA_in_gag(s(s(T123)), T126, T125))
avgA_in_gag(0, s(s(0)), s(0)) → avgA_out_gag(0, s(s(0)), s(0))
avgA_in_gag(0, 0, 0) → avgA_out_gag(0, 0, 0)
avgA_in_gag(0, s(0), 0) → avgA_out_gag(0, s(0), 0)
U5_gag(T123, T126, T125, avgA_out_gag(s(s(T123)), T126, T125)) → avgA_out_gag(T123, s(s(s(s(s(s(T126)))))), s(s(T125)))
U4_gag(T101, T104, T103, avgA_out_gag(T101, s(T104), T103)) → avgA_out_gag(T101, s(s(s(T104))), s(T103))
U3_gag(T61, T64, T63, avgA_out_gag(s(s(T61)), T64, T63)) → avgA_out_gag(s(T61), s(s(s(T64))), s(T63))
U2_gag(T42, T45, T44, avgA_out_gag(s(T42), T45, T44)) → avgA_out_gag(s(T42), s(s(T45)), s(T44))
U1_gag(T23, T26, T25, avgA_out_gag(T23, s(s(T26)), T25)) → avgA_out_gag(s(s(T23)), T26, T25)
AVGA_IN_GAG(s(T42), s(s(T45)), s(T44)) → AVGA_IN_GAG(s(T42), T45, T44)
AVGA_IN_GAG(s(s(T23)), T26, T25) → AVGA_IN_GAG(T23, s(s(T26)), T25)
AVGA_IN_GAG(s(T61), s(s(s(T64))), s(T63)) → AVGA_IN_GAG(s(s(T61)), T64, T63)
AVGA_IN_GAG(T101, s(s(s(T104))), s(T103)) → AVGA_IN_GAG(T101, s(T104), T103)
AVGA_IN_GAG(T123, s(s(s(s(s(s(T126)))))), s(s(T125))) → AVGA_IN_GAG(s(s(T123)), T126, T125)
AVGA_IN_GAG(s(T42), s(T44)) → AVGA_IN_GAG(s(T42), T44)
AVGA_IN_GAG(s(s(T23)), T25) → AVGA_IN_GAG(T23, T25)
AVGA_IN_GAG(s(T61), s(T63)) → AVGA_IN_GAG(s(s(T61)), T63)
AVGA_IN_GAG(T101, s(T103)) → AVGA_IN_GAG(T101, T103)
AVGA_IN_GAG(T123, s(s(T125))) → AVGA_IN_GAG(s(s(T123)), T125)
From the DPs we obtained the following set of size-change graphs: