0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 54 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 6 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 PiDP
↳7 PiDPToQDPProof (⇔, 15 ms)
↳8 QDP
↳9 QDPSizeChangeProof (⇔, 0 ms)
↳10 YES
bin_treeA_in_g(void) → bin_treeA_out_g(void)
bin_treeA_in_g(tree(T25, T26, T27)) → U1_g(T25, T26, T27, pB_in_gg(T26, T27))
pB_in_gg(T26, T27) → U2_gg(T26, T27, bin_treeA_in_g(T26))
U2_gg(T26, T27, bin_treeA_out_g(T26)) → U3_gg(T26, T27, bin_treeA_in_g(T27))
U3_gg(T26, T27, bin_treeA_out_g(T27)) → pB_out_gg(T26, T27)
U1_g(T25, T26, T27, pB_out_gg(T26, T27)) → bin_treeA_out_g(tree(T25, T26, T27))
BIN_TREEA_IN_G(tree(T25, T26, T27)) → U1_G(T25, T26, T27, pB_in_gg(T26, T27))
BIN_TREEA_IN_G(tree(T25, T26, T27)) → PB_IN_GG(T26, T27)
PB_IN_GG(T26, T27) → U2_GG(T26, T27, bin_treeA_in_g(T26))
PB_IN_GG(T26, T27) → BIN_TREEA_IN_G(T26)
U2_GG(T26, T27, bin_treeA_out_g(T26)) → U3_GG(T26, T27, bin_treeA_in_g(T27))
U2_GG(T26, T27, bin_treeA_out_g(T26)) → BIN_TREEA_IN_G(T27)
bin_treeA_in_g(void) → bin_treeA_out_g(void)
bin_treeA_in_g(tree(T25, T26, T27)) → U1_g(T25, T26, T27, pB_in_gg(T26, T27))
pB_in_gg(T26, T27) → U2_gg(T26, T27, bin_treeA_in_g(T26))
U2_gg(T26, T27, bin_treeA_out_g(T26)) → U3_gg(T26, T27, bin_treeA_in_g(T27))
U3_gg(T26, T27, bin_treeA_out_g(T27)) → pB_out_gg(T26, T27)
U1_g(T25, T26, T27, pB_out_gg(T26, T27)) → bin_treeA_out_g(tree(T25, T26, T27))
BIN_TREEA_IN_G(tree(T25, T26, T27)) → U1_G(T25, T26, T27, pB_in_gg(T26, T27))
BIN_TREEA_IN_G(tree(T25, T26, T27)) → PB_IN_GG(T26, T27)
PB_IN_GG(T26, T27) → U2_GG(T26, T27, bin_treeA_in_g(T26))
PB_IN_GG(T26, T27) → BIN_TREEA_IN_G(T26)
U2_GG(T26, T27, bin_treeA_out_g(T26)) → U3_GG(T26, T27, bin_treeA_in_g(T27))
U2_GG(T26, T27, bin_treeA_out_g(T26)) → BIN_TREEA_IN_G(T27)
bin_treeA_in_g(void) → bin_treeA_out_g(void)
bin_treeA_in_g(tree(T25, T26, T27)) → U1_g(T25, T26, T27, pB_in_gg(T26, T27))
pB_in_gg(T26, T27) → U2_gg(T26, T27, bin_treeA_in_g(T26))
U2_gg(T26, T27, bin_treeA_out_g(T26)) → U3_gg(T26, T27, bin_treeA_in_g(T27))
U3_gg(T26, T27, bin_treeA_out_g(T27)) → pB_out_gg(T26, T27)
U1_g(T25, T26, T27, pB_out_gg(T26, T27)) → bin_treeA_out_g(tree(T25, T26, T27))
BIN_TREEA_IN_G(tree(T25, T26, T27)) → PB_IN_GG(T26, T27)
PB_IN_GG(T26, T27) → U2_GG(T26, T27, bin_treeA_in_g(T26))
U2_GG(T26, T27, bin_treeA_out_g(T26)) → BIN_TREEA_IN_G(T27)
PB_IN_GG(T26, T27) → BIN_TREEA_IN_G(T26)
bin_treeA_in_g(void) → bin_treeA_out_g(void)
bin_treeA_in_g(tree(T25, T26, T27)) → U1_g(T25, T26, T27, pB_in_gg(T26, T27))
pB_in_gg(T26, T27) → U2_gg(T26, T27, bin_treeA_in_g(T26))
U2_gg(T26, T27, bin_treeA_out_g(T26)) → U3_gg(T26, T27, bin_treeA_in_g(T27))
U3_gg(T26, T27, bin_treeA_out_g(T27)) → pB_out_gg(T26, T27)
U1_g(T25, T26, T27, pB_out_gg(T26, T27)) → bin_treeA_out_g(tree(T25, T26, T27))
BIN_TREEA_IN_G(tree(T25, T26, T27)) → PB_IN_GG(T26, T27)
PB_IN_GG(T26, T27) → U2_GG(T26, T27, bin_treeA_in_g(T26))
U2_GG(T26, T27, bin_treeA_out_g(T26)) → BIN_TREEA_IN_G(T27)
PB_IN_GG(T26, T27) → BIN_TREEA_IN_G(T26)
bin_treeA_in_g(void) → bin_treeA_out_g(void)
bin_treeA_in_g(tree(T25, T26, T27)) → U1_g(T25, T26, T27, pB_in_gg(T26, T27))
pB_in_gg(T26, T27) → U2_gg(T26, T27, bin_treeA_in_g(T26))
U2_gg(T26, T27, bin_treeA_out_g(T26)) → U3_gg(T26, T27, bin_treeA_in_g(T27))
U3_gg(T26, T27, bin_treeA_out_g(T27)) → pB_out_gg(T26, T27)
U1_g(T25, T26, T27, pB_out_gg(T26, T27)) → bin_treeA_out_g(tree(T25, T26, T27))
bin_treeA_in_g(x0)
pB_in_gg(x0, x1)
U2_gg(x0, x1, x2)
U3_gg(x0, x1, x2)
U1_g(x0, x1, x2, x3)
From the DPs we obtained the following set of size-change graphs: