0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 194 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 120 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 (⇔, 1 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇒, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 PiDP
↳22 UsableRulesProof (⇔, 0 ms)
↳23 PiDP
↳24 PiDPToQDPProof (⇒, 0 ms)
↳25 QDP
↳26 Rewriting (⇔, 0 ms)
↳27 QDP
↳28 UsableRulesProof (⇔, 0 ms)
↳29 QDP
↳30 QReductionProof (⇔, 3 ms)
↳31 QDP
↳32 Rewriting (⇔, 0 ms)
↳33 QDP
↳34 UsableRulesProof (⇔, 0 ms)
↳35 QDP
↳36 QReductionProof (⇔, 0 ms)
↳37 QDP
↳38 Instantiation (⇔, 0 ms)
↳39 QDP
↳40 QDPOrderProof (⇔, 167 ms)
↳41 QDP
↳42 DependencyGraphProof (⇔, 0 ms)
↳43 TRUE
permA_in_ga(.(T24, T25), .(T26, T27)) → U1_ga(T24, T25, T26, T27, pB_in_aaaggaa(X43, T26, X44, T25, T24, X9, T27))
pB_in_aaaggaa(T31, T26, T32, T25, T24, X9, T33) → U6_aaaggaa(T31, T26, T32, T25, T24, X9, T33, app2D_in_aaag(T31, T26, T32, T25))
app2D_in_aaag(.(T50, X92), T52, X93, .(T50, T51)) → U3_aaag(T50, X92, T52, X93, T51, app2D_in_aaag(X92, T52, X93, T51))
app2D_in_aaag([], T60, T61, .(T60, T61)) → app2D_out_aaag([], T60, T61, .(T60, T61))
U3_aaag(T50, X92, T52, X93, T51, app2D_out_aaag(X92, T52, X93, T51)) → app2D_out_aaag(.(T50, X92), T52, X93, .(T50, T51))
U6_aaaggaa(T31, T26, T32, T25, T24, X9, T33, app2D_out_aaag(T31, T26, T32, T25)) → U7_aaaggaa(T31, T26, T32, T25, T24, X9, T33, pH_in_gggaa(T24, T31, T32, X9, T33))
pH_in_gggaa(T24, T31, T32, T65, T33) → U8_gggaa(T24, T31, T32, T65, T33, app1F_in_ggga(T24, T31, T32, T65))
app1F_in_ggga(T87, T88, T89, .(T87, X151)) → U5_ggga(T87, T88, T89, X151, app1E_in_gga(T88, T89, X151))
app1E_in_gga(.(T105, T106), T107, .(T105, X181)) → U4_gga(T105, T106, T107, X181, app1E_in_gga(T106, T107, X181))
app1E_in_gga([], T113, T113) → app1E_out_gga([], T113, T113)
U4_gga(T105, T106, T107, X181, app1E_out_gga(T106, T107, X181)) → app1E_out_gga(.(T105, T106), T107, .(T105, X181))
U5_ggga(T87, T88, T89, X151, app1E_out_gga(T88, T89, X151)) → app1F_out_ggga(T87, T88, T89, .(T87, X151))
U8_gggaa(T24, T31, T32, T65, T33, app1F_out_ggga(T24, T31, T32, T65)) → U9_gggaa(T24, T31, T32, T65, T33, permA_in_ga(T65, T33))
permA_in_ga(.(T125, T126), .(T125, T127)) → U2_ga(T125, T126, T127, pC_in_gaa(T126, X9, T127))
pC_in_gaa(T126, T128, T127) → U10_gaa(T126, T128, T127, app1G_in_ga(T126, T128))
app1G_in_ga(T131, T131) → app1G_out_ga(T131, T131)
U10_gaa(T126, T128, T127, app1G_out_ga(T126, T128)) → U11_gaa(T126, T128, T127, permA_in_ga(T128, T127))
permA_in_ga([], []) → permA_out_ga([], [])
U11_gaa(T126, T128, T127, permA_out_ga(T128, T127)) → pC_out_gaa(T126, T128, T127)
U2_ga(T125, T126, T127, pC_out_gaa(T126, X9, T127)) → permA_out_ga(.(T125, T126), .(T125, T127))
U9_gggaa(T24, T31, T32, T65, T33, permA_out_ga(T65, T33)) → pH_out_gggaa(T24, T31, T32, T65, T33)
U7_aaaggaa(T31, T26, T32, T25, T24, X9, T33, pH_out_gggaa(T24, T31, T32, X9, T33)) → pB_out_aaaggaa(T31, T26, T32, T25, T24, X9, T33)
U1_ga(T24, T25, T26, T27, pB_out_aaaggaa(X43, T26, X44, T25, T24, X9, T27)) → permA_out_ga(.(T24, T25), .(T26, T27))
PERMA_IN_GA(.(T24, T25), .(T26, T27)) → U1_GA(T24, T25, T26, T27, pB_in_aaaggaa(X43, T26, X44, T25, T24, X9, T27))
PERMA_IN_GA(.(T24, T25), .(T26, T27)) → PB_IN_AAAGGAA(X43, T26, X44, T25, T24, X9, T27)
PB_IN_AAAGGAA(T31, T26, T32, T25, T24, X9, T33) → U6_AAAGGAA(T31, T26, T32, T25, T24, X9, T33, app2D_in_aaag(T31, T26, T32, T25))
PB_IN_AAAGGAA(T31, T26, T32, T25, T24, X9, T33) → APP2D_IN_AAAG(T31, T26, T32, T25)
APP2D_IN_AAAG(.(T50, X92), T52, X93, .(T50, T51)) → U3_AAAG(T50, X92, T52, X93, T51, app2D_in_aaag(X92, T52, X93, T51))
APP2D_IN_AAAG(.(T50, X92), T52, X93, .(T50, T51)) → APP2D_IN_AAAG(X92, T52, X93, T51)
U6_AAAGGAA(T31, T26, T32, T25, T24, X9, T33, app2D_out_aaag(T31, T26, T32, T25)) → U7_AAAGGAA(T31, T26, T32, T25, T24, X9, T33, pH_in_gggaa(T24, T31, T32, X9, T33))
U6_AAAGGAA(T31, T26, T32, T25, T24, X9, T33, app2D_out_aaag(T31, T26, T32, T25)) → PH_IN_GGGAA(T24, T31, T32, X9, T33)
PH_IN_GGGAA(T24, T31, T32, T65, T33) → U8_GGGAA(T24, T31, T32, T65, T33, app1F_in_ggga(T24, T31, T32, T65))
PH_IN_GGGAA(T24, T31, T32, T65, T33) → APP1F_IN_GGGA(T24, T31, T32, T65)
APP1F_IN_GGGA(T87, T88, T89, .(T87, X151)) → U5_GGGA(T87, T88, T89, X151, app1E_in_gga(T88, T89, X151))
APP1F_IN_GGGA(T87, T88, T89, .(T87, X151)) → APP1E_IN_GGA(T88, T89, X151)
APP1E_IN_GGA(.(T105, T106), T107, .(T105, X181)) → U4_GGA(T105, T106, T107, X181, app1E_in_gga(T106, T107, X181))
APP1E_IN_GGA(.(T105, T106), T107, .(T105, X181)) → APP1E_IN_GGA(T106, T107, X181)
U8_GGGAA(T24, T31, T32, T65, T33, app1F_out_ggga(T24, T31, T32, T65)) → U9_GGGAA(T24, T31, T32, T65, T33, permA_in_ga(T65, T33))
U8_GGGAA(T24, T31, T32, T65, T33, app1F_out_ggga(T24, T31, T32, T65)) → PERMA_IN_GA(T65, T33)
PERMA_IN_GA(.(T125, T126), .(T125, T127)) → U2_GA(T125, T126, T127, pC_in_gaa(T126, X9, T127))
PERMA_IN_GA(.(T125, T126), .(T125, T127)) → PC_IN_GAA(T126, X9, T127)
PC_IN_GAA(T126, T128, T127) → U10_GAA(T126, T128, T127, app1G_in_ga(T126, T128))
PC_IN_GAA(T126, T128, T127) → APP1G_IN_GA(T126, T128)
U10_GAA(T126, T128, T127, app1G_out_ga(T126, T128)) → U11_GAA(T126, T128, T127, permA_in_ga(T128, T127))
U10_GAA(T126, T128, T127, app1G_out_ga(T126, T128)) → PERMA_IN_GA(T128, T127)
permA_in_ga(.(T24, T25), .(T26, T27)) → U1_ga(T24, T25, T26, T27, pB_in_aaaggaa(X43, T26, X44, T25, T24, X9, T27))
pB_in_aaaggaa(T31, T26, T32, T25, T24, X9, T33) → U6_aaaggaa(T31, T26, T32, T25, T24, X9, T33, app2D_in_aaag(T31, T26, T32, T25))
app2D_in_aaag(.(T50, X92), T52, X93, .(T50, T51)) → U3_aaag(T50, X92, T52, X93, T51, app2D_in_aaag(X92, T52, X93, T51))
app2D_in_aaag([], T60, T61, .(T60, T61)) → app2D_out_aaag([], T60, T61, .(T60, T61))
U3_aaag(T50, X92, T52, X93, T51, app2D_out_aaag(X92, T52, X93, T51)) → app2D_out_aaag(.(T50, X92), T52, X93, .(T50, T51))
U6_aaaggaa(T31, T26, T32, T25, T24, X9, T33, app2D_out_aaag(T31, T26, T32, T25)) → U7_aaaggaa(T31, T26, T32, T25, T24, X9, T33, pH_in_gggaa(T24, T31, T32, X9, T33))
pH_in_gggaa(T24, T31, T32, T65, T33) → U8_gggaa(T24, T31, T32, T65, T33, app1F_in_ggga(T24, T31, T32, T65))
app1F_in_ggga(T87, T88, T89, .(T87, X151)) → U5_ggga(T87, T88, T89, X151, app1E_in_gga(T88, T89, X151))
app1E_in_gga(.(T105, T106), T107, .(T105, X181)) → U4_gga(T105, T106, T107, X181, app1E_in_gga(T106, T107, X181))
app1E_in_gga([], T113, T113) → app1E_out_gga([], T113, T113)
U4_gga(T105, T106, T107, X181, app1E_out_gga(T106, T107, X181)) → app1E_out_gga(.(T105, T106), T107, .(T105, X181))
U5_ggga(T87, T88, T89, X151, app1E_out_gga(T88, T89, X151)) → app1F_out_ggga(T87, T88, T89, .(T87, X151))
U8_gggaa(T24, T31, T32, T65, T33, app1F_out_ggga(T24, T31, T32, T65)) → U9_gggaa(T24, T31, T32, T65, T33, permA_in_ga(T65, T33))
permA_in_ga(.(T125, T126), .(T125, T127)) → U2_ga(T125, T126, T127, pC_in_gaa(T126, X9, T127))
pC_in_gaa(T126, T128, T127) → U10_gaa(T126, T128, T127, app1G_in_ga(T126, T128))
app1G_in_ga(T131, T131) → app1G_out_ga(T131, T131)
U10_gaa(T126, T128, T127, app1G_out_ga(T126, T128)) → U11_gaa(T126, T128, T127, permA_in_ga(T128, T127))
permA_in_ga([], []) → permA_out_ga([], [])
U11_gaa(T126, T128, T127, permA_out_ga(T128, T127)) → pC_out_gaa(T126, T128, T127)
U2_ga(T125, T126, T127, pC_out_gaa(T126, X9, T127)) → permA_out_ga(.(T125, T126), .(T125, T127))
U9_gggaa(T24, T31, T32, T65, T33, permA_out_ga(T65, T33)) → pH_out_gggaa(T24, T31, T32, T65, T33)
U7_aaaggaa(T31, T26, T32, T25, T24, X9, T33, pH_out_gggaa(T24, T31, T32, X9, T33)) → pB_out_aaaggaa(T31, T26, T32, T25, T24, X9, T33)
U1_ga(T24, T25, T26, T27, pB_out_aaaggaa(X43, T26, X44, T25, T24, X9, T27)) → permA_out_ga(.(T24, T25), .(T26, T27))
PERMA_IN_GA(.(T24, T25), .(T26, T27)) → U1_GA(T24, T25, T26, T27, pB_in_aaaggaa(X43, T26, X44, T25, T24, X9, T27))
PERMA_IN_GA(.(T24, T25), .(T26, T27)) → PB_IN_AAAGGAA(X43, T26, X44, T25, T24, X9, T27)
PB_IN_AAAGGAA(T31, T26, T32, T25, T24, X9, T33) → U6_AAAGGAA(T31, T26, T32, T25, T24, X9, T33, app2D_in_aaag(T31, T26, T32, T25))
PB_IN_AAAGGAA(T31, T26, T32, T25, T24, X9, T33) → APP2D_IN_AAAG(T31, T26, T32, T25)
APP2D_IN_AAAG(.(T50, X92), T52, X93, .(T50, T51)) → U3_AAAG(T50, X92, T52, X93, T51, app2D_in_aaag(X92, T52, X93, T51))
APP2D_IN_AAAG(.(T50, X92), T52, X93, .(T50, T51)) → APP2D_IN_AAAG(X92, T52, X93, T51)
U6_AAAGGAA(T31, T26, T32, T25, T24, X9, T33, app2D_out_aaag(T31, T26, T32, T25)) → U7_AAAGGAA(T31, T26, T32, T25, T24, X9, T33, pH_in_gggaa(T24, T31, T32, X9, T33))
U6_AAAGGAA(T31, T26, T32, T25, T24, X9, T33, app2D_out_aaag(T31, T26, T32, T25)) → PH_IN_GGGAA(T24, T31, T32, X9, T33)
PH_IN_GGGAA(T24, T31, T32, T65, T33) → U8_GGGAA(T24, T31, T32, T65, T33, app1F_in_ggga(T24, T31, T32, T65))
PH_IN_GGGAA(T24, T31, T32, T65, T33) → APP1F_IN_GGGA(T24, T31, T32, T65)
APP1F_IN_GGGA(T87, T88, T89, .(T87, X151)) → U5_GGGA(T87, T88, T89, X151, app1E_in_gga(T88, T89, X151))
APP1F_IN_GGGA(T87, T88, T89, .(T87, X151)) → APP1E_IN_GGA(T88, T89, X151)
APP1E_IN_GGA(.(T105, T106), T107, .(T105, X181)) → U4_GGA(T105, T106, T107, X181, app1E_in_gga(T106, T107, X181))
APP1E_IN_GGA(.(T105, T106), T107, .(T105, X181)) → APP1E_IN_GGA(T106, T107, X181)
U8_GGGAA(T24, T31, T32, T65, T33, app1F_out_ggga(T24, T31, T32, T65)) → U9_GGGAA(T24, T31, T32, T65, T33, permA_in_ga(T65, T33))
U8_GGGAA(T24, T31, T32, T65, T33, app1F_out_ggga(T24, T31, T32, T65)) → PERMA_IN_GA(T65, T33)
PERMA_IN_GA(.(T125, T126), .(T125, T127)) → U2_GA(T125, T126, T127, pC_in_gaa(T126, X9, T127))
PERMA_IN_GA(.(T125, T126), .(T125, T127)) → PC_IN_GAA(T126, X9, T127)
PC_IN_GAA(T126, T128, T127) → U10_GAA(T126, T128, T127, app1G_in_ga(T126, T128))
PC_IN_GAA(T126, T128, T127) → APP1G_IN_GA(T126, T128)
U10_GAA(T126, T128, T127, app1G_out_ga(T126, T128)) → U11_GAA(T126, T128, T127, permA_in_ga(T128, T127))
U10_GAA(T126, T128, T127, app1G_out_ga(T126, T128)) → PERMA_IN_GA(T128, T127)
permA_in_ga(.(T24, T25), .(T26, T27)) → U1_ga(T24, T25, T26, T27, pB_in_aaaggaa(X43, T26, X44, T25, T24, X9, T27))
pB_in_aaaggaa(T31, T26, T32, T25, T24, X9, T33) → U6_aaaggaa(T31, T26, T32, T25, T24, X9, T33, app2D_in_aaag(T31, T26, T32, T25))
app2D_in_aaag(.(T50, X92), T52, X93, .(T50, T51)) → U3_aaag(T50, X92, T52, X93, T51, app2D_in_aaag(X92, T52, X93, T51))
app2D_in_aaag([], T60, T61, .(T60, T61)) → app2D_out_aaag([], T60, T61, .(T60, T61))
U3_aaag(T50, X92, T52, X93, T51, app2D_out_aaag(X92, T52, X93, T51)) → app2D_out_aaag(.(T50, X92), T52, X93, .(T50, T51))
U6_aaaggaa(T31, T26, T32, T25, T24, X9, T33, app2D_out_aaag(T31, T26, T32, T25)) → U7_aaaggaa(T31, T26, T32, T25, T24, X9, T33, pH_in_gggaa(T24, T31, T32, X9, T33))
pH_in_gggaa(T24, T31, T32, T65, T33) → U8_gggaa(T24, T31, T32, T65, T33, app1F_in_ggga(T24, T31, T32, T65))
app1F_in_ggga(T87, T88, T89, .(T87, X151)) → U5_ggga(T87, T88, T89, X151, app1E_in_gga(T88, T89, X151))
app1E_in_gga(.(T105, T106), T107, .(T105, X181)) → U4_gga(T105, T106, T107, X181, app1E_in_gga(T106, T107, X181))
app1E_in_gga([], T113, T113) → app1E_out_gga([], T113, T113)
U4_gga(T105, T106, T107, X181, app1E_out_gga(T106, T107, X181)) → app1E_out_gga(.(T105, T106), T107, .(T105, X181))
U5_ggga(T87, T88, T89, X151, app1E_out_gga(T88, T89, X151)) → app1F_out_ggga(T87, T88, T89, .(T87, X151))
U8_gggaa(T24, T31, T32, T65, T33, app1F_out_ggga(T24, T31, T32, T65)) → U9_gggaa(T24, T31, T32, T65, T33, permA_in_ga(T65, T33))
permA_in_ga(.(T125, T126), .(T125, T127)) → U2_ga(T125, T126, T127, pC_in_gaa(T126, X9, T127))
pC_in_gaa(T126, T128, T127) → U10_gaa(T126, T128, T127, app1G_in_ga(T126, T128))
app1G_in_ga(T131, T131) → app1G_out_ga(T131, T131)
U10_gaa(T126, T128, T127, app1G_out_ga(T126, T128)) → U11_gaa(T126, T128, T127, permA_in_ga(T128, T127))
permA_in_ga([], []) → permA_out_ga([], [])
U11_gaa(T126, T128, T127, permA_out_ga(T128, T127)) → pC_out_gaa(T126, T128, T127)
U2_ga(T125, T126, T127, pC_out_gaa(T126, X9, T127)) → permA_out_ga(.(T125, T126), .(T125, T127))
U9_gggaa(T24, T31, T32, T65, T33, permA_out_ga(T65, T33)) → pH_out_gggaa(T24, T31, T32, T65, T33)
U7_aaaggaa(T31, T26, T32, T25, T24, X9, T33, pH_out_gggaa(T24, T31, T32, X9, T33)) → pB_out_aaaggaa(T31, T26, T32, T25, T24, X9, T33)
U1_ga(T24, T25, T26, T27, pB_out_aaaggaa(X43, T26, X44, T25, T24, X9, T27)) → permA_out_ga(.(T24, T25), .(T26, T27))
APP1E_IN_GGA(.(T105, T106), T107, .(T105, X181)) → APP1E_IN_GGA(T106, T107, X181)
permA_in_ga(.(T24, T25), .(T26, T27)) → U1_ga(T24, T25, T26, T27, pB_in_aaaggaa(X43, T26, X44, T25, T24, X9, T27))
pB_in_aaaggaa(T31, T26, T32, T25, T24, X9, T33) → U6_aaaggaa(T31, T26, T32, T25, T24, X9, T33, app2D_in_aaag(T31, T26, T32, T25))
app2D_in_aaag(.(T50, X92), T52, X93, .(T50, T51)) → U3_aaag(T50, X92, T52, X93, T51, app2D_in_aaag(X92, T52, X93, T51))
app2D_in_aaag([], T60, T61, .(T60, T61)) → app2D_out_aaag([], T60, T61, .(T60, T61))
U3_aaag(T50, X92, T52, X93, T51, app2D_out_aaag(X92, T52, X93, T51)) → app2D_out_aaag(.(T50, X92), T52, X93, .(T50, T51))
U6_aaaggaa(T31, T26, T32, T25, T24, X9, T33, app2D_out_aaag(T31, T26, T32, T25)) → U7_aaaggaa(T31, T26, T32, T25, T24, X9, T33, pH_in_gggaa(T24, T31, T32, X9, T33))
pH_in_gggaa(T24, T31, T32, T65, T33) → U8_gggaa(T24, T31, T32, T65, T33, app1F_in_ggga(T24, T31, T32, T65))
app1F_in_ggga(T87, T88, T89, .(T87, X151)) → U5_ggga(T87, T88, T89, X151, app1E_in_gga(T88, T89, X151))
app1E_in_gga(.(T105, T106), T107, .(T105, X181)) → U4_gga(T105, T106, T107, X181, app1E_in_gga(T106, T107, X181))
app1E_in_gga([], T113, T113) → app1E_out_gga([], T113, T113)
U4_gga(T105, T106, T107, X181, app1E_out_gga(T106, T107, X181)) → app1E_out_gga(.(T105, T106), T107, .(T105, X181))
U5_ggga(T87, T88, T89, X151, app1E_out_gga(T88, T89, X151)) → app1F_out_ggga(T87, T88, T89, .(T87, X151))
U8_gggaa(T24, T31, T32, T65, T33, app1F_out_ggga(T24, T31, T32, T65)) → U9_gggaa(T24, T31, T32, T65, T33, permA_in_ga(T65, T33))
permA_in_ga(.(T125, T126), .(T125, T127)) → U2_ga(T125, T126, T127, pC_in_gaa(T126, X9, T127))
pC_in_gaa(T126, T128, T127) → U10_gaa(T126, T128, T127, app1G_in_ga(T126, T128))
app1G_in_ga(T131, T131) → app1G_out_ga(T131, T131)
U10_gaa(T126, T128, T127, app1G_out_ga(T126, T128)) → U11_gaa(T126, T128, T127, permA_in_ga(T128, T127))
permA_in_ga([], []) → permA_out_ga([], [])
U11_gaa(T126, T128, T127, permA_out_ga(T128, T127)) → pC_out_gaa(T126, T128, T127)
U2_ga(T125, T126, T127, pC_out_gaa(T126, X9, T127)) → permA_out_ga(.(T125, T126), .(T125, T127))
U9_gggaa(T24, T31, T32, T65, T33, permA_out_ga(T65, T33)) → pH_out_gggaa(T24, T31, T32, T65, T33)
U7_aaaggaa(T31, T26, T32, T25, T24, X9, T33, pH_out_gggaa(T24, T31, T32, X9, T33)) → pB_out_aaaggaa(T31, T26, T32, T25, T24, X9, T33)
U1_ga(T24, T25, T26, T27, pB_out_aaaggaa(X43, T26, X44, T25, T24, X9, T27)) → permA_out_ga(.(T24, T25), .(T26, T27))
APP1E_IN_GGA(.(T105, T106), T107, .(T105, X181)) → APP1E_IN_GGA(T106, T107, X181)
APP1E_IN_GGA(.(T105, T106), T107) → APP1E_IN_GGA(T106, T107)
From the DPs we obtained the following set of size-change graphs:
APP2D_IN_AAAG(.(T50, X92), T52, X93, .(T50, T51)) → APP2D_IN_AAAG(X92, T52, X93, T51)
permA_in_ga(.(T24, T25), .(T26, T27)) → U1_ga(T24, T25, T26, T27, pB_in_aaaggaa(X43, T26, X44, T25, T24, X9, T27))
pB_in_aaaggaa(T31, T26, T32, T25, T24, X9, T33) → U6_aaaggaa(T31, T26, T32, T25, T24, X9, T33, app2D_in_aaag(T31, T26, T32, T25))
app2D_in_aaag(.(T50, X92), T52, X93, .(T50, T51)) → U3_aaag(T50, X92, T52, X93, T51, app2D_in_aaag(X92, T52, X93, T51))
app2D_in_aaag([], T60, T61, .(T60, T61)) → app2D_out_aaag([], T60, T61, .(T60, T61))
U3_aaag(T50, X92, T52, X93, T51, app2D_out_aaag(X92, T52, X93, T51)) → app2D_out_aaag(.(T50, X92), T52, X93, .(T50, T51))
U6_aaaggaa(T31, T26, T32, T25, T24, X9, T33, app2D_out_aaag(T31, T26, T32, T25)) → U7_aaaggaa(T31, T26, T32, T25, T24, X9, T33, pH_in_gggaa(T24, T31, T32, X9, T33))
pH_in_gggaa(T24, T31, T32, T65, T33) → U8_gggaa(T24, T31, T32, T65, T33, app1F_in_ggga(T24, T31, T32, T65))
app1F_in_ggga(T87, T88, T89, .(T87, X151)) → U5_ggga(T87, T88, T89, X151, app1E_in_gga(T88, T89, X151))
app1E_in_gga(.(T105, T106), T107, .(T105, X181)) → U4_gga(T105, T106, T107, X181, app1E_in_gga(T106, T107, X181))
app1E_in_gga([], T113, T113) → app1E_out_gga([], T113, T113)
U4_gga(T105, T106, T107, X181, app1E_out_gga(T106, T107, X181)) → app1E_out_gga(.(T105, T106), T107, .(T105, X181))
U5_ggga(T87, T88, T89, X151, app1E_out_gga(T88, T89, X151)) → app1F_out_ggga(T87, T88, T89, .(T87, X151))
U8_gggaa(T24, T31, T32, T65, T33, app1F_out_ggga(T24, T31, T32, T65)) → U9_gggaa(T24, T31, T32, T65, T33, permA_in_ga(T65, T33))
permA_in_ga(.(T125, T126), .(T125, T127)) → U2_ga(T125, T126, T127, pC_in_gaa(T126, X9, T127))
pC_in_gaa(T126, T128, T127) → U10_gaa(T126, T128, T127, app1G_in_ga(T126, T128))
app1G_in_ga(T131, T131) → app1G_out_ga(T131, T131)
U10_gaa(T126, T128, T127, app1G_out_ga(T126, T128)) → U11_gaa(T126, T128, T127, permA_in_ga(T128, T127))
permA_in_ga([], []) → permA_out_ga([], [])
U11_gaa(T126, T128, T127, permA_out_ga(T128, T127)) → pC_out_gaa(T126, T128, T127)
U2_ga(T125, T126, T127, pC_out_gaa(T126, X9, T127)) → permA_out_ga(.(T125, T126), .(T125, T127))
U9_gggaa(T24, T31, T32, T65, T33, permA_out_ga(T65, T33)) → pH_out_gggaa(T24, T31, T32, T65, T33)
U7_aaaggaa(T31, T26, T32, T25, T24, X9, T33, pH_out_gggaa(T24, T31, T32, X9, T33)) → pB_out_aaaggaa(T31, T26, T32, T25, T24, X9, T33)
U1_ga(T24, T25, T26, T27, pB_out_aaaggaa(X43, T26, X44, T25, T24, X9, T27)) → permA_out_ga(.(T24, T25), .(T26, T27))
APP2D_IN_AAAG(.(T50, X92), T52, X93, .(T50, T51)) → APP2D_IN_AAAG(X92, T52, X93, T51)
APP2D_IN_AAAG(.(T50, T51)) → APP2D_IN_AAAG(T51)
From the DPs we obtained the following set of size-change graphs:
PERMA_IN_GA(.(T24, T25), .(T26, T27)) → PB_IN_AAAGGAA(X43, T26, X44, T25, T24, X9, T27)
PB_IN_AAAGGAA(T31, T26, T32, T25, T24, X9, T33) → U6_AAAGGAA(T31, T26, T32, T25, T24, X9, T33, app2D_in_aaag(T31, T26, T32, T25))
U6_AAAGGAA(T31, T26, T32, T25, T24, X9, T33, app2D_out_aaag(T31, T26, T32, T25)) → PH_IN_GGGAA(T24, T31, T32, X9, T33)
PH_IN_GGGAA(T24, T31, T32, T65, T33) → U8_GGGAA(T24, T31, T32, T65, T33, app1F_in_ggga(T24, T31, T32, T65))
U8_GGGAA(T24, T31, T32, T65, T33, app1F_out_ggga(T24, T31, T32, T65)) → PERMA_IN_GA(T65, T33)
PERMA_IN_GA(.(T125, T126), .(T125, T127)) → PC_IN_GAA(T126, X9, T127)
PC_IN_GAA(T126, T128, T127) → U10_GAA(T126, T128, T127, app1G_in_ga(T126, T128))
U10_GAA(T126, T128, T127, app1G_out_ga(T126, T128)) → PERMA_IN_GA(T128, T127)
permA_in_ga(.(T24, T25), .(T26, T27)) → U1_ga(T24, T25, T26, T27, pB_in_aaaggaa(X43, T26, X44, T25, T24, X9, T27))
pB_in_aaaggaa(T31, T26, T32, T25, T24, X9, T33) → U6_aaaggaa(T31, T26, T32, T25, T24, X9, T33, app2D_in_aaag(T31, T26, T32, T25))
app2D_in_aaag(.(T50, X92), T52, X93, .(T50, T51)) → U3_aaag(T50, X92, T52, X93, T51, app2D_in_aaag(X92, T52, X93, T51))
app2D_in_aaag([], T60, T61, .(T60, T61)) → app2D_out_aaag([], T60, T61, .(T60, T61))
U3_aaag(T50, X92, T52, X93, T51, app2D_out_aaag(X92, T52, X93, T51)) → app2D_out_aaag(.(T50, X92), T52, X93, .(T50, T51))
U6_aaaggaa(T31, T26, T32, T25, T24, X9, T33, app2D_out_aaag(T31, T26, T32, T25)) → U7_aaaggaa(T31, T26, T32, T25, T24, X9, T33, pH_in_gggaa(T24, T31, T32, X9, T33))
pH_in_gggaa(T24, T31, T32, T65, T33) → U8_gggaa(T24, T31, T32, T65, T33, app1F_in_ggga(T24, T31, T32, T65))
app1F_in_ggga(T87, T88, T89, .(T87, X151)) → U5_ggga(T87, T88, T89, X151, app1E_in_gga(T88, T89, X151))
app1E_in_gga(.(T105, T106), T107, .(T105, X181)) → U4_gga(T105, T106, T107, X181, app1E_in_gga(T106, T107, X181))
app1E_in_gga([], T113, T113) → app1E_out_gga([], T113, T113)
U4_gga(T105, T106, T107, X181, app1E_out_gga(T106, T107, X181)) → app1E_out_gga(.(T105, T106), T107, .(T105, X181))
U5_ggga(T87, T88, T89, X151, app1E_out_gga(T88, T89, X151)) → app1F_out_ggga(T87, T88, T89, .(T87, X151))
U8_gggaa(T24, T31, T32, T65, T33, app1F_out_ggga(T24, T31, T32, T65)) → U9_gggaa(T24, T31, T32, T65, T33, permA_in_ga(T65, T33))
permA_in_ga(.(T125, T126), .(T125, T127)) → U2_ga(T125, T126, T127, pC_in_gaa(T126, X9, T127))
pC_in_gaa(T126, T128, T127) → U10_gaa(T126, T128, T127, app1G_in_ga(T126, T128))
app1G_in_ga(T131, T131) → app1G_out_ga(T131, T131)
U10_gaa(T126, T128, T127, app1G_out_ga(T126, T128)) → U11_gaa(T126, T128, T127, permA_in_ga(T128, T127))
permA_in_ga([], []) → permA_out_ga([], [])
U11_gaa(T126, T128, T127, permA_out_ga(T128, T127)) → pC_out_gaa(T126, T128, T127)
U2_ga(T125, T126, T127, pC_out_gaa(T126, X9, T127)) → permA_out_ga(.(T125, T126), .(T125, T127))
U9_gggaa(T24, T31, T32, T65, T33, permA_out_ga(T65, T33)) → pH_out_gggaa(T24, T31, T32, T65, T33)
U7_aaaggaa(T31, T26, T32, T25, T24, X9, T33, pH_out_gggaa(T24, T31, T32, X9, T33)) → pB_out_aaaggaa(T31, T26, T32, T25, T24, X9, T33)
U1_ga(T24, T25, T26, T27, pB_out_aaaggaa(X43, T26, X44, T25, T24, X9, T27)) → permA_out_ga(.(T24, T25), .(T26, T27))
PERMA_IN_GA(.(T24, T25), .(T26, T27)) → PB_IN_AAAGGAA(X43, T26, X44, T25, T24, X9, T27)
PB_IN_AAAGGAA(T31, T26, T32, T25, T24, X9, T33) → U6_AAAGGAA(T31, T26, T32, T25, T24, X9, T33, app2D_in_aaag(T31, T26, T32, T25))
U6_AAAGGAA(T31, T26, T32, T25, T24, X9, T33, app2D_out_aaag(T31, T26, T32, T25)) → PH_IN_GGGAA(T24, T31, T32, X9, T33)
PH_IN_GGGAA(T24, T31, T32, T65, T33) → U8_GGGAA(T24, T31, T32, T65, T33, app1F_in_ggga(T24, T31, T32, T65))
U8_GGGAA(T24, T31, T32, T65, T33, app1F_out_ggga(T24, T31, T32, T65)) → PERMA_IN_GA(T65, T33)
PERMA_IN_GA(.(T125, T126), .(T125, T127)) → PC_IN_GAA(T126, X9, T127)
PC_IN_GAA(T126, T128, T127) → U10_GAA(T126, T128, T127, app1G_in_ga(T126, T128))
U10_GAA(T126, T128, T127, app1G_out_ga(T126, T128)) → PERMA_IN_GA(T128, T127)
app2D_in_aaag(.(T50, X92), T52, X93, .(T50, T51)) → U3_aaag(T50, X92, T52, X93, T51, app2D_in_aaag(X92, T52, X93, T51))
app2D_in_aaag([], T60, T61, .(T60, T61)) → app2D_out_aaag([], T60, T61, .(T60, T61))
app1F_in_ggga(T87, T88, T89, .(T87, X151)) → U5_ggga(T87, T88, T89, X151, app1E_in_gga(T88, T89, X151))
app1G_in_ga(T131, T131) → app1G_out_ga(T131, T131)
U3_aaag(T50, X92, T52, X93, T51, app2D_out_aaag(X92, T52, X93, T51)) → app2D_out_aaag(.(T50, X92), T52, X93, .(T50, T51))
U5_ggga(T87, T88, T89, X151, app1E_out_gga(T88, T89, X151)) → app1F_out_ggga(T87, T88, T89, .(T87, X151))
app1E_in_gga(.(T105, T106), T107, .(T105, X181)) → U4_gga(T105, T106, T107, X181, app1E_in_gga(T106, T107, X181))
app1E_in_gga([], T113, T113) → app1E_out_gga([], T113, T113)
U4_gga(T105, T106, T107, X181, app1E_out_gga(T106, T107, X181)) → app1E_out_gga(.(T105, T106), T107, .(T105, X181))
PERMA_IN_GA(.(T24, T25)) → PB_IN_AAAGGAA(T25, T24)
PB_IN_AAAGGAA(T25, T24) → U6_AAAGGAA(T25, T24, app2D_in_aaag(T25))
U6_AAAGGAA(T25, T24, app2D_out_aaag(T31, T26, T32, T25)) → PH_IN_GGGAA(T24, T31, T32)
PH_IN_GGGAA(T24, T31, T32) → U8_GGGAA(T24, T31, T32, app1F_in_ggga(T24, T31, T32))
U8_GGGAA(T24, T31, T32, app1F_out_ggga(T24, T31, T32, T65)) → PERMA_IN_GA(T65)
PERMA_IN_GA(.(T125, T126)) → PC_IN_GAA(T126)
PC_IN_GAA(T126) → U10_GAA(T126, app1G_in_ga(T126))
U10_GAA(T126, app1G_out_ga(T126, T128)) → PERMA_IN_GA(T128)
app2D_in_aaag(.(T50, T51)) → U3_aaag(T50, T51, app2D_in_aaag(T51))
app2D_in_aaag(.(T60, T61)) → app2D_out_aaag([], T60, T61, .(T60, T61))
app1F_in_ggga(T87, T88, T89) → U5_ggga(T87, T88, T89, app1E_in_gga(T88, T89))
app1G_in_ga(T131) → app1G_out_ga(T131, T131)
U3_aaag(T50, T51, app2D_out_aaag(X92, T52, X93, T51)) → app2D_out_aaag(.(T50, X92), T52, X93, .(T50, T51))
U5_ggga(T87, T88, T89, app1E_out_gga(T88, T89, X151)) → app1F_out_ggga(T87, T88, T89, .(T87, X151))
app1E_in_gga(.(T105, T106), T107) → U4_gga(T105, T106, T107, app1E_in_gga(T106, T107))
app1E_in_gga([], T113) → app1E_out_gga([], T113, T113)
U4_gga(T105, T106, T107, app1E_out_gga(T106, T107, X181)) → app1E_out_gga(.(T105, T106), T107, .(T105, X181))
app2D_in_aaag(x0)
app1F_in_ggga(x0, x1, x2)
app1G_in_ga(x0)
U3_aaag(x0, x1, x2)
U5_ggga(x0, x1, x2, x3)
app1E_in_gga(x0, x1)
U4_gga(x0, x1, x2, x3)
PH_IN_GGGAA(T24, T31, T32) → U8_GGGAA(T24, T31, T32, U5_ggga(T24, T31, T32, app1E_in_gga(T31, T32)))
PERMA_IN_GA(.(T24, T25)) → PB_IN_AAAGGAA(T25, T24)
PB_IN_AAAGGAA(T25, T24) → U6_AAAGGAA(T25, T24, app2D_in_aaag(T25))
U6_AAAGGAA(T25, T24, app2D_out_aaag(T31, T26, T32, T25)) → PH_IN_GGGAA(T24, T31, T32)
U8_GGGAA(T24, T31, T32, app1F_out_ggga(T24, T31, T32, T65)) → PERMA_IN_GA(T65)
PERMA_IN_GA(.(T125, T126)) → PC_IN_GAA(T126)
PC_IN_GAA(T126) → U10_GAA(T126, app1G_in_ga(T126))
U10_GAA(T126, app1G_out_ga(T126, T128)) → PERMA_IN_GA(T128)
PH_IN_GGGAA(T24, T31, T32) → U8_GGGAA(T24, T31, T32, U5_ggga(T24, T31, T32, app1E_in_gga(T31, T32)))
app2D_in_aaag(.(T50, T51)) → U3_aaag(T50, T51, app2D_in_aaag(T51))
app2D_in_aaag(.(T60, T61)) → app2D_out_aaag([], T60, T61, .(T60, T61))
app1F_in_ggga(T87, T88, T89) → U5_ggga(T87, T88, T89, app1E_in_gga(T88, T89))
app1G_in_ga(T131) → app1G_out_ga(T131, T131)
U3_aaag(T50, T51, app2D_out_aaag(X92, T52, X93, T51)) → app2D_out_aaag(.(T50, X92), T52, X93, .(T50, T51))
U5_ggga(T87, T88, T89, app1E_out_gga(T88, T89, X151)) → app1F_out_ggga(T87, T88, T89, .(T87, X151))
app1E_in_gga(.(T105, T106), T107) → U4_gga(T105, T106, T107, app1E_in_gga(T106, T107))
app1E_in_gga([], T113) → app1E_out_gga([], T113, T113)
U4_gga(T105, T106, T107, app1E_out_gga(T106, T107, X181)) → app1E_out_gga(.(T105, T106), T107, .(T105, X181))
app2D_in_aaag(x0)
app1F_in_ggga(x0, x1, x2)
app1G_in_ga(x0)
U3_aaag(x0, x1, x2)
U5_ggga(x0, x1, x2, x3)
app1E_in_gga(x0, x1)
U4_gga(x0, x1, x2, x3)
PERMA_IN_GA(.(T24, T25)) → PB_IN_AAAGGAA(T25, T24)
PB_IN_AAAGGAA(T25, T24) → U6_AAAGGAA(T25, T24, app2D_in_aaag(T25))
U6_AAAGGAA(T25, T24, app2D_out_aaag(T31, T26, T32, T25)) → PH_IN_GGGAA(T24, T31, T32)
U8_GGGAA(T24, T31, T32, app1F_out_ggga(T24, T31, T32, T65)) → PERMA_IN_GA(T65)
PERMA_IN_GA(.(T125, T126)) → PC_IN_GAA(T126)
PC_IN_GAA(T126) → U10_GAA(T126, app1G_in_ga(T126))
U10_GAA(T126, app1G_out_ga(T126, T128)) → PERMA_IN_GA(T128)
PH_IN_GGGAA(T24, T31, T32) → U8_GGGAA(T24, T31, T32, U5_ggga(T24, T31, T32, app1E_in_gga(T31, T32)))
app1E_in_gga(.(T105, T106), T107) → U4_gga(T105, T106, T107, app1E_in_gga(T106, T107))
app1E_in_gga([], T113) → app1E_out_gga([], T113, T113)
U5_ggga(T87, T88, T89, app1E_out_gga(T88, T89, X151)) → app1F_out_ggga(T87, T88, T89, .(T87, X151))
U4_gga(T105, T106, T107, app1E_out_gga(T106, T107, X181)) → app1E_out_gga(.(T105, T106), T107, .(T105, X181))
app1G_in_ga(T131) → app1G_out_ga(T131, T131)
app2D_in_aaag(.(T50, T51)) → U3_aaag(T50, T51, app2D_in_aaag(T51))
app2D_in_aaag(.(T60, T61)) → app2D_out_aaag([], T60, T61, .(T60, T61))
U3_aaag(T50, T51, app2D_out_aaag(X92, T52, X93, T51)) → app2D_out_aaag(.(T50, X92), T52, X93, .(T50, T51))
app2D_in_aaag(x0)
app1F_in_ggga(x0, x1, x2)
app1G_in_ga(x0)
U3_aaag(x0, x1, x2)
U5_ggga(x0, x1, x2, x3)
app1E_in_gga(x0, x1)
U4_gga(x0, x1, x2, x3)
app1F_in_ggga(x0, x1, x2)
PERMA_IN_GA(.(T24, T25)) → PB_IN_AAAGGAA(T25, T24)
PB_IN_AAAGGAA(T25, T24) → U6_AAAGGAA(T25, T24, app2D_in_aaag(T25))
U6_AAAGGAA(T25, T24, app2D_out_aaag(T31, T26, T32, T25)) → PH_IN_GGGAA(T24, T31, T32)
U8_GGGAA(T24, T31, T32, app1F_out_ggga(T24, T31, T32, T65)) → PERMA_IN_GA(T65)
PERMA_IN_GA(.(T125, T126)) → PC_IN_GAA(T126)
PC_IN_GAA(T126) → U10_GAA(T126, app1G_in_ga(T126))
U10_GAA(T126, app1G_out_ga(T126, T128)) → PERMA_IN_GA(T128)
PH_IN_GGGAA(T24, T31, T32) → U8_GGGAA(T24, T31, T32, U5_ggga(T24, T31, T32, app1E_in_gga(T31, T32)))
app1E_in_gga(.(T105, T106), T107) → U4_gga(T105, T106, T107, app1E_in_gga(T106, T107))
app1E_in_gga([], T113) → app1E_out_gga([], T113, T113)
U5_ggga(T87, T88, T89, app1E_out_gga(T88, T89, X151)) → app1F_out_ggga(T87, T88, T89, .(T87, X151))
U4_gga(T105, T106, T107, app1E_out_gga(T106, T107, X181)) → app1E_out_gga(.(T105, T106), T107, .(T105, X181))
app1G_in_ga(T131) → app1G_out_ga(T131, T131)
app2D_in_aaag(.(T50, T51)) → U3_aaag(T50, T51, app2D_in_aaag(T51))
app2D_in_aaag(.(T60, T61)) → app2D_out_aaag([], T60, T61, .(T60, T61))
U3_aaag(T50, T51, app2D_out_aaag(X92, T52, X93, T51)) → app2D_out_aaag(.(T50, X92), T52, X93, .(T50, T51))
app2D_in_aaag(x0)
app1G_in_ga(x0)
U3_aaag(x0, x1, x2)
U5_ggga(x0, x1, x2, x3)
app1E_in_gga(x0, x1)
U4_gga(x0, x1, x2, x3)
PC_IN_GAA(T126) → U10_GAA(T126, app1G_out_ga(T126, T126))
PERMA_IN_GA(.(T24, T25)) → PB_IN_AAAGGAA(T25, T24)
PB_IN_AAAGGAA(T25, T24) → U6_AAAGGAA(T25, T24, app2D_in_aaag(T25))
U6_AAAGGAA(T25, T24, app2D_out_aaag(T31, T26, T32, T25)) → PH_IN_GGGAA(T24, T31, T32)
U8_GGGAA(T24, T31, T32, app1F_out_ggga(T24, T31, T32, T65)) → PERMA_IN_GA(T65)
PERMA_IN_GA(.(T125, T126)) → PC_IN_GAA(T126)
U10_GAA(T126, app1G_out_ga(T126, T128)) → PERMA_IN_GA(T128)
PH_IN_GGGAA(T24, T31, T32) → U8_GGGAA(T24, T31, T32, U5_ggga(T24, T31, T32, app1E_in_gga(T31, T32)))
PC_IN_GAA(T126) → U10_GAA(T126, app1G_out_ga(T126, T126))
app1E_in_gga(.(T105, T106), T107) → U4_gga(T105, T106, T107, app1E_in_gga(T106, T107))
app1E_in_gga([], T113) → app1E_out_gga([], T113, T113)
U5_ggga(T87, T88, T89, app1E_out_gga(T88, T89, X151)) → app1F_out_ggga(T87, T88, T89, .(T87, X151))
U4_gga(T105, T106, T107, app1E_out_gga(T106, T107, X181)) → app1E_out_gga(.(T105, T106), T107, .(T105, X181))
app1G_in_ga(T131) → app1G_out_ga(T131, T131)
app2D_in_aaag(.(T50, T51)) → U3_aaag(T50, T51, app2D_in_aaag(T51))
app2D_in_aaag(.(T60, T61)) → app2D_out_aaag([], T60, T61, .(T60, T61))
U3_aaag(T50, T51, app2D_out_aaag(X92, T52, X93, T51)) → app2D_out_aaag(.(T50, X92), T52, X93, .(T50, T51))
app2D_in_aaag(x0)
app1G_in_ga(x0)
U3_aaag(x0, x1, x2)
U5_ggga(x0, x1, x2, x3)
app1E_in_gga(x0, x1)
U4_gga(x0, x1, x2, x3)
PERMA_IN_GA(.(T24, T25)) → PB_IN_AAAGGAA(T25, T24)
PB_IN_AAAGGAA(T25, T24) → U6_AAAGGAA(T25, T24, app2D_in_aaag(T25))
U6_AAAGGAA(T25, T24, app2D_out_aaag(T31, T26, T32, T25)) → PH_IN_GGGAA(T24, T31, T32)
U8_GGGAA(T24, T31, T32, app1F_out_ggga(T24, T31, T32, T65)) → PERMA_IN_GA(T65)
PERMA_IN_GA(.(T125, T126)) → PC_IN_GAA(T126)
U10_GAA(T126, app1G_out_ga(T126, T128)) → PERMA_IN_GA(T128)
PH_IN_GGGAA(T24, T31, T32) → U8_GGGAA(T24, T31, T32, U5_ggga(T24, T31, T32, app1E_in_gga(T31, T32)))
PC_IN_GAA(T126) → U10_GAA(T126, app1G_out_ga(T126, T126))
app1E_in_gga(.(T105, T106), T107) → U4_gga(T105, T106, T107, app1E_in_gga(T106, T107))
app1E_in_gga([], T113) → app1E_out_gga([], T113, T113)
U5_ggga(T87, T88, T89, app1E_out_gga(T88, T89, X151)) → app1F_out_ggga(T87, T88, T89, .(T87, X151))
U4_gga(T105, T106, T107, app1E_out_gga(T106, T107, X181)) → app1E_out_gga(.(T105, T106), T107, .(T105, X181))
app2D_in_aaag(.(T50, T51)) → U3_aaag(T50, T51, app2D_in_aaag(T51))
app2D_in_aaag(.(T60, T61)) → app2D_out_aaag([], T60, T61, .(T60, T61))
U3_aaag(T50, T51, app2D_out_aaag(X92, T52, X93, T51)) → app2D_out_aaag(.(T50, X92), T52, X93, .(T50, T51))
app2D_in_aaag(x0)
app1G_in_ga(x0)
U3_aaag(x0, x1, x2)
U5_ggga(x0, x1, x2, x3)
app1E_in_gga(x0, x1)
U4_gga(x0, x1, x2, x3)
app1G_in_ga(x0)
PERMA_IN_GA(.(T24, T25)) → PB_IN_AAAGGAA(T25, T24)
PB_IN_AAAGGAA(T25, T24) → U6_AAAGGAA(T25, T24, app2D_in_aaag(T25))
U6_AAAGGAA(T25, T24, app2D_out_aaag(T31, T26, T32, T25)) → PH_IN_GGGAA(T24, T31, T32)
U8_GGGAA(T24, T31, T32, app1F_out_ggga(T24, T31, T32, T65)) → PERMA_IN_GA(T65)
PERMA_IN_GA(.(T125, T126)) → PC_IN_GAA(T126)
U10_GAA(T126, app1G_out_ga(T126, T128)) → PERMA_IN_GA(T128)
PH_IN_GGGAA(T24, T31, T32) → U8_GGGAA(T24, T31, T32, U5_ggga(T24, T31, T32, app1E_in_gga(T31, T32)))
PC_IN_GAA(T126) → U10_GAA(T126, app1G_out_ga(T126, T126))
app1E_in_gga(.(T105, T106), T107) → U4_gga(T105, T106, T107, app1E_in_gga(T106, T107))
app1E_in_gga([], T113) → app1E_out_gga([], T113, T113)
U5_ggga(T87, T88, T89, app1E_out_gga(T88, T89, X151)) → app1F_out_ggga(T87, T88, T89, .(T87, X151))
U4_gga(T105, T106, T107, app1E_out_gga(T106, T107, X181)) → app1E_out_gga(.(T105, T106), T107, .(T105, X181))
app2D_in_aaag(.(T50, T51)) → U3_aaag(T50, T51, app2D_in_aaag(T51))
app2D_in_aaag(.(T60, T61)) → app2D_out_aaag([], T60, T61, .(T60, T61))
U3_aaag(T50, T51, app2D_out_aaag(X92, T52, X93, T51)) → app2D_out_aaag(.(T50, X92), T52, X93, .(T50, T51))
app2D_in_aaag(x0)
U3_aaag(x0, x1, x2)
U5_ggga(x0, x1, x2, x3)
app1E_in_gga(x0, x1)
U4_gga(x0, x1, x2, x3)
U10_GAA(z0, app1G_out_ga(z0, z0)) → PERMA_IN_GA(z0)
PERMA_IN_GA(.(T24, T25)) → PB_IN_AAAGGAA(T25, T24)
PB_IN_AAAGGAA(T25, T24) → U6_AAAGGAA(T25, T24, app2D_in_aaag(T25))
U6_AAAGGAA(T25, T24, app2D_out_aaag(T31, T26, T32, T25)) → PH_IN_GGGAA(T24, T31, T32)
U8_GGGAA(T24, T31, T32, app1F_out_ggga(T24, T31, T32, T65)) → PERMA_IN_GA(T65)
PERMA_IN_GA(.(T125, T126)) → PC_IN_GAA(T126)
PH_IN_GGGAA(T24, T31, T32) → U8_GGGAA(T24, T31, T32, U5_ggga(T24, T31, T32, app1E_in_gga(T31, T32)))
PC_IN_GAA(T126) → U10_GAA(T126, app1G_out_ga(T126, T126))
U10_GAA(z0, app1G_out_ga(z0, z0)) → PERMA_IN_GA(z0)
app1E_in_gga(.(T105, T106), T107) → U4_gga(T105, T106, T107, app1E_in_gga(T106, T107))
app1E_in_gga([], T113) → app1E_out_gga([], T113, T113)
U5_ggga(T87, T88, T89, app1E_out_gga(T88, T89, X151)) → app1F_out_ggga(T87, T88, T89, .(T87, X151))
U4_gga(T105, T106, T107, app1E_out_gga(T106, T107, X181)) → app1E_out_gga(.(T105, T106), T107, .(T105, X181))
app2D_in_aaag(.(T50, T51)) → U3_aaag(T50, T51, app2D_in_aaag(T51))
app2D_in_aaag(.(T60, T61)) → app2D_out_aaag([], T60, T61, .(T60, T61))
U3_aaag(T50, T51, app2D_out_aaag(X92, T52, X93, T51)) → app2D_out_aaag(.(T50, X92), T52, X93, .(T50, T51))
app2D_in_aaag(x0)
U3_aaag(x0, x1, x2)
U5_ggga(x0, x1, x2, x3)
app1E_in_gga(x0, x1)
U4_gga(x0, x1, x2, x3)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PB_IN_AAAGGAA(T25, T24) → U6_AAAGGAA(T25, T24, app2D_in_aaag(T25))
U10_GAA(z0, app1G_out_ga(z0, z0)) → PERMA_IN_GA(z0)
POL(.(x1, x2)) = 1 + x2
POL(PB_IN_AAAGGAA(x1, x2)) = 1 + x1
POL(PC_IN_GAA(x1)) = 1 + x1
POL(PERMA_IN_GA(x1)) = x1
POL(PH_IN_GGGAA(x1, x2, x3)) = x2 + x3
POL(U10_GAA(x1, x2)) = x2
POL(U3_aaag(x1, x2, x3)) = 1 + x3
POL(U4_gga(x1, x2, x3, x4)) = 1 + x4
POL(U5_ggga(x1, x2, x3, x4)) = x4
POL(U6_AAAGGAA(x1, x2, x3)) = x3
POL(U8_GGGAA(x1, x2, x3, x4)) = x4
POL([]) = 1
POL(app1E_in_gga(x1, x2)) = x1 + x2
POL(app1E_out_gga(x1, x2, x3)) = 1 + x3
POL(app1F_out_ggga(x1, x2, x3, x4)) = x4
POL(app1G_out_ga(x1, x2)) = 1 + x2
POL(app2D_in_aaag(x1)) = x1
POL(app2D_out_aaag(x1, x2, x3, x4)) = x1 + x3
app2D_in_aaag(.(T50, T51)) → U3_aaag(T50, T51, app2D_in_aaag(T51))
app2D_in_aaag(.(T60, T61)) → app2D_out_aaag([], T60, T61, .(T60, T61))
app1E_in_gga(.(T105, T106), T107) → U4_gga(T105, T106, T107, app1E_in_gga(T106, T107))
app1E_in_gga([], T113) → app1E_out_gga([], T113, T113)
U5_ggga(T87, T88, T89, app1E_out_gga(T88, T89, X151)) → app1F_out_ggga(T87, T88, T89, .(T87, X151))
U4_gga(T105, T106, T107, app1E_out_gga(T106, T107, X181)) → app1E_out_gga(.(T105, T106), T107, .(T105, X181))
U3_aaag(T50, T51, app2D_out_aaag(X92, T52, X93, T51)) → app2D_out_aaag(.(T50, X92), T52, X93, .(T50, T51))
PERMA_IN_GA(.(T24, T25)) → PB_IN_AAAGGAA(T25, T24)
U6_AAAGGAA(T25, T24, app2D_out_aaag(T31, T26, T32, T25)) → PH_IN_GGGAA(T24, T31, T32)
U8_GGGAA(T24, T31, T32, app1F_out_ggga(T24, T31, T32, T65)) → PERMA_IN_GA(T65)
PERMA_IN_GA(.(T125, T126)) → PC_IN_GAA(T126)
PH_IN_GGGAA(T24, T31, T32) → U8_GGGAA(T24, T31, T32, U5_ggga(T24, T31, T32, app1E_in_gga(T31, T32)))
PC_IN_GAA(T126) → U10_GAA(T126, app1G_out_ga(T126, T126))
app1E_in_gga(.(T105, T106), T107) → U4_gga(T105, T106, T107, app1E_in_gga(T106, T107))
app1E_in_gga([], T113) → app1E_out_gga([], T113, T113)
U5_ggga(T87, T88, T89, app1E_out_gga(T88, T89, X151)) → app1F_out_ggga(T87, T88, T89, .(T87, X151))
U4_gga(T105, T106, T107, app1E_out_gga(T106, T107, X181)) → app1E_out_gga(.(T105, T106), T107, .(T105, X181))
app2D_in_aaag(.(T50, T51)) → U3_aaag(T50, T51, app2D_in_aaag(T51))
app2D_in_aaag(.(T60, T61)) → app2D_out_aaag([], T60, T61, .(T60, T61))
U3_aaag(T50, T51, app2D_out_aaag(X92, T52, X93, T51)) → app2D_out_aaag(.(T50, X92), T52, X93, .(T50, T51))
app2D_in_aaag(x0)
U3_aaag(x0, x1, x2)
U5_ggga(x0, x1, x2, x3)
app1E_in_gga(x0, x1)
U4_gga(x0, x1, x2, x3)