0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 68 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 13 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 (⇔, 77 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
samefringeA_in_gg(nil, nil) → samefringeA_out_gg(nil, nil)
samefringeA_in_gg(cons(T7, T8), cons(T9, T10)) → U1_gg(T7, T8, T9, T10, pB_in_ggaaggaa(T7, T8, X14, X15, T9, T10, X16, X17))
pB_in_ggaaggaa(nil, T15, nil, T15, T9, T10, X16, X17) → U3_ggaaggaa(T15, T9, T10, X16, X17, pD_in_ggaag(T9, T10, X16, X17, T15))
pD_in_ggaag(T9, T10, T16, T17, T15) → U5_ggaag(T9, T10, T16, T17, T15, gopherC_in_ggaa(T9, T10, T16, T17))
gopherC_in_ggaa(nil, T22, nil, T22) → gopherC_out_ggaa(nil, T22, nil, T22)
gopherC_in_ggaa(cons(T29, T30), T31, X44, X45) → U2_ggaa(T29, T30, T31, X44, X45, gopherC_in_ggaa(T29, cons(T30, T31), X44, X45))
U2_ggaa(T29, T30, T31, X44, X45, gopherC_out_ggaa(T29, cons(T30, T31), X44, X45)) → gopherC_out_ggaa(cons(T29, T30), T31, X44, X45)
U5_ggaag(T9, T10, T16, T17, T15, gopherC_out_ggaa(T9, T10, T16, T17)) → U6_ggaag(T9, T10, T16, T17, T15, samefringeA_in_gg(T15, T17))
U6_ggaag(T9, T10, T16, T17, T15, samefringeA_out_gg(T15, T17)) → pD_out_ggaag(T9, T10, T16, T17, T15)
U3_ggaaggaa(T15, T9, T10, X16, X17, pD_out_ggaag(T9, T10, X16, X17, T15)) → pB_out_ggaaggaa(nil, T15, nil, T15, T9, T10, X16, X17)
pB_in_ggaaggaa(cons(T38, T39), T40, X62, X63, T9, T10, X16, X17) → U4_ggaaggaa(T38, T39, T40, X62, X63, T9, T10, X16, X17, pB_in_ggaaggaa(T38, cons(T39, T40), X62, X63, T9, T10, X16, X17))
U4_ggaaggaa(T38, T39, T40, X62, X63, T9, T10, X16, X17, pB_out_ggaaggaa(T38, cons(T39, T40), X62, X63, T9, T10, X16, X17)) → pB_out_ggaaggaa(cons(T38, T39), T40, X62, X63, T9, T10, X16, X17)
U1_gg(T7, T8, T9, T10, pB_out_ggaaggaa(T7, T8, X14, X15, T9, T10, X16, X17)) → samefringeA_out_gg(cons(T7, T8), cons(T9, T10))
SAMEFRINGEA_IN_GG(cons(T7, T8), cons(T9, T10)) → U1_GG(T7, T8, T9, T10, pB_in_ggaaggaa(T7, T8, X14, X15, T9, T10, X16, X17))
SAMEFRINGEA_IN_GG(cons(T7, T8), cons(T9, T10)) → PB_IN_GGAAGGAA(T7, T8, X14, X15, T9, T10, X16, X17)
PB_IN_GGAAGGAA(nil, T15, nil, T15, T9, T10, X16, X17) → U3_GGAAGGAA(T15, T9, T10, X16, X17, pD_in_ggaag(T9, T10, X16, X17, T15))
PB_IN_GGAAGGAA(nil, T15, nil, T15, T9, T10, X16, X17) → PD_IN_GGAAG(T9, T10, X16, X17, T15)
PD_IN_GGAAG(T9, T10, T16, T17, T15) → U5_GGAAG(T9, T10, T16, T17, T15, gopherC_in_ggaa(T9, T10, T16, T17))
PD_IN_GGAAG(T9, T10, T16, T17, T15) → GOPHERC_IN_GGAA(T9, T10, T16, T17)
GOPHERC_IN_GGAA(cons(T29, T30), T31, X44, X45) → U2_GGAA(T29, T30, T31, X44, X45, gopherC_in_ggaa(T29, cons(T30, T31), X44, X45))
GOPHERC_IN_GGAA(cons(T29, T30), T31, X44, X45) → GOPHERC_IN_GGAA(T29, cons(T30, T31), X44, X45)
U5_GGAAG(T9, T10, T16, T17, T15, gopherC_out_ggaa(T9, T10, T16, T17)) → U6_GGAAG(T9, T10, T16, T17, T15, samefringeA_in_gg(T15, T17))
U5_GGAAG(T9, T10, T16, T17, T15, gopherC_out_ggaa(T9, T10, T16, T17)) → SAMEFRINGEA_IN_GG(T15, T17)
PB_IN_GGAAGGAA(cons(T38, T39), T40, X62, X63, T9, T10, X16, X17) → U4_GGAAGGAA(T38, T39, T40, X62, X63, T9, T10, X16, X17, pB_in_ggaaggaa(T38, cons(T39, T40), X62, X63, T9, T10, X16, X17))
PB_IN_GGAAGGAA(cons(T38, T39), T40, X62, X63, T9, T10, X16, X17) → PB_IN_GGAAGGAA(T38, cons(T39, T40), X62, X63, T9, T10, X16, X17)
samefringeA_in_gg(nil, nil) → samefringeA_out_gg(nil, nil)
samefringeA_in_gg(cons(T7, T8), cons(T9, T10)) → U1_gg(T7, T8, T9, T10, pB_in_ggaaggaa(T7, T8, X14, X15, T9, T10, X16, X17))
pB_in_ggaaggaa(nil, T15, nil, T15, T9, T10, X16, X17) → U3_ggaaggaa(T15, T9, T10, X16, X17, pD_in_ggaag(T9, T10, X16, X17, T15))
pD_in_ggaag(T9, T10, T16, T17, T15) → U5_ggaag(T9, T10, T16, T17, T15, gopherC_in_ggaa(T9, T10, T16, T17))
gopherC_in_ggaa(nil, T22, nil, T22) → gopherC_out_ggaa(nil, T22, nil, T22)
gopherC_in_ggaa(cons(T29, T30), T31, X44, X45) → U2_ggaa(T29, T30, T31, X44, X45, gopherC_in_ggaa(T29, cons(T30, T31), X44, X45))
U2_ggaa(T29, T30, T31, X44, X45, gopherC_out_ggaa(T29, cons(T30, T31), X44, X45)) → gopherC_out_ggaa(cons(T29, T30), T31, X44, X45)
U5_ggaag(T9, T10, T16, T17, T15, gopherC_out_ggaa(T9, T10, T16, T17)) → U6_ggaag(T9, T10, T16, T17, T15, samefringeA_in_gg(T15, T17))
U6_ggaag(T9, T10, T16, T17, T15, samefringeA_out_gg(T15, T17)) → pD_out_ggaag(T9, T10, T16, T17, T15)
U3_ggaaggaa(T15, T9, T10, X16, X17, pD_out_ggaag(T9, T10, X16, X17, T15)) → pB_out_ggaaggaa(nil, T15, nil, T15, T9, T10, X16, X17)
pB_in_ggaaggaa(cons(T38, T39), T40, X62, X63, T9, T10, X16, X17) → U4_ggaaggaa(T38, T39, T40, X62, X63, T9, T10, X16, X17, pB_in_ggaaggaa(T38, cons(T39, T40), X62, X63, T9, T10, X16, X17))
U4_ggaaggaa(T38, T39, T40, X62, X63, T9, T10, X16, X17, pB_out_ggaaggaa(T38, cons(T39, T40), X62, X63, T9, T10, X16, X17)) → pB_out_ggaaggaa(cons(T38, T39), T40, X62, X63, T9, T10, X16, X17)
U1_gg(T7, T8, T9, T10, pB_out_ggaaggaa(T7, T8, X14, X15, T9, T10, X16, X17)) → samefringeA_out_gg(cons(T7, T8), cons(T9, T10))
SAMEFRINGEA_IN_GG(cons(T7, T8), cons(T9, T10)) → U1_GG(T7, T8, T9, T10, pB_in_ggaaggaa(T7, T8, X14, X15, T9, T10, X16, X17))
SAMEFRINGEA_IN_GG(cons(T7, T8), cons(T9, T10)) → PB_IN_GGAAGGAA(T7, T8, X14, X15, T9, T10, X16, X17)
PB_IN_GGAAGGAA(nil, T15, nil, T15, T9, T10, X16, X17) → U3_GGAAGGAA(T15, T9, T10, X16, X17, pD_in_ggaag(T9, T10, X16, X17, T15))
PB_IN_GGAAGGAA(nil, T15, nil, T15, T9, T10, X16, X17) → PD_IN_GGAAG(T9, T10, X16, X17, T15)
PD_IN_GGAAG(T9, T10, T16, T17, T15) → U5_GGAAG(T9, T10, T16, T17, T15, gopherC_in_ggaa(T9, T10, T16, T17))
PD_IN_GGAAG(T9, T10, T16, T17, T15) → GOPHERC_IN_GGAA(T9, T10, T16, T17)
GOPHERC_IN_GGAA(cons(T29, T30), T31, X44, X45) → U2_GGAA(T29, T30, T31, X44, X45, gopherC_in_ggaa(T29, cons(T30, T31), X44, X45))
GOPHERC_IN_GGAA(cons(T29, T30), T31, X44, X45) → GOPHERC_IN_GGAA(T29, cons(T30, T31), X44, X45)
U5_GGAAG(T9, T10, T16, T17, T15, gopherC_out_ggaa(T9, T10, T16, T17)) → U6_GGAAG(T9, T10, T16, T17, T15, samefringeA_in_gg(T15, T17))
U5_GGAAG(T9, T10, T16, T17, T15, gopherC_out_ggaa(T9, T10, T16, T17)) → SAMEFRINGEA_IN_GG(T15, T17)
PB_IN_GGAAGGAA(cons(T38, T39), T40, X62, X63, T9, T10, X16, X17) → U4_GGAAGGAA(T38, T39, T40, X62, X63, T9, T10, X16, X17, pB_in_ggaaggaa(T38, cons(T39, T40), X62, X63, T9, T10, X16, X17))
PB_IN_GGAAGGAA(cons(T38, T39), T40, X62, X63, T9, T10, X16, X17) → PB_IN_GGAAGGAA(T38, cons(T39, T40), X62, X63, T9, T10, X16, X17)
samefringeA_in_gg(nil, nil) → samefringeA_out_gg(nil, nil)
samefringeA_in_gg(cons(T7, T8), cons(T9, T10)) → U1_gg(T7, T8, T9, T10, pB_in_ggaaggaa(T7, T8, X14, X15, T9, T10, X16, X17))
pB_in_ggaaggaa(nil, T15, nil, T15, T9, T10, X16, X17) → U3_ggaaggaa(T15, T9, T10, X16, X17, pD_in_ggaag(T9, T10, X16, X17, T15))
pD_in_ggaag(T9, T10, T16, T17, T15) → U5_ggaag(T9, T10, T16, T17, T15, gopherC_in_ggaa(T9, T10, T16, T17))
gopherC_in_ggaa(nil, T22, nil, T22) → gopherC_out_ggaa(nil, T22, nil, T22)
gopherC_in_ggaa(cons(T29, T30), T31, X44, X45) → U2_ggaa(T29, T30, T31, X44, X45, gopherC_in_ggaa(T29, cons(T30, T31), X44, X45))
U2_ggaa(T29, T30, T31, X44, X45, gopherC_out_ggaa(T29, cons(T30, T31), X44, X45)) → gopherC_out_ggaa(cons(T29, T30), T31, X44, X45)
U5_ggaag(T9, T10, T16, T17, T15, gopherC_out_ggaa(T9, T10, T16, T17)) → U6_ggaag(T9, T10, T16, T17, T15, samefringeA_in_gg(T15, T17))
U6_ggaag(T9, T10, T16, T17, T15, samefringeA_out_gg(T15, T17)) → pD_out_ggaag(T9, T10, T16, T17, T15)
U3_ggaaggaa(T15, T9, T10, X16, X17, pD_out_ggaag(T9, T10, X16, X17, T15)) → pB_out_ggaaggaa(nil, T15, nil, T15, T9, T10, X16, X17)
pB_in_ggaaggaa(cons(T38, T39), T40, X62, X63, T9, T10, X16, X17) → U4_ggaaggaa(T38, T39, T40, X62, X63, T9, T10, X16, X17, pB_in_ggaaggaa(T38, cons(T39, T40), X62, X63, T9, T10, X16, X17))
U4_ggaaggaa(T38, T39, T40, X62, X63, T9, T10, X16, X17, pB_out_ggaaggaa(T38, cons(T39, T40), X62, X63, T9, T10, X16, X17)) → pB_out_ggaaggaa(cons(T38, T39), T40, X62, X63, T9, T10, X16, X17)
U1_gg(T7, T8, T9, T10, pB_out_ggaaggaa(T7, T8, X14, X15, T9, T10, X16, X17)) → samefringeA_out_gg(cons(T7, T8), cons(T9, T10))
GOPHERC_IN_GGAA(cons(T29, T30), T31, X44, X45) → GOPHERC_IN_GGAA(T29, cons(T30, T31), X44, X45)
samefringeA_in_gg(nil, nil) → samefringeA_out_gg(nil, nil)
samefringeA_in_gg(cons(T7, T8), cons(T9, T10)) → U1_gg(T7, T8, T9, T10, pB_in_ggaaggaa(T7, T8, X14, X15, T9, T10, X16, X17))
pB_in_ggaaggaa(nil, T15, nil, T15, T9, T10, X16, X17) → U3_ggaaggaa(T15, T9, T10, X16, X17, pD_in_ggaag(T9, T10, X16, X17, T15))
pD_in_ggaag(T9, T10, T16, T17, T15) → U5_ggaag(T9, T10, T16, T17, T15, gopherC_in_ggaa(T9, T10, T16, T17))
gopherC_in_ggaa(nil, T22, nil, T22) → gopherC_out_ggaa(nil, T22, nil, T22)
gopherC_in_ggaa(cons(T29, T30), T31, X44, X45) → U2_ggaa(T29, T30, T31, X44, X45, gopherC_in_ggaa(T29, cons(T30, T31), X44, X45))
U2_ggaa(T29, T30, T31, X44, X45, gopherC_out_ggaa(T29, cons(T30, T31), X44, X45)) → gopherC_out_ggaa(cons(T29, T30), T31, X44, X45)
U5_ggaag(T9, T10, T16, T17, T15, gopherC_out_ggaa(T9, T10, T16, T17)) → U6_ggaag(T9, T10, T16, T17, T15, samefringeA_in_gg(T15, T17))
U6_ggaag(T9, T10, T16, T17, T15, samefringeA_out_gg(T15, T17)) → pD_out_ggaag(T9, T10, T16, T17, T15)
U3_ggaaggaa(T15, T9, T10, X16, X17, pD_out_ggaag(T9, T10, X16, X17, T15)) → pB_out_ggaaggaa(nil, T15, nil, T15, T9, T10, X16, X17)
pB_in_ggaaggaa(cons(T38, T39), T40, X62, X63, T9, T10, X16, X17) → U4_ggaaggaa(T38, T39, T40, X62, X63, T9, T10, X16, X17, pB_in_ggaaggaa(T38, cons(T39, T40), X62, X63, T9, T10, X16, X17))
U4_ggaaggaa(T38, T39, T40, X62, X63, T9, T10, X16, X17, pB_out_ggaaggaa(T38, cons(T39, T40), X62, X63, T9, T10, X16, X17)) → pB_out_ggaaggaa(cons(T38, T39), T40, X62, X63, T9, T10, X16, X17)
U1_gg(T7, T8, T9, T10, pB_out_ggaaggaa(T7, T8, X14, X15, T9, T10, X16, X17)) → samefringeA_out_gg(cons(T7, T8), cons(T9, T10))
GOPHERC_IN_GGAA(cons(T29, T30), T31, X44, X45) → GOPHERC_IN_GGAA(T29, cons(T30, T31), X44, X45)
GOPHERC_IN_GGAA(cons(T29, T30), T31) → GOPHERC_IN_GGAA(T29, cons(T30, T31))
From the DPs we obtained the following set of size-change graphs:
SAMEFRINGEA_IN_GG(cons(T7, T8), cons(T9, T10)) → PB_IN_GGAAGGAA(T7, T8, X14, X15, T9, T10, X16, X17)
PB_IN_GGAAGGAA(nil, T15, nil, T15, T9, T10, X16, X17) → PD_IN_GGAAG(T9, T10, X16, X17, T15)
PD_IN_GGAAG(T9, T10, T16, T17, T15) → U5_GGAAG(T9, T10, T16, T17, T15, gopherC_in_ggaa(T9, T10, T16, T17))
U5_GGAAG(T9, T10, T16, T17, T15, gopherC_out_ggaa(T9, T10, T16, T17)) → SAMEFRINGEA_IN_GG(T15, T17)
PB_IN_GGAAGGAA(cons(T38, T39), T40, X62, X63, T9, T10, X16, X17) → PB_IN_GGAAGGAA(T38, cons(T39, T40), X62, X63, T9, T10, X16, X17)
samefringeA_in_gg(nil, nil) → samefringeA_out_gg(nil, nil)
samefringeA_in_gg(cons(T7, T8), cons(T9, T10)) → U1_gg(T7, T8, T9, T10, pB_in_ggaaggaa(T7, T8, X14, X15, T9, T10, X16, X17))
pB_in_ggaaggaa(nil, T15, nil, T15, T9, T10, X16, X17) → U3_ggaaggaa(T15, T9, T10, X16, X17, pD_in_ggaag(T9, T10, X16, X17, T15))
pD_in_ggaag(T9, T10, T16, T17, T15) → U5_ggaag(T9, T10, T16, T17, T15, gopherC_in_ggaa(T9, T10, T16, T17))
gopherC_in_ggaa(nil, T22, nil, T22) → gopherC_out_ggaa(nil, T22, nil, T22)
gopherC_in_ggaa(cons(T29, T30), T31, X44, X45) → U2_ggaa(T29, T30, T31, X44, X45, gopherC_in_ggaa(T29, cons(T30, T31), X44, X45))
U2_ggaa(T29, T30, T31, X44, X45, gopherC_out_ggaa(T29, cons(T30, T31), X44, X45)) → gopherC_out_ggaa(cons(T29, T30), T31, X44, X45)
U5_ggaag(T9, T10, T16, T17, T15, gopherC_out_ggaa(T9, T10, T16, T17)) → U6_ggaag(T9, T10, T16, T17, T15, samefringeA_in_gg(T15, T17))
U6_ggaag(T9, T10, T16, T17, T15, samefringeA_out_gg(T15, T17)) → pD_out_ggaag(T9, T10, T16, T17, T15)
U3_ggaaggaa(T15, T9, T10, X16, X17, pD_out_ggaag(T9, T10, X16, X17, T15)) → pB_out_ggaaggaa(nil, T15, nil, T15, T9, T10, X16, X17)
pB_in_ggaaggaa(cons(T38, T39), T40, X62, X63, T9, T10, X16, X17) → U4_ggaaggaa(T38, T39, T40, X62, X63, T9, T10, X16, X17, pB_in_ggaaggaa(T38, cons(T39, T40), X62, X63, T9, T10, X16, X17))
U4_ggaaggaa(T38, T39, T40, X62, X63, T9, T10, X16, X17, pB_out_ggaaggaa(T38, cons(T39, T40), X62, X63, T9, T10, X16, X17)) → pB_out_ggaaggaa(cons(T38, T39), T40, X62, X63, T9, T10, X16, X17)
U1_gg(T7, T8, T9, T10, pB_out_ggaaggaa(T7, T8, X14, X15, T9, T10, X16, X17)) → samefringeA_out_gg(cons(T7, T8), cons(T9, T10))
SAMEFRINGEA_IN_GG(cons(T7, T8), cons(T9, T10)) → PB_IN_GGAAGGAA(T7, T8, X14, X15, T9, T10, X16, X17)
PB_IN_GGAAGGAA(nil, T15, nil, T15, T9, T10, X16, X17) → PD_IN_GGAAG(T9, T10, X16, X17, T15)
PD_IN_GGAAG(T9, T10, T16, T17, T15) → U5_GGAAG(T9, T10, T16, T17, T15, gopherC_in_ggaa(T9, T10, T16, T17))
U5_GGAAG(T9, T10, T16, T17, T15, gopherC_out_ggaa(T9, T10, T16, T17)) → SAMEFRINGEA_IN_GG(T15, T17)
PB_IN_GGAAGGAA(cons(T38, T39), T40, X62, X63, T9, T10, X16, X17) → PB_IN_GGAAGGAA(T38, cons(T39, T40), X62, X63, T9, T10, X16, X17)
gopherC_in_ggaa(nil, T22, nil, T22) → gopherC_out_ggaa(nil, T22, nil, T22)
gopherC_in_ggaa(cons(T29, T30), T31, X44, X45) → U2_ggaa(T29, T30, T31, X44, X45, gopherC_in_ggaa(T29, cons(T30, T31), X44, X45))
U2_ggaa(T29, T30, T31, X44, X45, gopherC_out_ggaa(T29, cons(T30, T31), X44, X45)) → gopherC_out_ggaa(cons(T29, T30), T31, X44, X45)
SAMEFRINGEA_IN_GG(cons(T7, T8), cons(T9, T10)) → PB_IN_GGAAGGAA(T7, T8, T9, T10)
PB_IN_GGAAGGAA(nil, T15, T9, T10) → PD_IN_GGAAG(T9, T10, T15)
PD_IN_GGAAG(T9, T10, T15) → U5_GGAAG(T9, T10, T15, gopherC_in_ggaa(T9, T10))
U5_GGAAG(T9, T10, T15, gopherC_out_ggaa(T9, T10, T16, T17)) → SAMEFRINGEA_IN_GG(T15, T17)
PB_IN_GGAAGGAA(cons(T38, T39), T40, T9, T10) → PB_IN_GGAAGGAA(T38, cons(T39, T40), T9, T10)
gopherC_in_ggaa(nil, T22) → gopherC_out_ggaa(nil, T22, nil, T22)
gopherC_in_ggaa(cons(T29, T30), T31) → U2_ggaa(T29, T30, T31, gopherC_in_ggaa(T29, cons(T30, T31)))
U2_ggaa(T29, T30, T31, gopherC_out_ggaa(T29, cons(T30, T31), X44, X45)) → gopherC_out_ggaa(cons(T29, T30), T31, X44, X45)
gopherC_in_ggaa(x0, x1)
U2_ggaa(x0, x1, x2, x3)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
SAMEFRINGEA_IN_GG(cons(T7, T8), cons(T9, T10)) → PB_IN_GGAAGGAA(T7, T8, T9, T10)
POL(PB_IN_GGAAGGAA(x1, x2, x3, x4)) = x1 + x2
POL(PD_IN_GGAAG(x1, x2, x3)) = x3
POL(SAMEFRINGEA_IN_GG(x1, x2)) = x1
POL(U2_ggaa(x1, x2, x3, x4)) = 0
POL(U5_GGAAG(x1, x2, x3, x4)) = x3
POL(cons(x1, x2)) = 1 + x1 + x2
POL(gopherC_in_ggaa(x1, x2)) = 0
POL(gopherC_out_ggaa(x1, x2, x3, x4)) = 0
POL(nil) = 0
PB_IN_GGAAGGAA(nil, T15, T9, T10) → PD_IN_GGAAG(T9, T10, T15)
PD_IN_GGAAG(T9, T10, T15) → U5_GGAAG(T9, T10, T15, gopherC_in_ggaa(T9, T10))
U5_GGAAG(T9, T10, T15, gopherC_out_ggaa(T9, T10, T16, T17)) → SAMEFRINGEA_IN_GG(T15, T17)
PB_IN_GGAAGGAA(cons(T38, T39), T40, T9, T10) → PB_IN_GGAAGGAA(T38, cons(T39, T40), T9, T10)
gopherC_in_ggaa(nil, T22) → gopherC_out_ggaa(nil, T22, nil, T22)
gopherC_in_ggaa(cons(T29, T30), T31) → U2_ggaa(T29, T30, T31, gopherC_in_ggaa(T29, cons(T30, T31)))
U2_ggaa(T29, T30, T31, gopherC_out_ggaa(T29, cons(T30, T31), X44, X45)) → gopherC_out_ggaa(cons(T29, T30), T31, X44, X45)
gopherC_in_ggaa(x0, x1)
U2_ggaa(x0, x1, x2, x3)
PB_IN_GGAAGGAA(cons(T38, T39), T40, T9, T10) → PB_IN_GGAAGGAA(T38, cons(T39, T40), T9, T10)
gopherC_in_ggaa(nil, T22) → gopherC_out_ggaa(nil, T22, nil, T22)
gopherC_in_ggaa(cons(T29, T30), T31) → U2_ggaa(T29, T30, T31, gopherC_in_ggaa(T29, cons(T30, T31)))
U2_ggaa(T29, T30, T31, gopherC_out_ggaa(T29, cons(T30, T31), X44, X45)) → gopherC_out_ggaa(cons(T29, T30), T31, X44, X45)
gopherC_in_ggaa(x0, x1)
U2_ggaa(x0, x1, x2, x3)
PB_IN_GGAAGGAA(cons(T38, T39), T40, T9, T10) → PB_IN_GGAAGGAA(T38, cons(T39, T40), T9, T10)
gopherC_in_ggaa(x0, x1)
U2_ggaa(x0, x1, x2, x3)
gopherC_in_ggaa(x0, x1)
U2_ggaa(x0, x1, x2, x3)
PB_IN_GGAAGGAA(cons(T38, T39), T40, T9, T10) → PB_IN_GGAAGGAA(T38, cons(T39, T40), T9, T10)
From the DPs we obtained the following set of size-change graphs: