0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 141 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 47 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 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 QDPOrderProof (⇔, 81 ms)
↳20 QDP
↳21 DependencyGraphProof (⇔, 0 ms)
↳22 QDP
↳23 UsableRulesProof (⇔, 0 ms)
↳24 QDP
↳25 QReductionProof (⇔, 0 ms)
↳26 QDP
↳27 QDPSizeChangeProof (⇔, 0 ms)
↳28 YES
sameleavesA_in_gg(leaf(T6), leaf(T6)) → sameleavesA_out_gg(leaf(T6), leaf(T6))
sameleavesA_in_gg(tree(T11, T12), tree(T13, T14)) → U1_gg(T11, T12, T13, T14, pB_in_ggaagga(T11, T12, X15, X16, T13, T14, X17))
pB_in_ggaagga(leaf(T23), T24, T23, T24, T13, T14, X17) → U3_ggaagga(T23, T24, T13, T14, X17, pD_in_gggag(T13, T14, T23, X17, T24))
pD_in_gggag(T13, T14, T23, T29, T24) → U5_gggag(T13, T14, T23, T29, T24, getleaveC_in_ggga(T13, T14, T23, T29))
getleaveC_in_ggga(leaf(T42), T43, T42, T43) → getleaveC_out_ggga(leaf(T42), T43, T42, T43)
getleaveC_in_ggga(tree(T52, T53), T54, T55, X63) → U2_ggga(T52, T53, T54, T55, X63, getleaveC_in_ggga(T52, tree(T53, T54), T55, X63))
U2_ggga(T52, T53, T54, T55, X63, getleaveC_out_ggga(T52, tree(T53, T54), T55, X63)) → getleaveC_out_ggga(tree(T52, T53), T54, T55, X63)
U5_gggag(T13, T14, T23, T29, T24, getleaveC_out_ggga(T13, T14, T23, T29)) → U6_gggag(T13, T14, T23, T29, T24, sameleavesA_in_gg(T24, T29))
U6_gggag(T13, T14, T23, T29, T24, sameleavesA_out_gg(T24, T29)) → pD_out_gggag(T13, T14, T23, T29, T24)
U3_ggaagga(T23, T24, T13, T14, X17, pD_out_gggag(T13, T14, T23, X17, T24)) → pB_out_ggaagga(leaf(T23), T24, T23, T24, T13, T14, X17)
pB_in_ggaagga(tree(T70, T71), T72, X89, X90, T13, T14, X17) → U4_ggaagga(T70, T71, T72, X89, X90, T13, T14, X17, pB_in_ggaagga(T70, tree(T71, T72), X89, X90, T13, T14, X17))
U4_ggaagga(T70, T71, T72, X89, X90, T13, T14, X17, pB_out_ggaagga(T70, tree(T71, T72), X89, X90, T13, T14, X17)) → pB_out_ggaagga(tree(T70, T71), T72, X89, X90, T13, T14, X17)
U1_gg(T11, T12, T13, T14, pB_out_ggaagga(T11, T12, X15, X16, T13, T14, X17)) → sameleavesA_out_gg(tree(T11, T12), tree(T13, T14))
SAMELEAVESA_IN_GG(tree(T11, T12), tree(T13, T14)) → U1_GG(T11, T12, T13, T14, pB_in_ggaagga(T11, T12, X15, X16, T13, T14, X17))
SAMELEAVESA_IN_GG(tree(T11, T12), tree(T13, T14)) → PB_IN_GGAAGGA(T11, T12, X15, X16, T13, T14, X17)
PB_IN_GGAAGGA(leaf(T23), T24, T23, T24, T13, T14, X17) → U3_GGAAGGA(T23, T24, T13, T14, X17, pD_in_gggag(T13, T14, T23, X17, T24))
PB_IN_GGAAGGA(leaf(T23), T24, T23, T24, T13, T14, X17) → PD_IN_GGGAG(T13, T14, T23, X17, T24)
PD_IN_GGGAG(T13, T14, T23, T29, T24) → U5_GGGAG(T13, T14, T23, T29, T24, getleaveC_in_ggga(T13, T14, T23, T29))
PD_IN_GGGAG(T13, T14, T23, T29, T24) → GETLEAVEC_IN_GGGA(T13, T14, T23, T29)
GETLEAVEC_IN_GGGA(tree(T52, T53), T54, T55, X63) → U2_GGGA(T52, T53, T54, T55, X63, getleaveC_in_ggga(T52, tree(T53, T54), T55, X63))
GETLEAVEC_IN_GGGA(tree(T52, T53), T54, T55, X63) → GETLEAVEC_IN_GGGA(T52, tree(T53, T54), T55, X63)
U5_GGGAG(T13, T14, T23, T29, T24, getleaveC_out_ggga(T13, T14, T23, T29)) → U6_GGGAG(T13, T14, T23, T29, T24, sameleavesA_in_gg(T24, T29))
U5_GGGAG(T13, T14, T23, T29, T24, getleaveC_out_ggga(T13, T14, T23, T29)) → SAMELEAVESA_IN_GG(T24, T29)
PB_IN_GGAAGGA(tree(T70, T71), T72, X89, X90, T13, T14, X17) → U4_GGAAGGA(T70, T71, T72, X89, X90, T13, T14, X17, pB_in_ggaagga(T70, tree(T71, T72), X89, X90, T13, T14, X17))
PB_IN_GGAAGGA(tree(T70, T71), T72, X89, X90, T13, T14, X17) → PB_IN_GGAAGGA(T70, tree(T71, T72), X89, X90, T13, T14, X17)
sameleavesA_in_gg(leaf(T6), leaf(T6)) → sameleavesA_out_gg(leaf(T6), leaf(T6))
sameleavesA_in_gg(tree(T11, T12), tree(T13, T14)) → U1_gg(T11, T12, T13, T14, pB_in_ggaagga(T11, T12, X15, X16, T13, T14, X17))
pB_in_ggaagga(leaf(T23), T24, T23, T24, T13, T14, X17) → U3_ggaagga(T23, T24, T13, T14, X17, pD_in_gggag(T13, T14, T23, X17, T24))
pD_in_gggag(T13, T14, T23, T29, T24) → U5_gggag(T13, T14, T23, T29, T24, getleaveC_in_ggga(T13, T14, T23, T29))
getleaveC_in_ggga(leaf(T42), T43, T42, T43) → getleaveC_out_ggga(leaf(T42), T43, T42, T43)
getleaveC_in_ggga(tree(T52, T53), T54, T55, X63) → U2_ggga(T52, T53, T54, T55, X63, getleaveC_in_ggga(T52, tree(T53, T54), T55, X63))
U2_ggga(T52, T53, T54, T55, X63, getleaveC_out_ggga(T52, tree(T53, T54), T55, X63)) → getleaveC_out_ggga(tree(T52, T53), T54, T55, X63)
U5_gggag(T13, T14, T23, T29, T24, getleaveC_out_ggga(T13, T14, T23, T29)) → U6_gggag(T13, T14, T23, T29, T24, sameleavesA_in_gg(T24, T29))
U6_gggag(T13, T14, T23, T29, T24, sameleavesA_out_gg(T24, T29)) → pD_out_gggag(T13, T14, T23, T29, T24)
U3_ggaagga(T23, T24, T13, T14, X17, pD_out_gggag(T13, T14, T23, X17, T24)) → pB_out_ggaagga(leaf(T23), T24, T23, T24, T13, T14, X17)
pB_in_ggaagga(tree(T70, T71), T72, X89, X90, T13, T14, X17) → U4_ggaagga(T70, T71, T72, X89, X90, T13, T14, X17, pB_in_ggaagga(T70, tree(T71, T72), X89, X90, T13, T14, X17))
U4_ggaagga(T70, T71, T72, X89, X90, T13, T14, X17, pB_out_ggaagga(T70, tree(T71, T72), X89, X90, T13, T14, X17)) → pB_out_ggaagga(tree(T70, T71), T72, X89, X90, T13, T14, X17)
U1_gg(T11, T12, T13, T14, pB_out_ggaagga(T11, T12, X15, X16, T13, T14, X17)) → sameleavesA_out_gg(tree(T11, T12), tree(T13, T14))
SAMELEAVESA_IN_GG(tree(T11, T12), tree(T13, T14)) → U1_GG(T11, T12, T13, T14, pB_in_ggaagga(T11, T12, X15, X16, T13, T14, X17))
SAMELEAVESA_IN_GG(tree(T11, T12), tree(T13, T14)) → PB_IN_GGAAGGA(T11, T12, X15, X16, T13, T14, X17)
PB_IN_GGAAGGA(leaf(T23), T24, T23, T24, T13, T14, X17) → U3_GGAAGGA(T23, T24, T13, T14, X17, pD_in_gggag(T13, T14, T23, X17, T24))
PB_IN_GGAAGGA(leaf(T23), T24, T23, T24, T13, T14, X17) → PD_IN_GGGAG(T13, T14, T23, X17, T24)
PD_IN_GGGAG(T13, T14, T23, T29, T24) → U5_GGGAG(T13, T14, T23, T29, T24, getleaveC_in_ggga(T13, T14, T23, T29))
PD_IN_GGGAG(T13, T14, T23, T29, T24) → GETLEAVEC_IN_GGGA(T13, T14, T23, T29)
GETLEAVEC_IN_GGGA(tree(T52, T53), T54, T55, X63) → U2_GGGA(T52, T53, T54, T55, X63, getleaveC_in_ggga(T52, tree(T53, T54), T55, X63))
GETLEAVEC_IN_GGGA(tree(T52, T53), T54, T55, X63) → GETLEAVEC_IN_GGGA(T52, tree(T53, T54), T55, X63)
U5_GGGAG(T13, T14, T23, T29, T24, getleaveC_out_ggga(T13, T14, T23, T29)) → U6_GGGAG(T13, T14, T23, T29, T24, sameleavesA_in_gg(T24, T29))
U5_GGGAG(T13, T14, T23, T29, T24, getleaveC_out_ggga(T13, T14, T23, T29)) → SAMELEAVESA_IN_GG(T24, T29)
PB_IN_GGAAGGA(tree(T70, T71), T72, X89, X90, T13, T14, X17) → U4_GGAAGGA(T70, T71, T72, X89, X90, T13, T14, X17, pB_in_ggaagga(T70, tree(T71, T72), X89, X90, T13, T14, X17))
PB_IN_GGAAGGA(tree(T70, T71), T72, X89, X90, T13, T14, X17) → PB_IN_GGAAGGA(T70, tree(T71, T72), X89, X90, T13, T14, X17)
sameleavesA_in_gg(leaf(T6), leaf(T6)) → sameleavesA_out_gg(leaf(T6), leaf(T6))
sameleavesA_in_gg(tree(T11, T12), tree(T13, T14)) → U1_gg(T11, T12, T13, T14, pB_in_ggaagga(T11, T12, X15, X16, T13, T14, X17))
pB_in_ggaagga(leaf(T23), T24, T23, T24, T13, T14, X17) → U3_ggaagga(T23, T24, T13, T14, X17, pD_in_gggag(T13, T14, T23, X17, T24))
pD_in_gggag(T13, T14, T23, T29, T24) → U5_gggag(T13, T14, T23, T29, T24, getleaveC_in_ggga(T13, T14, T23, T29))
getleaveC_in_ggga(leaf(T42), T43, T42, T43) → getleaveC_out_ggga(leaf(T42), T43, T42, T43)
getleaveC_in_ggga(tree(T52, T53), T54, T55, X63) → U2_ggga(T52, T53, T54, T55, X63, getleaveC_in_ggga(T52, tree(T53, T54), T55, X63))
U2_ggga(T52, T53, T54, T55, X63, getleaveC_out_ggga(T52, tree(T53, T54), T55, X63)) → getleaveC_out_ggga(tree(T52, T53), T54, T55, X63)
U5_gggag(T13, T14, T23, T29, T24, getleaveC_out_ggga(T13, T14, T23, T29)) → U6_gggag(T13, T14, T23, T29, T24, sameleavesA_in_gg(T24, T29))
U6_gggag(T13, T14, T23, T29, T24, sameleavesA_out_gg(T24, T29)) → pD_out_gggag(T13, T14, T23, T29, T24)
U3_ggaagga(T23, T24, T13, T14, X17, pD_out_gggag(T13, T14, T23, X17, T24)) → pB_out_ggaagga(leaf(T23), T24, T23, T24, T13, T14, X17)
pB_in_ggaagga(tree(T70, T71), T72, X89, X90, T13, T14, X17) → U4_ggaagga(T70, T71, T72, X89, X90, T13, T14, X17, pB_in_ggaagga(T70, tree(T71, T72), X89, X90, T13, T14, X17))
U4_ggaagga(T70, T71, T72, X89, X90, T13, T14, X17, pB_out_ggaagga(T70, tree(T71, T72), X89, X90, T13, T14, X17)) → pB_out_ggaagga(tree(T70, T71), T72, X89, X90, T13, T14, X17)
U1_gg(T11, T12, T13, T14, pB_out_ggaagga(T11, T12, X15, X16, T13, T14, X17)) → sameleavesA_out_gg(tree(T11, T12), tree(T13, T14))
GETLEAVEC_IN_GGGA(tree(T52, T53), T54, T55, X63) → GETLEAVEC_IN_GGGA(T52, tree(T53, T54), T55, X63)
sameleavesA_in_gg(leaf(T6), leaf(T6)) → sameleavesA_out_gg(leaf(T6), leaf(T6))
sameleavesA_in_gg(tree(T11, T12), tree(T13, T14)) → U1_gg(T11, T12, T13, T14, pB_in_ggaagga(T11, T12, X15, X16, T13, T14, X17))
pB_in_ggaagga(leaf(T23), T24, T23, T24, T13, T14, X17) → U3_ggaagga(T23, T24, T13, T14, X17, pD_in_gggag(T13, T14, T23, X17, T24))
pD_in_gggag(T13, T14, T23, T29, T24) → U5_gggag(T13, T14, T23, T29, T24, getleaveC_in_ggga(T13, T14, T23, T29))
getleaveC_in_ggga(leaf(T42), T43, T42, T43) → getleaveC_out_ggga(leaf(T42), T43, T42, T43)
getleaveC_in_ggga(tree(T52, T53), T54, T55, X63) → U2_ggga(T52, T53, T54, T55, X63, getleaveC_in_ggga(T52, tree(T53, T54), T55, X63))
U2_ggga(T52, T53, T54, T55, X63, getleaveC_out_ggga(T52, tree(T53, T54), T55, X63)) → getleaveC_out_ggga(tree(T52, T53), T54, T55, X63)
U5_gggag(T13, T14, T23, T29, T24, getleaveC_out_ggga(T13, T14, T23, T29)) → U6_gggag(T13, T14, T23, T29, T24, sameleavesA_in_gg(T24, T29))
U6_gggag(T13, T14, T23, T29, T24, sameleavesA_out_gg(T24, T29)) → pD_out_gggag(T13, T14, T23, T29, T24)
U3_ggaagga(T23, T24, T13, T14, X17, pD_out_gggag(T13, T14, T23, X17, T24)) → pB_out_ggaagga(leaf(T23), T24, T23, T24, T13, T14, X17)
pB_in_ggaagga(tree(T70, T71), T72, X89, X90, T13, T14, X17) → U4_ggaagga(T70, T71, T72, X89, X90, T13, T14, X17, pB_in_ggaagga(T70, tree(T71, T72), X89, X90, T13, T14, X17))
U4_ggaagga(T70, T71, T72, X89, X90, T13, T14, X17, pB_out_ggaagga(T70, tree(T71, T72), X89, X90, T13, T14, X17)) → pB_out_ggaagga(tree(T70, T71), T72, X89, X90, T13, T14, X17)
U1_gg(T11, T12, T13, T14, pB_out_ggaagga(T11, T12, X15, X16, T13, T14, X17)) → sameleavesA_out_gg(tree(T11, T12), tree(T13, T14))
GETLEAVEC_IN_GGGA(tree(T52, T53), T54, T55, X63) → GETLEAVEC_IN_GGGA(T52, tree(T53, T54), T55, X63)
GETLEAVEC_IN_GGGA(tree(T52, T53), T54, T55) → GETLEAVEC_IN_GGGA(T52, tree(T53, T54), T55)
From the DPs we obtained the following set of size-change graphs:
SAMELEAVESA_IN_GG(tree(T11, T12), tree(T13, T14)) → PB_IN_GGAAGGA(T11, T12, X15, X16, T13, T14, X17)
PB_IN_GGAAGGA(leaf(T23), T24, T23, T24, T13, T14, X17) → PD_IN_GGGAG(T13, T14, T23, X17, T24)
PD_IN_GGGAG(T13, T14, T23, T29, T24) → U5_GGGAG(T13, T14, T23, T29, T24, getleaveC_in_ggga(T13, T14, T23, T29))
U5_GGGAG(T13, T14, T23, T29, T24, getleaveC_out_ggga(T13, T14, T23, T29)) → SAMELEAVESA_IN_GG(T24, T29)
PB_IN_GGAAGGA(tree(T70, T71), T72, X89, X90, T13, T14, X17) → PB_IN_GGAAGGA(T70, tree(T71, T72), X89, X90, T13, T14, X17)
sameleavesA_in_gg(leaf(T6), leaf(T6)) → sameleavesA_out_gg(leaf(T6), leaf(T6))
sameleavesA_in_gg(tree(T11, T12), tree(T13, T14)) → U1_gg(T11, T12, T13, T14, pB_in_ggaagga(T11, T12, X15, X16, T13, T14, X17))
pB_in_ggaagga(leaf(T23), T24, T23, T24, T13, T14, X17) → U3_ggaagga(T23, T24, T13, T14, X17, pD_in_gggag(T13, T14, T23, X17, T24))
pD_in_gggag(T13, T14, T23, T29, T24) → U5_gggag(T13, T14, T23, T29, T24, getleaveC_in_ggga(T13, T14, T23, T29))
getleaveC_in_ggga(leaf(T42), T43, T42, T43) → getleaveC_out_ggga(leaf(T42), T43, T42, T43)
getleaveC_in_ggga(tree(T52, T53), T54, T55, X63) → U2_ggga(T52, T53, T54, T55, X63, getleaveC_in_ggga(T52, tree(T53, T54), T55, X63))
U2_ggga(T52, T53, T54, T55, X63, getleaveC_out_ggga(T52, tree(T53, T54), T55, X63)) → getleaveC_out_ggga(tree(T52, T53), T54, T55, X63)
U5_gggag(T13, T14, T23, T29, T24, getleaveC_out_ggga(T13, T14, T23, T29)) → U6_gggag(T13, T14, T23, T29, T24, sameleavesA_in_gg(T24, T29))
U6_gggag(T13, T14, T23, T29, T24, sameleavesA_out_gg(T24, T29)) → pD_out_gggag(T13, T14, T23, T29, T24)
U3_ggaagga(T23, T24, T13, T14, X17, pD_out_gggag(T13, T14, T23, X17, T24)) → pB_out_ggaagga(leaf(T23), T24, T23, T24, T13, T14, X17)
pB_in_ggaagga(tree(T70, T71), T72, X89, X90, T13, T14, X17) → U4_ggaagga(T70, T71, T72, X89, X90, T13, T14, X17, pB_in_ggaagga(T70, tree(T71, T72), X89, X90, T13, T14, X17))
U4_ggaagga(T70, T71, T72, X89, X90, T13, T14, X17, pB_out_ggaagga(T70, tree(T71, T72), X89, X90, T13, T14, X17)) → pB_out_ggaagga(tree(T70, T71), T72, X89, X90, T13, T14, X17)
U1_gg(T11, T12, T13, T14, pB_out_ggaagga(T11, T12, X15, X16, T13, T14, X17)) → sameleavesA_out_gg(tree(T11, T12), tree(T13, T14))
SAMELEAVESA_IN_GG(tree(T11, T12), tree(T13, T14)) → PB_IN_GGAAGGA(T11, T12, X15, X16, T13, T14, X17)
PB_IN_GGAAGGA(leaf(T23), T24, T23, T24, T13, T14, X17) → PD_IN_GGGAG(T13, T14, T23, X17, T24)
PD_IN_GGGAG(T13, T14, T23, T29, T24) → U5_GGGAG(T13, T14, T23, T29, T24, getleaveC_in_ggga(T13, T14, T23, T29))
U5_GGGAG(T13, T14, T23, T29, T24, getleaveC_out_ggga(T13, T14, T23, T29)) → SAMELEAVESA_IN_GG(T24, T29)
PB_IN_GGAAGGA(tree(T70, T71), T72, X89, X90, T13, T14, X17) → PB_IN_GGAAGGA(T70, tree(T71, T72), X89, X90, T13, T14, X17)
getleaveC_in_ggga(leaf(T42), T43, T42, T43) → getleaveC_out_ggga(leaf(T42), T43, T42, T43)
getleaveC_in_ggga(tree(T52, T53), T54, T55, X63) → U2_ggga(T52, T53, T54, T55, X63, getleaveC_in_ggga(T52, tree(T53, T54), T55, X63))
U2_ggga(T52, T53, T54, T55, X63, getleaveC_out_ggga(T52, tree(T53, T54), T55, X63)) → getleaveC_out_ggga(tree(T52, T53), T54, T55, X63)
SAMELEAVESA_IN_GG(tree(T11, T12), tree(T13, T14)) → PB_IN_GGAAGGA(T11, T12, T13, T14)
PB_IN_GGAAGGA(leaf(T23), T24, T13, T14) → PD_IN_GGGAG(T13, T14, T23, T24)
PD_IN_GGGAG(T13, T14, T23, T24) → U5_GGGAG(T13, T14, T23, T24, getleaveC_in_ggga(T13, T14, T23))
U5_GGGAG(T13, T14, T23, T24, getleaveC_out_ggga(T13, T14, T23, T29)) → SAMELEAVESA_IN_GG(T24, T29)
PB_IN_GGAAGGA(tree(T70, T71), T72, T13, T14) → PB_IN_GGAAGGA(T70, tree(T71, T72), T13, T14)
getleaveC_in_ggga(leaf(T42), T43, T42) → getleaveC_out_ggga(leaf(T42), T43, T42, T43)
getleaveC_in_ggga(tree(T52, T53), T54, T55) → U2_ggga(T52, T53, T54, T55, getleaveC_in_ggga(T52, tree(T53, T54), T55))
U2_ggga(T52, T53, T54, T55, getleaveC_out_ggga(T52, tree(T53, T54), T55, X63)) → getleaveC_out_ggga(tree(T52, T53), T54, T55, X63)
getleaveC_in_ggga(x0, x1, x2)
U2_ggga(x0, x1, x2, x3, x4)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
U5_GGGAG(T13, T14, T23, T24, getleaveC_out_ggga(T13, T14, T23, T29)) → SAMELEAVESA_IN_GG(T24, T29)
POL(PB_IN_GGAAGGA(x1, x2, x3, x4)) = x1 + x2
POL(PD_IN_GGGAG(x1, x2, x3, x4)) = 1 + x3 + x4
POL(SAMELEAVESA_IN_GG(x1, x2)) = x1
POL(U2_ggga(x1, x2, x3, x4, x5)) = 0
POL(U5_GGGAG(x1, x2, x3, x4, x5)) = 1 + x3 + x4
POL(getleaveC_in_ggga(x1, x2, x3)) = 0
POL(getleaveC_out_ggga(x1, x2, x3, x4)) = 0
POL(leaf(x1)) = 1 + x1
POL(tree(x1, x2)) = x1 + x2
SAMELEAVESA_IN_GG(tree(T11, T12), tree(T13, T14)) → PB_IN_GGAAGGA(T11, T12, T13, T14)
PB_IN_GGAAGGA(leaf(T23), T24, T13, T14) → PD_IN_GGGAG(T13, T14, T23, T24)
PD_IN_GGGAG(T13, T14, T23, T24) → U5_GGGAG(T13, T14, T23, T24, getleaveC_in_ggga(T13, T14, T23))
PB_IN_GGAAGGA(tree(T70, T71), T72, T13, T14) → PB_IN_GGAAGGA(T70, tree(T71, T72), T13, T14)
getleaveC_in_ggga(leaf(T42), T43, T42) → getleaveC_out_ggga(leaf(T42), T43, T42, T43)
getleaveC_in_ggga(tree(T52, T53), T54, T55) → U2_ggga(T52, T53, T54, T55, getleaveC_in_ggga(T52, tree(T53, T54), T55))
U2_ggga(T52, T53, T54, T55, getleaveC_out_ggga(T52, tree(T53, T54), T55, X63)) → getleaveC_out_ggga(tree(T52, T53), T54, T55, X63)
getleaveC_in_ggga(x0, x1, x2)
U2_ggga(x0, x1, x2, x3, x4)
PB_IN_GGAAGGA(tree(T70, T71), T72, T13, T14) → PB_IN_GGAAGGA(T70, tree(T71, T72), T13, T14)
getleaveC_in_ggga(leaf(T42), T43, T42) → getleaveC_out_ggga(leaf(T42), T43, T42, T43)
getleaveC_in_ggga(tree(T52, T53), T54, T55) → U2_ggga(T52, T53, T54, T55, getleaveC_in_ggga(T52, tree(T53, T54), T55))
U2_ggga(T52, T53, T54, T55, getleaveC_out_ggga(T52, tree(T53, T54), T55, X63)) → getleaveC_out_ggga(tree(T52, T53), T54, T55, X63)
getleaveC_in_ggga(x0, x1, x2)
U2_ggga(x0, x1, x2, x3, x4)
PB_IN_GGAAGGA(tree(T70, T71), T72, T13, T14) → PB_IN_GGAAGGA(T70, tree(T71, T72), T13, T14)
getleaveC_in_ggga(x0, x1, x2)
U2_ggga(x0, x1, x2, x3, x4)
getleaveC_in_ggga(x0, x1, x2)
U2_ggga(x0, x1, x2, x3, x4)
PB_IN_GGAAGGA(tree(T70, T71), T72, T13, T14) → PB_IN_GGAAGGA(T70, tree(T71, T72), T13, T14)
From the DPs we obtained the following set of size-change graphs: