0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 66 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 0 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 4 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇔, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇔, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
hA_in_g(c(s(T8), T9)) → U1_g(T8, T9, pB_in_gg(T8, T9))
pB_in_gg(T8, T9) → U4_gg(T8, T9, fC_in_gg(T8, T9))
fC_in_gg(s(T18), T19) → U2_gg(T18, T19, fC_in_gg(T18, s(T19)))
U2_gg(T18, T19, fC_out_gg(T18, s(T19))) → fC_out_gg(s(T18), T19)
U4_gg(T8, T9, fC_out_gg(T8, T9)) → U5_gg(T8, T9, gD_in_gg(T8, T9))
gD_in_gg(T28, s(T29)) → U3_gg(T28, T29, gD_in_gg(s(T28), T29))
U3_gg(T28, T29, gD_out_gg(s(T28), T29)) → gD_out_gg(T28, s(T29))
U5_gg(T8, T9, gD_out_gg(T8, T9)) → pB_out_gg(T8, T9)
U1_g(T8, T9, pB_out_gg(T8, T9)) → hA_out_g(c(s(T8), T9))
HA_IN_G(c(s(T8), T9)) → U1_G(T8, T9, pB_in_gg(T8, T9))
HA_IN_G(c(s(T8), T9)) → PB_IN_GG(T8, T9)
PB_IN_GG(T8, T9) → U4_GG(T8, T9, fC_in_gg(T8, T9))
PB_IN_GG(T8, T9) → FC_IN_GG(T8, T9)
FC_IN_GG(s(T18), T19) → U2_GG(T18, T19, fC_in_gg(T18, s(T19)))
FC_IN_GG(s(T18), T19) → FC_IN_GG(T18, s(T19))
U4_GG(T8, T9, fC_out_gg(T8, T9)) → U5_GG(T8, T9, gD_in_gg(T8, T9))
U4_GG(T8, T9, fC_out_gg(T8, T9)) → GD_IN_GG(T8, T9)
GD_IN_GG(T28, s(T29)) → U3_GG(T28, T29, gD_in_gg(s(T28), T29))
GD_IN_GG(T28, s(T29)) → GD_IN_GG(s(T28), T29)
hA_in_g(c(s(T8), T9)) → U1_g(T8, T9, pB_in_gg(T8, T9))
pB_in_gg(T8, T9) → U4_gg(T8, T9, fC_in_gg(T8, T9))
fC_in_gg(s(T18), T19) → U2_gg(T18, T19, fC_in_gg(T18, s(T19)))
U2_gg(T18, T19, fC_out_gg(T18, s(T19))) → fC_out_gg(s(T18), T19)
U4_gg(T8, T9, fC_out_gg(T8, T9)) → U5_gg(T8, T9, gD_in_gg(T8, T9))
gD_in_gg(T28, s(T29)) → U3_gg(T28, T29, gD_in_gg(s(T28), T29))
U3_gg(T28, T29, gD_out_gg(s(T28), T29)) → gD_out_gg(T28, s(T29))
U5_gg(T8, T9, gD_out_gg(T8, T9)) → pB_out_gg(T8, T9)
U1_g(T8, T9, pB_out_gg(T8, T9)) → hA_out_g(c(s(T8), T9))
HA_IN_G(c(s(T8), T9)) → U1_G(T8, T9, pB_in_gg(T8, T9))
HA_IN_G(c(s(T8), T9)) → PB_IN_GG(T8, T9)
PB_IN_GG(T8, T9) → U4_GG(T8, T9, fC_in_gg(T8, T9))
PB_IN_GG(T8, T9) → FC_IN_GG(T8, T9)
FC_IN_GG(s(T18), T19) → U2_GG(T18, T19, fC_in_gg(T18, s(T19)))
FC_IN_GG(s(T18), T19) → FC_IN_GG(T18, s(T19))
U4_GG(T8, T9, fC_out_gg(T8, T9)) → U5_GG(T8, T9, gD_in_gg(T8, T9))
U4_GG(T8, T9, fC_out_gg(T8, T9)) → GD_IN_GG(T8, T9)
GD_IN_GG(T28, s(T29)) → U3_GG(T28, T29, gD_in_gg(s(T28), T29))
GD_IN_GG(T28, s(T29)) → GD_IN_GG(s(T28), T29)
hA_in_g(c(s(T8), T9)) → U1_g(T8, T9, pB_in_gg(T8, T9))
pB_in_gg(T8, T9) → U4_gg(T8, T9, fC_in_gg(T8, T9))
fC_in_gg(s(T18), T19) → U2_gg(T18, T19, fC_in_gg(T18, s(T19)))
U2_gg(T18, T19, fC_out_gg(T18, s(T19))) → fC_out_gg(s(T18), T19)
U4_gg(T8, T9, fC_out_gg(T8, T9)) → U5_gg(T8, T9, gD_in_gg(T8, T9))
gD_in_gg(T28, s(T29)) → U3_gg(T28, T29, gD_in_gg(s(T28), T29))
U3_gg(T28, T29, gD_out_gg(s(T28), T29)) → gD_out_gg(T28, s(T29))
U5_gg(T8, T9, gD_out_gg(T8, T9)) → pB_out_gg(T8, T9)
U1_g(T8, T9, pB_out_gg(T8, T9)) → hA_out_g(c(s(T8), T9))
GD_IN_GG(T28, s(T29)) → GD_IN_GG(s(T28), T29)
hA_in_g(c(s(T8), T9)) → U1_g(T8, T9, pB_in_gg(T8, T9))
pB_in_gg(T8, T9) → U4_gg(T8, T9, fC_in_gg(T8, T9))
fC_in_gg(s(T18), T19) → U2_gg(T18, T19, fC_in_gg(T18, s(T19)))
U2_gg(T18, T19, fC_out_gg(T18, s(T19))) → fC_out_gg(s(T18), T19)
U4_gg(T8, T9, fC_out_gg(T8, T9)) → U5_gg(T8, T9, gD_in_gg(T8, T9))
gD_in_gg(T28, s(T29)) → U3_gg(T28, T29, gD_in_gg(s(T28), T29))
U3_gg(T28, T29, gD_out_gg(s(T28), T29)) → gD_out_gg(T28, s(T29))
U5_gg(T8, T9, gD_out_gg(T8, T9)) → pB_out_gg(T8, T9)
U1_g(T8, T9, pB_out_gg(T8, T9)) → hA_out_g(c(s(T8), T9))
GD_IN_GG(T28, s(T29)) → GD_IN_GG(s(T28), T29)
GD_IN_GG(T28, s(T29)) → GD_IN_GG(s(T28), T29)
From the DPs we obtained the following set of size-change graphs:
FC_IN_GG(s(T18), T19) → FC_IN_GG(T18, s(T19))
hA_in_g(c(s(T8), T9)) → U1_g(T8, T9, pB_in_gg(T8, T9))
pB_in_gg(T8, T9) → U4_gg(T8, T9, fC_in_gg(T8, T9))
fC_in_gg(s(T18), T19) → U2_gg(T18, T19, fC_in_gg(T18, s(T19)))
U2_gg(T18, T19, fC_out_gg(T18, s(T19))) → fC_out_gg(s(T18), T19)
U4_gg(T8, T9, fC_out_gg(T8, T9)) → U5_gg(T8, T9, gD_in_gg(T8, T9))
gD_in_gg(T28, s(T29)) → U3_gg(T28, T29, gD_in_gg(s(T28), T29))
U3_gg(T28, T29, gD_out_gg(s(T28), T29)) → gD_out_gg(T28, s(T29))
U5_gg(T8, T9, gD_out_gg(T8, T9)) → pB_out_gg(T8, T9)
U1_g(T8, T9, pB_out_gg(T8, T9)) → hA_out_g(c(s(T8), T9))
FC_IN_GG(s(T18), T19) → FC_IN_GG(T18, s(T19))
FC_IN_GG(s(T18), T19) → FC_IN_GG(T18, s(T19))
From the DPs we obtained the following set of size-change graphs: