0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇐)
↳2 Prolog
↳3 PrologToPiTRSProof (⇐)
↳4 PiTRS
↳5 DependencyPairsProof (⇔)
↳6 PiDP
↳7 DependencyGraphProof (⇔)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔)
↳11 PiDP
↳12 PiDPToQDPProof (⇐)
↳13 QDP
↳14 QDPSizeChangeProof (⇔)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔)
↳18 PiDP
↳19 PiDPToQDPProof (⇐)
↳20 QDP
↳21 NonTerminationProof (⇔)
↳22 NO
↳23 PiDP
↳24 UsableRulesProof (⇔)
↳25 PiDP
↳26 PiDPToQDPProof (⇐)
↳27 QDP
↳28 QDPSizeChangeProof (⇔)
↳29 YES
↳30 PiDP
↳31 UsableRulesProof (⇔)
↳32 PiDP
↳33 PiDPToQDPProof (⇐)
↳34 QDP
↳35 NonTerminationProof (⇔)
↳36 NO
↳37 PiDP
↳38 UsableRulesProof (⇔)
↳39 PiDP
↳40 PiDPToQDPProof (⇐)
↳41 QDP
↳42 QDPSizeChangeProof (⇔)
↳43 YES
↳44 PrologToPiTRSProof (⇐)
↳45 PiTRS
↳46 DependencyPairsProof (⇔)
↳47 PiDP
↳48 DependencyGraphProof (⇔)
↳49 AND
↳50 PiDP
↳51 UsableRulesProof (⇔)
↳52 PiDP
↳53 PiDPToQDPProof (⇐)
↳54 QDP
↳55 QDPSizeChangeProof (⇔)
↳56 YES
↳57 PiDP
↳58 UsableRulesProof (⇔)
↳59 PiDP
↳60 PiDPToQDPProof (⇐)
↳61 QDP
↳62 NonTerminationProof (⇔)
↳63 NO
↳64 PiDP
↳65 UsableRulesProof (⇔)
↳66 PiDP
↳67 PiDPToQDPProof (⇐)
↳68 QDP
↳69 QDPSizeChangeProof (⇔)
↳70 YES
↳71 PiDP
↳72 UsableRulesProof (⇔)
↳73 PiDP
↳74 PiDPToQDPProof (⇐)
↳75 QDP
↳76 NonTerminationProof (⇔)
↳77 NO
↳78 PiDP
↳79 UsableRulesProof (⇔)
↳80 PiDP
↳81 PiDPToQDPProof (⇐)
↳82 QDP
↳83 QDPSizeChangeProof (⇔)
↳84 YES
shanoi1_in_gggga(s(0), T9, T10, T11, .(mv(T9, T11), [])) → shanoi1_out_gggga(s(0), T9, T10, T11, .(mv(T9, T11), []))
shanoi1_in_gggga(s(s(T31)), T18, T19, T20, T22) → U10_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T18, T20, T19, X26))
shanoi11_in_gggga(0, T57, T58, T59, .(mv(T57, T59), [])) → shanoi11_out_gggga(0, T57, T58, T59, .(mv(T57, T59), []))
shanoi11_in_gggga(s(T88), T69, T70, T71, X101) → U1_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, X98))
shanoi11_in_gggga(s(T88), T69, T70, T71, X101) → U2_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, T95))
U2_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U3_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T70, T69, T71, X99))
U3_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T70, T69, T71, X99)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U2_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_in_gggga(T88, T70, T69, T71, T108))
U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U5_gggga(T88, T69, T70, T71, X101, append28_in_aga(T95, .(mv(T69, T71), []), X100))
append28_in_aga([], T130, T130) → append28_out_aga([], T130, T130)
append28_in_aga(.(T137, T138), T139, .(T137, X178)) → U8_aga(T137, T138, T139, X178, append28_in_aga(T138, T139, X178))
U8_aga(T137, T138, T139, X178, append28_out_aga(T138, T139, X178)) → append28_out_aga(.(T137, T138), T139, .(T137, X178))
U5_gggga(T88, T69, T70, T71, X101, append28_out_aga(T95, .(mv(T69, T71), []), X100)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U6_gggga(T88, T69, T70, T71, X101, T108, append28_in_aga(T95, .(mv(T69, T71), []), T119))
U6_gggga(T88, T69, T70, T71, X101, T108, append28_out_aga(T95, .(mv(T69, T71), []), T119)) → U7_gggga(T88, T69, T70, T71, X101, append28_in_gaa(T119, T108, X101))
append28_in_gaa([], T130, T130) → append28_out_gaa([], T130, T130)
append28_in_gaa(.(T137, T138), T139, .(T137, X178)) → U8_gaa(T137, T138, T139, X178, append28_in_gaa(T138, T139, X178))
U8_gaa(T137, T138, T139, X178, append28_out_gaa(T138, T139, X178)) → append28_out_gaa(.(T137, T138), T139, .(T137, X178))
U7_gggga(T88, T69, T70, T71, X101, append28_out_gaa(T119, T108, X101)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U1_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, X98)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U10_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, X26)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
shanoi1_in_gggga(s(s(T31)), T18, T19, T20, T22) → U11_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T18, T20, T19, T38))
U11_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → U12_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T20, T18, T20, X27))
U12_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T20, T18, T20, X27)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
U11_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_in_gggga(T31, T20, T18, T20, T148))
U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → U14_gggga(T31, T18, T19, T20, T22, append40_in_aga(T38, .(mv(T18, T20), []), X28))
append40_in_aga([], T170, T170) → append40_out_aga([], T170, T170)
append40_in_aga(.(T179, T180), T181, .(T179, T183)) → U9_aga(T179, T180, T181, T183, append40_in_aga(T180, T181, T183))
U9_aga(T179, T180, T181, T183, append40_out_aga(T180, T181, T183)) → append40_out_aga(.(T179, T180), T181, .(T179, T183))
U14_gggga(T31, T18, T19, T20, T22, append40_out_aga(T38, .(mv(T18, T20), []), X28)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → U15_gggga(T31, T18, T19, T20, T22, T148, append40_in_aga(T38, .(mv(T18, T20), []), T159))
U15_gggga(T31, T18, T19, T20, T22, T148, append40_out_aga(T38, .(mv(T18, T20), []), T159)) → U16_gggga(T31, T18, T19, T20, T22, append40_in_gaa(T159, T148, T22))
append40_in_gaa([], T170, T170) → append40_out_gaa([], T170, T170)
append40_in_gaa(.(T179, T180), T181, .(T179, T183)) → U9_gaa(T179, T180, T181, T183, append40_in_gaa(T180, T181, T183))
U9_gaa(T179, T180, T181, T183, append40_out_gaa(T180, T181, T183)) → append40_out_gaa(.(T179, T180), T181, .(T179, T183))
U16_gggga(T31, T18, T19, T20, T22, append40_out_gaa(T159, T148, T22)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
shanoi1_in_gggga(s(0), T9, T10, T11, .(mv(T9, T11), [])) → shanoi1_out_gggga(s(0), T9, T10, T11, .(mv(T9, T11), []))
shanoi1_in_gggga(s(s(T31)), T18, T19, T20, T22) → U10_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T18, T20, T19, X26))
shanoi11_in_gggga(0, T57, T58, T59, .(mv(T57, T59), [])) → shanoi11_out_gggga(0, T57, T58, T59, .(mv(T57, T59), []))
shanoi11_in_gggga(s(T88), T69, T70, T71, X101) → U1_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, X98))
shanoi11_in_gggga(s(T88), T69, T70, T71, X101) → U2_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, T95))
U2_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U3_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T70, T69, T71, X99))
U3_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T70, T69, T71, X99)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U2_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_in_gggga(T88, T70, T69, T71, T108))
U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U5_gggga(T88, T69, T70, T71, X101, append28_in_aga(T95, .(mv(T69, T71), []), X100))
append28_in_aga([], T130, T130) → append28_out_aga([], T130, T130)
append28_in_aga(.(T137, T138), T139, .(T137, X178)) → U8_aga(T137, T138, T139, X178, append28_in_aga(T138, T139, X178))
U8_aga(T137, T138, T139, X178, append28_out_aga(T138, T139, X178)) → append28_out_aga(.(T137, T138), T139, .(T137, X178))
U5_gggga(T88, T69, T70, T71, X101, append28_out_aga(T95, .(mv(T69, T71), []), X100)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U6_gggga(T88, T69, T70, T71, X101, T108, append28_in_aga(T95, .(mv(T69, T71), []), T119))
U6_gggga(T88, T69, T70, T71, X101, T108, append28_out_aga(T95, .(mv(T69, T71), []), T119)) → U7_gggga(T88, T69, T70, T71, X101, append28_in_gaa(T119, T108, X101))
append28_in_gaa([], T130, T130) → append28_out_gaa([], T130, T130)
append28_in_gaa(.(T137, T138), T139, .(T137, X178)) → U8_gaa(T137, T138, T139, X178, append28_in_gaa(T138, T139, X178))
U8_gaa(T137, T138, T139, X178, append28_out_gaa(T138, T139, X178)) → append28_out_gaa(.(T137, T138), T139, .(T137, X178))
U7_gggga(T88, T69, T70, T71, X101, append28_out_gaa(T119, T108, X101)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U1_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, X98)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U10_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, X26)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
shanoi1_in_gggga(s(s(T31)), T18, T19, T20, T22) → U11_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T18, T20, T19, T38))
U11_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → U12_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T20, T18, T20, X27))
U12_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T20, T18, T20, X27)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
U11_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_in_gggga(T31, T20, T18, T20, T148))
U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → U14_gggga(T31, T18, T19, T20, T22, append40_in_aga(T38, .(mv(T18, T20), []), X28))
append40_in_aga([], T170, T170) → append40_out_aga([], T170, T170)
append40_in_aga(.(T179, T180), T181, .(T179, T183)) → U9_aga(T179, T180, T181, T183, append40_in_aga(T180, T181, T183))
U9_aga(T179, T180, T181, T183, append40_out_aga(T180, T181, T183)) → append40_out_aga(.(T179, T180), T181, .(T179, T183))
U14_gggga(T31, T18, T19, T20, T22, append40_out_aga(T38, .(mv(T18, T20), []), X28)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → U15_gggga(T31, T18, T19, T20, T22, T148, append40_in_aga(T38, .(mv(T18, T20), []), T159))
U15_gggga(T31, T18, T19, T20, T22, T148, append40_out_aga(T38, .(mv(T18, T20), []), T159)) → U16_gggga(T31, T18, T19, T20, T22, append40_in_gaa(T159, T148, T22))
append40_in_gaa([], T170, T170) → append40_out_gaa([], T170, T170)
append40_in_gaa(.(T179, T180), T181, .(T179, T183)) → U9_gaa(T179, T180, T181, T183, append40_in_gaa(T180, T181, T183))
U9_gaa(T179, T180, T181, T183, append40_out_gaa(T180, T181, T183)) → append40_out_gaa(.(T179, T180), T181, .(T179, T183))
U16_gggga(T31, T18, T19, T20, T22, append40_out_gaa(T159, T148, T22)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
SHANOI1_IN_GGGGA(s(s(T31)), T18, T19, T20, T22) → U10_GGGGA(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T18, T20, T19, X26))
SHANOI1_IN_GGGGA(s(s(T31)), T18, T19, T20, T22) → SHANOI11_IN_GGGGA(T31, T18, T20, T19, X26)
SHANOI11_IN_GGGGA(s(T88), T69, T70, T71, X101) → U1_GGGGA(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, X98))
SHANOI11_IN_GGGGA(s(T88), T69, T70, T71, X101) → SHANOI11_IN_GGGGA(T88, T69, T71, T70, X98)
SHANOI11_IN_GGGGA(s(T88), T69, T70, T71, X101) → U2_GGGGA(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, T95))
U2_GGGGA(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U3_GGGGA(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T70, T69, T71, X99))
U2_GGGGA(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → SHANOI11_IN_GGGGA(T88, T70, T69, T71, X99)
U2_GGGGA(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U4_GGGGA(T88, T69, T70, T71, X101, T95, shanoi11_in_gggga(T88, T70, T69, T71, T108))
U4_GGGGA(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U5_GGGGA(T88, T69, T70, T71, X101, append28_in_aga(T95, .(mv(T69, T71), []), X100))
U4_GGGGA(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → APPEND28_IN_AGA(T95, .(mv(T69, T71), []), X100)
APPEND28_IN_AGA(.(T137, T138), T139, .(T137, X178)) → U8_AGA(T137, T138, T139, X178, append28_in_aga(T138, T139, X178))
APPEND28_IN_AGA(.(T137, T138), T139, .(T137, X178)) → APPEND28_IN_AGA(T138, T139, X178)
U4_GGGGA(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U6_GGGGA(T88, T69, T70, T71, X101, T108, append28_in_aga(T95, .(mv(T69, T71), []), T119))
U6_GGGGA(T88, T69, T70, T71, X101, T108, append28_out_aga(T95, .(mv(T69, T71), []), T119)) → U7_GGGGA(T88, T69, T70, T71, X101, append28_in_gaa(T119, T108, X101))
U6_GGGGA(T88, T69, T70, T71, X101, T108, append28_out_aga(T95, .(mv(T69, T71), []), T119)) → APPEND28_IN_GAA(T119, T108, X101)
APPEND28_IN_GAA(.(T137, T138), T139, .(T137, X178)) → U8_GAA(T137, T138, T139, X178, append28_in_gaa(T138, T139, X178))
APPEND28_IN_GAA(.(T137, T138), T139, .(T137, X178)) → APPEND28_IN_GAA(T138, T139, X178)
SHANOI1_IN_GGGGA(s(s(T31)), T18, T19, T20, T22) → U11_GGGGA(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T18, T20, T19, T38))
U11_GGGGA(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → U12_GGGGA(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T20, T18, T20, X27))
U11_GGGGA(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → SHANOI11_IN_GGGGA(T31, T20, T18, T20, X27)
U11_GGGGA(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → U13_GGGGA(T31, T18, T19, T20, T22, T38, shanoi11_in_gggga(T31, T20, T18, T20, T148))
U13_GGGGA(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → U14_GGGGA(T31, T18, T19, T20, T22, append40_in_aga(T38, .(mv(T18, T20), []), X28))
U13_GGGGA(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → APPEND40_IN_AGA(T38, .(mv(T18, T20), []), X28)
APPEND40_IN_AGA(.(T179, T180), T181, .(T179, T183)) → U9_AGA(T179, T180, T181, T183, append40_in_aga(T180, T181, T183))
APPEND40_IN_AGA(.(T179, T180), T181, .(T179, T183)) → APPEND40_IN_AGA(T180, T181, T183)
U13_GGGGA(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → U15_GGGGA(T31, T18, T19, T20, T22, T148, append40_in_aga(T38, .(mv(T18, T20), []), T159))
U15_GGGGA(T31, T18, T19, T20, T22, T148, append40_out_aga(T38, .(mv(T18, T20), []), T159)) → U16_GGGGA(T31, T18, T19, T20, T22, append40_in_gaa(T159, T148, T22))
U15_GGGGA(T31, T18, T19, T20, T22, T148, append40_out_aga(T38, .(mv(T18, T20), []), T159)) → APPEND40_IN_GAA(T159, T148, T22)
APPEND40_IN_GAA(.(T179, T180), T181, .(T179, T183)) → U9_GAA(T179, T180, T181, T183, append40_in_gaa(T180, T181, T183))
APPEND40_IN_GAA(.(T179, T180), T181, .(T179, T183)) → APPEND40_IN_GAA(T180, T181, T183)
shanoi1_in_gggga(s(0), T9, T10, T11, .(mv(T9, T11), [])) → shanoi1_out_gggga(s(0), T9, T10, T11, .(mv(T9, T11), []))
shanoi1_in_gggga(s(s(T31)), T18, T19, T20, T22) → U10_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T18, T20, T19, X26))
shanoi11_in_gggga(0, T57, T58, T59, .(mv(T57, T59), [])) → shanoi11_out_gggga(0, T57, T58, T59, .(mv(T57, T59), []))
shanoi11_in_gggga(s(T88), T69, T70, T71, X101) → U1_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, X98))
shanoi11_in_gggga(s(T88), T69, T70, T71, X101) → U2_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, T95))
U2_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U3_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T70, T69, T71, X99))
U3_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T70, T69, T71, X99)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U2_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_in_gggga(T88, T70, T69, T71, T108))
U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U5_gggga(T88, T69, T70, T71, X101, append28_in_aga(T95, .(mv(T69, T71), []), X100))
append28_in_aga([], T130, T130) → append28_out_aga([], T130, T130)
append28_in_aga(.(T137, T138), T139, .(T137, X178)) → U8_aga(T137, T138, T139, X178, append28_in_aga(T138, T139, X178))
U8_aga(T137, T138, T139, X178, append28_out_aga(T138, T139, X178)) → append28_out_aga(.(T137, T138), T139, .(T137, X178))
U5_gggga(T88, T69, T70, T71, X101, append28_out_aga(T95, .(mv(T69, T71), []), X100)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U6_gggga(T88, T69, T70, T71, X101, T108, append28_in_aga(T95, .(mv(T69, T71), []), T119))
U6_gggga(T88, T69, T70, T71, X101, T108, append28_out_aga(T95, .(mv(T69, T71), []), T119)) → U7_gggga(T88, T69, T70, T71, X101, append28_in_gaa(T119, T108, X101))
append28_in_gaa([], T130, T130) → append28_out_gaa([], T130, T130)
append28_in_gaa(.(T137, T138), T139, .(T137, X178)) → U8_gaa(T137, T138, T139, X178, append28_in_gaa(T138, T139, X178))
U8_gaa(T137, T138, T139, X178, append28_out_gaa(T138, T139, X178)) → append28_out_gaa(.(T137, T138), T139, .(T137, X178))
U7_gggga(T88, T69, T70, T71, X101, append28_out_gaa(T119, T108, X101)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U1_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, X98)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U10_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, X26)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
shanoi1_in_gggga(s(s(T31)), T18, T19, T20, T22) → U11_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T18, T20, T19, T38))
U11_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → U12_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T20, T18, T20, X27))
U12_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T20, T18, T20, X27)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
U11_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_in_gggga(T31, T20, T18, T20, T148))
U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → U14_gggga(T31, T18, T19, T20, T22, append40_in_aga(T38, .(mv(T18, T20), []), X28))
append40_in_aga([], T170, T170) → append40_out_aga([], T170, T170)
append40_in_aga(.(T179, T180), T181, .(T179, T183)) → U9_aga(T179, T180, T181, T183, append40_in_aga(T180, T181, T183))
U9_aga(T179, T180, T181, T183, append40_out_aga(T180, T181, T183)) → append40_out_aga(.(T179, T180), T181, .(T179, T183))
U14_gggga(T31, T18, T19, T20, T22, append40_out_aga(T38, .(mv(T18, T20), []), X28)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → U15_gggga(T31, T18, T19, T20, T22, T148, append40_in_aga(T38, .(mv(T18, T20), []), T159))
U15_gggga(T31, T18, T19, T20, T22, T148, append40_out_aga(T38, .(mv(T18, T20), []), T159)) → U16_gggga(T31, T18, T19, T20, T22, append40_in_gaa(T159, T148, T22))
append40_in_gaa([], T170, T170) → append40_out_gaa([], T170, T170)
append40_in_gaa(.(T179, T180), T181, .(T179, T183)) → U9_gaa(T179, T180, T181, T183, append40_in_gaa(T180, T181, T183))
U9_gaa(T179, T180, T181, T183, append40_out_gaa(T180, T181, T183)) → append40_out_gaa(.(T179, T180), T181, .(T179, T183))
U16_gggga(T31, T18, T19, T20, T22, append40_out_gaa(T159, T148, T22)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
SHANOI1_IN_GGGGA(s(s(T31)), T18, T19, T20, T22) → U10_GGGGA(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T18, T20, T19, X26))
SHANOI1_IN_GGGGA(s(s(T31)), T18, T19, T20, T22) → SHANOI11_IN_GGGGA(T31, T18, T20, T19, X26)
SHANOI11_IN_GGGGA(s(T88), T69, T70, T71, X101) → U1_GGGGA(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, X98))
SHANOI11_IN_GGGGA(s(T88), T69, T70, T71, X101) → SHANOI11_IN_GGGGA(T88, T69, T71, T70, X98)
SHANOI11_IN_GGGGA(s(T88), T69, T70, T71, X101) → U2_GGGGA(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, T95))
U2_GGGGA(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U3_GGGGA(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T70, T69, T71, X99))
U2_GGGGA(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → SHANOI11_IN_GGGGA(T88, T70, T69, T71, X99)
U2_GGGGA(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U4_GGGGA(T88, T69, T70, T71, X101, T95, shanoi11_in_gggga(T88, T70, T69, T71, T108))
U4_GGGGA(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U5_GGGGA(T88, T69, T70, T71, X101, append28_in_aga(T95, .(mv(T69, T71), []), X100))
U4_GGGGA(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → APPEND28_IN_AGA(T95, .(mv(T69, T71), []), X100)
APPEND28_IN_AGA(.(T137, T138), T139, .(T137, X178)) → U8_AGA(T137, T138, T139, X178, append28_in_aga(T138, T139, X178))
APPEND28_IN_AGA(.(T137, T138), T139, .(T137, X178)) → APPEND28_IN_AGA(T138, T139, X178)
U4_GGGGA(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U6_GGGGA(T88, T69, T70, T71, X101, T108, append28_in_aga(T95, .(mv(T69, T71), []), T119))
U6_GGGGA(T88, T69, T70, T71, X101, T108, append28_out_aga(T95, .(mv(T69, T71), []), T119)) → U7_GGGGA(T88, T69, T70, T71, X101, append28_in_gaa(T119, T108, X101))
U6_GGGGA(T88, T69, T70, T71, X101, T108, append28_out_aga(T95, .(mv(T69, T71), []), T119)) → APPEND28_IN_GAA(T119, T108, X101)
APPEND28_IN_GAA(.(T137, T138), T139, .(T137, X178)) → U8_GAA(T137, T138, T139, X178, append28_in_gaa(T138, T139, X178))
APPEND28_IN_GAA(.(T137, T138), T139, .(T137, X178)) → APPEND28_IN_GAA(T138, T139, X178)
SHANOI1_IN_GGGGA(s(s(T31)), T18, T19, T20, T22) → U11_GGGGA(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T18, T20, T19, T38))
U11_GGGGA(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → U12_GGGGA(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T20, T18, T20, X27))
U11_GGGGA(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → SHANOI11_IN_GGGGA(T31, T20, T18, T20, X27)
U11_GGGGA(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → U13_GGGGA(T31, T18, T19, T20, T22, T38, shanoi11_in_gggga(T31, T20, T18, T20, T148))
U13_GGGGA(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → U14_GGGGA(T31, T18, T19, T20, T22, append40_in_aga(T38, .(mv(T18, T20), []), X28))
U13_GGGGA(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → APPEND40_IN_AGA(T38, .(mv(T18, T20), []), X28)
APPEND40_IN_AGA(.(T179, T180), T181, .(T179, T183)) → U9_AGA(T179, T180, T181, T183, append40_in_aga(T180, T181, T183))
APPEND40_IN_AGA(.(T179, T180), T181, .(T179, T183)) → APPEND40_IN_AGA(T180, T181, T183)
U13_GGGGA(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → U15_GGGGA(T31, T18, T19, T20, T22, T148, append40_in_aga(T38, .(mv(T18, T20), []), T159))
U15_GGGGA(T31, T18, T19, T20, T22, T148, append40_out_aga(T38, .(mv(T18, T20), []), T159)) → U16_GGGGA(T31, T18, T19, T20, T22, append40_in_gaa(T159, T148, T22))
U15_GGGGA(T31, T18, T19, T20, T22, T148, append40_out_aga(T38, .(mv(T18, T20), []), T159)) → APPEND40_IN_GAA(T159, T148, T22)
APPEND40_IN_GAA(.(T179, T180), T181, .(T179, T183)) → U9_GAA(T179, T180, T181, T183, append40_in_gaa(T180, T181, T183))
APPEND40_IN_GAA(.(T179, T180), T181, .(T179, T183)) → APPEND40_IN_GAA(T180, T181, T183)
shanoi1_in_gggga(s(0), T9, T10, T11, .(mv(T9, T11), [])) → shanoi1_out_gggga(s(0), T9, T10, T11, .(mv(T9, T11), []))
shanoi1_in_gggga(s(s(T31)), T18, T19, T20, T22) → U10_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T18, T20, T19, X26))
shanoi11_in_gggga(0, T57, T58, T59, .(mv(T57, T59), [])) → shanoi11_out_gggga(0, T57, T58, T59, .(mv(T57, T59), []))
shanoi11_in_gggga(s(T88), T69, T70, T71, X101) → U1_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, X98))
shanoi11_in_gggga(s(T88), T69, T70, T71, X101) → U2_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, T95))
U2_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U3_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T70, T69, T71, X99))
U3_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T70, T69, T71, X99)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U2_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_in_gggga(T88, T70, T69, T71, T108))
U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U5_gggga(T88, T69, T70, T71, X101, append28_in_aga(T95, .(mv(T69, T71), []), X100))
append28_in_aga([], T130, T130) → append28_out_aga([], T130, T130)
append28_in_aga(.(T137, T138), T139, .(T137, X178)) → U8_aga(T137, T138, T139, X178, append28_in_aga(T138, T139, X178))
U8_aga(T137, T138, T139, X178, append28_out_aga(T138, T139, X178)) → append28_out_aga(.(T137, T138), T139, .(T137, X178))
U5_gggga(T88, T69, T70, T71, X101, append28_out_aga(T95, .(mv(T69, T71), []), X100)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U6_gggga(T88, T69, T70, T71, X101, T108, append28_in_aga(T95, .(mv(T69, T71), []), T119))
U6_gggga(T88, T69, T70, T71, X101, T108, append28_out_aga(T95, .(mv(T69, T71), []), T119)) → U7_gggga(T88, T69, T70, T71, X101, append28_in_gaa(T119, T108, X101))
append28_in_gaa([], T130, T130) → append28_out_gaa([], T130, T130)
append28_in_gaa(.(T137, T138), T139, .(T137, X178)) → U8_gaa(T137, T138, T139, X178, append28_in_gaa(T138, T139, X178))
U8_gaa(T137, T138, T139, X178, append28_out_gaa(T138, T139, X178)) → append28_out_gaa(.(T137, T138), T139, .(T137, X178))
U7_gggga(T88, T69, T70, T71, X101, append28_out_gaa(T119, T108, X101)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U1_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, X98)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U10_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, X26)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
shanoi1_in_gggga(s(s(T31)), T18, T19, T20, T22) → U11_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T18, T20, T19, T38))
U11_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → U12_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T20, T18, T20, X27))
U12_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T20, T18, T20, X27)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
U11_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_in_gggga(T31, T20, T18, T20, T148))
U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → U14_gggga(T31, T18, T19, T20, T22, append40_in_aga(T38, .(mv(T18, T20), []), X28))
append40_in_aga([], T170, T170) → append40_out_aga([], T170, T170)
append40_in_aga(.(T179, T180), T181, .(T179, T183)) → U9_aga(T179, T180, T181, T183, append40_in_aga(T180, T181, T183))
U9_aga(T179, T180, T181, T183, append40_out_aga(T180, T181, T183)) → append40_out_aga(.(T179, T180), T181, .(T179, T183))
U14_gggga(T31, T18, T19, T20, T22, append40_out_aga(T38, .(mv(T18, T20), []), X28)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → U15_gggga(T31, T18, T19, T20, T22, T148, append40_in_aga(T38, .(mv(T18, T20), []), T159))
U15_gggga(T31, T18, T19, T20, T22, T148, append40_out_aga(T38, .(mv(T18, T20), []), T159)) → U16_gggga(T31, T18, T19, T20, T22, append40_in_gaa(T159, T148, T22))
append40_in_gaa([], T170, T170) → append40_out_gaa([], T170, T170)
append40_in_gaa(.(T179, T180), T181, .(T179, T183)) → U9_gaa(T179, T180, T181, T183, append40_in_gaa(T180, T181, T183))
U9_gaa(T179, T180, T181, T183, append40_out_gaa(T180, T181, T183)) → append40_out_gaa(.(T179, T180), T181, .(T179, T183))
U16_gggga(T31, T18, T19, T20, T22, append40_out_gaa(T159, T148, T22)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
APPEND40_IN_GAA(.(T179, T180), T181, .(T179, T183)) → APPEND40_IN_GAA(T180, T181, T183)
shanoi1_in_gggga(s(0), T9, T10, T11, .(mv(T9, T11), [])) → shanoi1_out_gggga(s(0), T9, T10, T11, .(mv(T9, T11), []))
shanoi1_in_gggga(s(s(T31)), T18, T19, T20, T22) → U10_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T18, T20, T19, X26))
shanoi11_in_gggga(0, T57, T58, T59, .(mv(T57, T59), [])) → shanoi11_out_gggga(0, T57, T58, T59, .(mv(T57, T59), []))
shanoi11_in_gggga(s(T88), T69, T70, T71, X101) → U1_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, X98))
shanoi11_in_gggga(s(T88), T69, T70, T71, X101) → U2_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, T95))
U2_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U3_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T70, T69, T71, X99))
U3_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T70, T69, T71, X99)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U2_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_in_gggga(T88, T70, T69, T71, T108))
U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U5_gggga(T88, T69, T70, T71, X101, append28_in_aga(T95, .(mv(T69, T71), []), X100))
append28_in_aga([], T130, T130) → append28_out_aga([], T130, T130)
append28_in_aga(.(T137, T138), T139, .(T137, X178)) → U8_aga(T137, T138, T139, X178, append28_in_aga(T138, T139, X178))
U8_aga(T137, T138, T139, X178, append28_out_aga(T138, T139, X178)) → append28_out_aga(.(T137, T138), T139, .(T137, X178))
U5_gggga(T88, T69, T70, T71, X101, append28_out_aga(T95, .(mv(T69, T71), []), X100)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U6_gggga(T88, T69, T70, T71, X101, T108, append28_in_aga(T95, .(mv(T69, T71), []), T119))
U6_gggga(T88, T69, T70, T71, X101, T108, append28_out_aga(T95, .(mv(T69, T71), []), T119)) → U7_gggga(T88, T69, T70, T71, X101, append28_in_gaa(T119, T108, X101))
append28_in_gaa([], T130, T130) → append28_out_gaa([], T130, T130)
append28_in_gaa(.(T137, T138), T139, .(T137, X178)) → U8_gaa(T137, T138, T139, X178, append28_in_gaa(T138, T139, X178))
U8_gaa(T137, T138, T139, X178, append28_out_gaa(T138, T139, X178)) → append28_out_gaa(.(T137, T138), T139, .(T137, X178))
U7_gggga(T88, T69, T70, T71, X101, append28_out_gaa(T119, T108, X101)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U1_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, X98)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U10_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, X26)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
shanoi1_in_gggga(s(s(T31)), T18, T19, T20, T22) → U11_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T18, T20, T19, T38))
U11_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → U12_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T20, T18, T20, X27))
U12_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T20, T18, T20, X27)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
U11_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_in_gggga(T31, T20, T18, T20, T148))
U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → U14_gggga(T31, T18, T19, T20, T22, append40_in_aga(T38, .(mv(T18, T20), []), X28))
append40_in_aga([], T170, T170) → append40_out_aga([], T170, T170)
append40_in_aga(.(T179, T180), T181, .(T179, T183)) → U9_aga(T179, T180, T181, T183, append40_in_aga(T180, T181, T183))
U9_aga(T179, T180, T181, T183, append40_out_aga(T180, T181, T183)) → append40_out_aga(.(T179, T180), T181, .(T179, T183))
U14_gggga(T31, T18, T19, T20, T22, append40_out_aga(T38, .(mv(T18, T20), []), X28)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → U15_gggga(T31, T18, T19, T20, T22, T148, append40_in_aga(T38, .(mv(T18, T20), []), T159))
U15_gggga(T31, T18, T19, T20, T22, T148, append40_out_aga(T38, .(mv(T18, T20), []), T159)) → U16_gggga(T31, T18, T19, T20, T22, append40_in_gaa(T159, T148, T22))
append40_in_gaa([], T170, T170) → append40_out_gaa([], T170, T170)
append40_in_gaa(.(T179, T180), T181, .(T179, T183)) → U9_gaa(T179, T180, T181, T183, append40_in_gaa(T180, T181, T183))
U9_gaa(T179, T180, T181, T183, append40_out_gaa(T180, T181, T183)) → append40_out_gaa(.(T179, T180), T181, .(T179, T183))
U16_gggga(T31, T18, T19, T20, T22, append40_out_gaa(T159, T148, T22)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
APPEND40_IN_GAA(.(T179, T180), T181, .(T179, T183)) → APPEND40_IN_GAA(T180, T181, T183)
APPEND40_IN_GAA(.(T180)) → APPEND40_IN_GAA(T180)
From the DPs we obtained the following set of size-change graphs:
APPEND40_IN_AGA(.(T179, T180), T181, .(T179, T183)) → APPEND40_IN_AGA(T180, T181, T183)
shanoi1_in_gggga(s(0), T9, T10, T11, .(mv(T9, T11), [])) → shanoi1_out_gggga(s(0), T9, T10, T11, .(mv(T9, T11), []))
shanoi1_in_gggga(s(s(T31)), T18, T19, T20, T22) → U10_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T18, T20, T19, X26))
shanoi11_in_gggga(0, T57, T58, T59, .(mv(T57, T59), [])) → shanoi11_out_gggga(0, T57, T58, T59, .(mv(T57, T59), []))
shanoi11_in_gggga(s(T88), T69, T70, T71, X101) → U1_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, X98))
shanoi11_in_gggga(s(T88), T69, T70, T71, X101) → U2_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, T95))
U2_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U3_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T70, T69, T71, X99))
U3_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T70, T69, T71, X99)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U2_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_in_gggga(T88, T70, T69, T71, T108))
U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U5_gggga(T88, T69, T70, T71, X101, append28_in_aga(T95, .(mv(T69, T71), []), X100))
append28_in_aga([], T130, T130) → append28_out_aga([], T130, T130)
append28_in_aga(.(T137, T138), T139, .(T137, X178)) → U8_aga(T137, T138, T139, X178, append28_in_aga(T138, T139, X178))
U8_aga(T137, T138, T139, X178, append28_out_aga(T138, T139, X178)) → append28_out_aga(.(T137, T138), T139, .(T137, X178))
U5_gggga(T88, T69, T70, T71, X101, append28_out_aga(T95, .(mv(T69, T71), []), X100)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U6_gggga(T88, T69, T70, T71, X101, T108, append28_in_aga(T95, .(mv(T69, T71), []), T119))
U6_gggga(T88, T69, T70, T71, X101, T108, append28_out_aga(T95, .(mv(T69, T71), []), T119)) → U7_gggga(T88, T69, T70, T71, X101, append28_in_gaa(T119, T108, X101))
append28_in_gaa([], T130, T130) → append28_out_gaa([], T130, T130)
append28_in_gaa(.(T137, T138), T139, .(T137, X178)) → U8_gaa(T137, T138, T139, X178, append28_in_gaa(T138, T139, X178))
U8_gaa(T137, T138, T139, X178, append28_out_gaa(T138, T139, X178)) → append28_out_gaa(.(T137, T138), T139, .(T137, X178))
U7_gggga(T88, T69, T70, T71, X101, append28_out_gaa(T119, T108, X101)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U1_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, X98)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U10_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, X26)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
shanoi1_in_gggga(s(s(T31)), T18, T19, T20, T22) → U11_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T18, T20, T19, T38))
U11_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → U12_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T20, T18, T20, X27))
U12_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T20, T18, T20, X27)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
U11_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_in_gggga(T31, T20, T18, T20, T148))
U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → U14_gggga(T31, T18, T19, T20, T22, append40_in_aga(T38, .(mv(T18, T20), []), X28))
append40_in_aga([], T170, T170) → append40_out_aga([], T170, T170)
append40_in_aga(.(T179, T180), T181, .(T179, T183)) → U9_aga(T179, T180, T181, T183, append40_in_aga(T180, T181, T183))
U9_aga(T179, T180, T181, T183, append40_out_aga(T180, T181, T183)) → append40_out_aga(.(T179, T180), T181, .(T179, T183))
U14_gggga(T31, T18, T19, T20, T22, append40_out_aga(T38, .(mv(T18, T20), []), X28)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → U15_gggga(T31, T18, T19, T20, T22, T148, append40_in_aga(T38, .(mv(T18, T20), []), T159))
U15_gggga(T31, T18, T19, T20, T22, T148, append40_out_aga(T38, .(mv(T18, T20), []), T159)) → U16_gggga(T31, T18, T19, T20, T22, append40_in_gaa(T159, T148, T22))
append40_in_gaa([], T170, T170) → append40_out_gaa([], T170, T170)
append40_in_gaa(.(T179, T180), T181, .(T179, T183)) → U9_gaa(T179, T180, T181, T183, append40_in_gaa(T180, T181, T183))
U9_gaa(T179, T180, T181, T183, append40_out_gaa(T180, T181, T183)) → append40_out_gaa(.(T179, T180), T181, .(T179, T183))
U16_gggga(T31, T18, T19, T20, T22, append40_out_gaa(T159, T148, T22)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
APPEND40_IN_AGA(.(T179, T180), T181, .(T179, T183)) → APPEND40_IN_AGA(T180, T181, T183)
APPEND40_IN_AGA(T181) → APPEND40_IN_AGA(T181)
APPEND28_IN_GAA(.(T137, T138), T139, .(T137, X178)) → APPEND28_IN_GAA(T138, T139, X178)
shanoi1_in_gggga(s(0), T9, T10, T11, .(mv(T9, T11), [])) → shanoi1_out_gggga(s(0), T9, T10, T11, .(mv(T9, T11), []))
shanoi1_in_gggga(s(s(T31)), T18, T19, T20, T22) → U10_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T18, T20, T19, X26))
shanoi11_in_gggga(0, T57, T58, T59, .(mv(T57, T59), [])) → shanoi11_out_gggga(0, T57, T58, T59, .(mv(T57, T59), []))
shanoi11_in_gggga(s(T88), T69, T70, T71, X101) → U1_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, X98))
shanoi11_in_gggga(s(T88), T69, T70, T71, X101) → U2_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, T95))
U2_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U3_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T70, T69, T71, X99))
U3_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T70, T69, T71, X99)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U2_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_in_gggga(T88, T70, T69, T71, T108))
U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U5_gggga(T88, T69, T70, T71, X101, append28_in_aga(T95, .(mv(T69, T71), []), X100))
append28_in_aga([], T130, T130) → append28_out_aga([], T130, T130)
append28_in_aga(.(T137, T138), T139, .(T137, X178)) → U8_aga(T137, T138, T139, X178, append28_in_aga(T138, T139, X178))
U8_aga(T137, T138, T139, X178, append28_out_aga(T138, T139, X178)) → append28_out_aga(.(T137, T138), T139, .(T137, X178))
U5_gggga(T88, T69, T70, T71, X101, append28_out_aga(T95, .(mv(T69, T71), []), X100)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U6_gggga(T88, T69, T70, T71, X101, T108, append28_in_aga(T95, .(mv(T69, T71), []), T119))
U6_gggga(T88, T69, T70, T71, X101, T108, append28_out_aga(T95, .(mv(T69, T71), []), T119)) → U7_gggga(T88, T69, T70, T71, X101, append28_in_gaa(T119, T108, X101))
append28_in_gaa([], T130, T130) → append28_out_gaa([], T130, T130)
append28_in_gaa(.(T137, T138), T139, .(T137, X178)) → U8_gaa(T137, T138, T139, X178, append28_in_gaa(T138, T139, X178))
U8_gaa(T137, T138, T139, X178, append28_out_gaa(T138, T139, X178)) → append28_out_gaa(.(T137, T138), T139, .(T137, X178))
U7_gggga(T88, T69, T70, T71, X101, append28_out_gaa(T119, T108, X101)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U1_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, X98)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U10_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, X26)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
shanoi1_in_gggga(s(s(T31)), T18, T19, T20, T22) → U11_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T18, T20, T19, T38))
U11_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → U12_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T20, T18, T20, X27))
U12_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T20, T18, T20, X27)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
U11_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_in_gggga(T31, T20, T18, T20, T148))
U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → U14_gggga(T31, T18, T19, T20, T22, append40_in_aga(T38, .(mv(T18, T20), []), X28))
append40_in_aga([], T170, T170) → append40_out_aga([], T170, T170)
append40_in_aga(.(T179, T180), T181, .(T179, T183)) → U9_aga(T179, T180, T181, T183, append40_in_aga(T180, T181, T183))
U9_aga(T179, T180, T181, T183, append40_out_aga(T180, T181, T183)) → append40_out_aga(.(T179, T180), T181, .(T179, T183))
U14_gggga(T31, T18, T19, T20, T22, append40_out_aga(T38, .(mv(T18, T20), []), X28)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → U15_gggga(T31, T18, T19, T20, T22, T148, append40_in_aga(T38, .(mv(T18, T20), []), T159))
U15_gggga(T31, T18, T19, T20, T22, T148, append40_out_aga(T38, .(mv(T18, T20), []), T159)) → U16_gggga(T31, T18, T19, T20, T22, append40_in_gaa(T159, T148, T22))
append40_in_gaa([], T170, T170) → append40_out_gaa([], T170, T170)
append40_in_gaa(.(T179, T180), T181, .(T179, T183)) → U9_gaa(T179, T180, T181, T183, append40_in_gaa(T180, T181, T183))
U9_gaa(T179, T180, T181, T183, append40_out_gaa(T180, T181, T183)) → append40_out_gaa(.(T179, T180), T181, .(T179, T183))
U16_gggga(T31, T18, T19, T20, T22, append40_out_gaa(T159, T148, T22)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
APPEND28_IN_GAA(.(T137, T138), T139, .(T137, X178)) → APPEND28_IN_GAA(T138, T139, X178)
APPEND28_IN_GAA(.(T138)) → APPEND28_IN_GAA(T138)
From the DPs we obtained the following set of size-change graphs:
APPEND28_IN_AGA(.(T137, T138), T139, .(T137, X178)) → APPEND28_IN_AGA(T138, T139, X178)
shanoi1_in_gggga(s(0), T9, T10, T11, .(mv(T9, T11), [])) → shanoi1_out_gggga(s(0), T9, T10, T11, .(mv(T9, T11), []))
shanoi1_in_gggga(s(s(T31)), T18, T19, T20, T22) → U10_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T18, T20, T19, X26))
shanoi11_in_gggga(0, T57, T58, T59, .(mv(T57, T59), [])) → shanoi11_out_gggga(0, T57, T58, T59, .(mv(T57, T59), []))
shanoi11_in_gggga(s(T88), T69, T70, T71, X101) → U1_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, X98))
shanoi11_in_gggga(s(T88), T69, T70, T71, X101) → U2_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, T95))
U2_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U3_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T70, T69, T71, X99))
U3_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T70, T69, T71, X99)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U2_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_in_gggga(T88, T70, T69, T71, T108))
U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U5_gggga(T88, T69, T70, T71, X101, append28_in_aga(T95, .(mv(T69, T71), []), X100))
append28_in_aga([], T130, T130) → append28_out_aga([], T130, T130)
append28_in_aga(.(T137, T138), T139, .(T137, X178)) → U8_aga(T137, T138, T139, X178, append28_in_aga(T138, T139, X178))
U8_aga(T137, T138, T139, X178, append28_out_aga(T138, T139, X178)) → append28_out_aga(.(T137, T138), T139, .(T137, X178))
U5_gggga(T88, T69, T70, T71, X101, append28_out_aga(T95, .(mv(T69, T71), []), X100)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U6_gggga(T88, T69, T70, T71, X101, T108, append28_in_aga(T95, .(mv(T69, T71), []), T119))
U6_gggga(T88, T69, T70, T71, X101, T108, append28_out_aga(T95, .(mv(T69, T71), []), T119)) → U7_gggga(T88, T69, T70, T71, X101, append28_in_gaa(T119, T108, X101))
append28_in_gaa([], T130, T130) → append28_out_gaa([], T130, T130)
append28_in_gaa(.(T137, T138), T139, .(T137, X178)) → U8_gaa(T137, T138, T139, X178, append28_in_gaa(T138, T139, X178))
U8_gaa(T137, T138, T139, X178, append28_out_gaa(T138, T139, X178)) → append28_out_gaa(.(T137, T138), T139, .(T137, X178))
U7_gggga(T88, T69, T70, T71, X101, append28_out_gaa(T119, T108, X101)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U1_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, X98)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U10_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, X26)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
shanoi1_in_gggga(s(s(T31)), T18, T19, T20, T22) → U11_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T18, T20, T19, T38))
U11_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → U12_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T20, T18, T20, X27))
U12_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T20, T18, T20, X27)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
U11_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_in_gggga(T31, T20, T18, T20, T148))
U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → U14_gggga(T31, T18, T19, T20, T22, append40_in_aga(T38, .(mv(T18, T20), []), X28))
append40_in_aga([], T170, T170) → append40_out_aga([], T170, T170)
append40_in_aga(.(T179, T180), T181, .(T179, T183)) → U9_aga(T179, T180, T181, T183, append40_in_aga(T180, T181, T183))
U9_aga(T179, T180, T181, T183, append40_out_aga(T180, T181, T183)) → append40_out_aga(.(T179, T180), T181, .(T179, T183))
U14_gggga(T31, T18, T19, T20, T22, append40_out_aga(T38, .(mv(T18, T20), []), X28)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → U15_gggga(T31, T18, T19, T20, T22, T148, append40_in_aga(T38, .(mv(T18, T20), []), T159))
U15_gggga(T31, T18, T19, T20, T22, T148, append40_out_aga(T38, .(mv(T18, T20), []), T159)) → U16_gggga(T31, T18, T19, T20, T22, append40_in_gaa(T159, T148, T22))
append40_in_gaa([], T170, T170) → append40_out_gaa([], T170, T170)
append40_in_gaa(.(T179, T180), T181, .(T179, T183)) → U9_gaa(T179, T180, T181, T183, append40_in_gaa(T180, T181, T183))
U9_gaa(T179, T180, T181, T183, append40_out_gaa(T180, T181, T183)) → append40_out_gaa(.(T179, T180), T181, .(T179, T183))
U16_gggga(T31, T18, T19, T20, T22, append40_out_gaa(T159, T148, T22)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
APPEND28_IN_AGA(.(T137, T138), T139, .(T137, X178)) → APPEND28_IN_AGA(T138, T139, X178)
APPEND28_IN_AGA(T139) → APPEND28_IN_AGA(T139)
SHANOI11_IN_GGGGA(s(T88), T69, T70, T71, X101) → U2_GGGGA(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, T95))
U2_GGGGA(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → SHANOI11_IN_GGGGA(T88, T70, T69, T71, X99)
SHANOI11_IN_GGGGA(s(T88), T69, T70, T71, X101) → SHANOI11_IN_GGGGA(T88, T69, T71, T70, X98)
shanoi1_in_gggga(s(0), T9, T10, T11, .(mv(T9, T11), [])) → shanoi1_out_gggga(s(0), T9, T10, T11, .(mv(T9, T11), []))
shanoi1_in_gggga(s(s(T31)), T18, T19, T20, T22) → U10_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T18, T20, T19, X26))
shanoi11_in_gggga(0, T57, T58, T59, .(mv(T57, T59), [])) → shanoi11_out_gggga(0, T57, T58, T59, .(mv(T57, T59), []))
shanoi11_in_gggga(s(T88), T69, T70, T71, X101) → U1_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, X98))
shanoi11_in_gggga(s(T88), T69, T70, T71, X101) → U2_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, T95))
U2_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U3_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T70, T69, T71, X99))
U3_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T70, T69, T71, X99)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U2_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_in_gggga(T88, T70, T69, T71, T108))
U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U5_gggga(T88, T69, T70, T71, X101, append28_in_aga(T95, .(mv(T69, T71), []), X100))
append28_in_aga([], T130, T130) → append28_out_aga([], T130, T130)
append28_in_aga(.(T137, T138), T139, .(T137, X178)) → U8_aga(T137, T138, T139, X178, append28_in_aga(T138, T139, X178))
U8_aga(T137, T138, T139, X178, append28_out_aga(T138, T139, X178)) → append28_out_aga(.(T137, T138), T139, .(T137, X178))
U5_gggga(T88, T69, T70, T71, X101, append28_out_aga(T95, .(mv(T69, T71), []), X100)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U6_gggga(T88, T69, T70, T71, X101, T108, append28_in_aga(T95, .(mv(T69, T71), []), T119))
U6_gggga(T88, T69, T70, T71, X101, T108, append28_out_aga(T95, .(mv(T69, T71), []), T119)) → U7_gggga(T88, T69, T70, T71, X101, append28_in_gaa(T119, T108, X101))
append28_in_gaa([], T130, T130) → append28_out_gaa([], T130, T130)
append28_in_gaa(.(T137, T138), T139, .(T137, X178)) → U8_gaa(T137, T138, T139, X178, append28_in_gaa(T138, T139, X178))
U8_gaa(T137, T138, T139, X178, append28_out_gaa(T138, T139, X178)) → append28_out_gaa(.(T137, T138), T139, .(T137, X178))
U7_gggga(T88, T69, T70, T71, X101, append28_out_gaa(T119, T108, X101)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U1_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, X98)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U10_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, X26)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
shanoi1_in_gggga(s(s(T31)), T18, T19, T20, T22) → U11_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T18, T20, T19, T38))
U11_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → U12_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T20, T18, T20, X27))
U12_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T20, T18, T20, X27)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
U11_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_in_gggga(T31, T20, T18, T20, T148))
U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → U14_gggga(T31, T18, T19, T20, T22, append40_in_aga(T38, .(mv(T18, T20), []), X28))
append40_in_aga([], T170, T170) → append40_out_aga([], T170, T170)
append40_in_aga(.(T179, T180), T181, .(T179, T183)) → U9_aga(T179, T180, T181, T183, append40_in_aga(T180, T181, T183))
U9_aga(T179, T180, T181, T183, append40_out_aga(T180, T181, T183)) → append40_out_aga(.(T179, T180), T181, .(T179, T183))
U14_gggga(T31, T18, T19, T20, T22, append40_out_aga(T38, .(mv(T18, T20), []), X28)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → U15_gggga(T31, T18, T19, T20, T22, T148, append40_in_aga(T38, .(mv(T18, T20), []), T159))
U15_gggga(T31, T18, T19, T20, T22, T148, append40_out_aga(T38, .(mv(T18, T20), []), T159)) → U16_gggga(T31, T18, T19, T20, T22, append40_in_gaa(T159, T148, T22))
append40_in_gaa([], T170, T170) → append40_out_gaa([], T170, T170)
append40_in_gaa(.(T179, T180), T181, .(T179, T183)) → U9_gaa(T179, T180, T181, T183, append40_in_gaa(T180, T181, T183))
U9_gaa(T179, T180, T181, T183, append40_out_gaa(T180, T181, T183)) → append40_out_gaa(.(T179, T180), T181, .(T179, T183))
U16_gggga(T31, T18, T19, T20, T22, append40_out_gaa(T159, T148, T22)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
SHANOI11_IN_GGGGA(s(T88), T69, T70, T71, X101) → U2_GGGGA(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, T95))
U2_GGGGA(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → SHANOI11_IN_GGGGA(T88, T70, T69, T71, X99)
SHANOI11_IN_GGGGA(s(T88), T69, T70, T71, X101) → SHANOI11_IN_GGGGA(T88, T69, T71, T70, X98)
shanoi11_in_gggga(0, T57, T58, T59, .(mv(T57, T59), [])) → shanoi11_out_gggga(0, T57, T58, T59, .(mv(T57, T59), []))
shanoi11_in_gggga(s(T88), T69, T70, T71, X101) → U1_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, X98))
shanoi11_in_gggga(s(T88), T69, T70, T71, X101) → U2_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, T95))
U1_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, X98)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U2_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U3_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T70, T69, T71, X99))
U2_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_in_gggga(T88, T70, T69, T71, T108))
U3_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T70, T69, T71, X99)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U5_gggga(T88, T69, T70, T71, X101, append28_in_aga(T95, .(mv(T69, T71), []), X100))
U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U6_gggga(T88, T69, T70, T71, X101, T108, append28_in_aga(T95, .(mv(T69, T71), []), T119))
U5_gggga(T88, T69, T70, T71, X101, append28_out_aga(T95, .(mv(T69, T71), []), X100)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U6_gggga(T88, T69, T70, T71, X101, T108, append28_out_aga(T95, .(mv(T69, T71), []), T119)) → U7_gggga(T88, T69, T70, T71, X101, append28_in_gaa(T119, T108, X101))
append28_in_aga([], T130, T130) → append28_out_aga([], T130, T130)
append28_in_aga(.(T137, T138), T139, .(T137, X178)) → U8_aga(T137, T138, T139, X178, append28_in_aga(T138, T139, X178))
U7_gggga(T88, T69, T70, T71, X101, append28_out_gaa(T119, T108, X101)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U8_aga(T137, T138, T139, X178, append28_out_aga(T138, T139, X178)) → append28_out_aga(.(T137, T138), T139, .(T137, X178))
append28_in_gaa([], T130, T130) → append28_out_gaa([], T130, T130)
append28_in_gaa(.(T137, T138), T139, .(T137, X178)) → U8_gaa(T137, T138, T139, X178, append28_in_gaa(T138, T139, X178))
U8_gaa(T137, T138, T139, X178, append28_out_gaa(T138, T139, X178)) → append28_out_gaa(.(T137, T138), T139, .(T137, X178))
SHANOI11_IN_GGGGA(s(T88), T69, T70, T71) → U2_GGGGA(T88, T69, T70, T71, shanoi11_in_gggga(T88, T69, T71, T70))
U2_GGGGA(T88, T69, T70, T71, shanoi11_out_gggga) → SHANOI11_IN_GGGGA(T88, T70, T69, T71)
SHANOI11_IN_GGGGA(s(T88), T69, T70, T71) → SHANOI11_IN_GGGGA(T88, T69, T71, T70)
shanoi11_in_gggga(0, T57, T58, T59) → shanoi11_out_gggga
shanoi11_in_gggga(s(T88), T69, T70, T71) → U1_gggga(shanoi11_in_gggga(T88, T69, T71, T70))
shanoi11_in_gggga(s(T88), T69, T70, T71) → U2_gggga(T88, T69, T70, T71, shanoi11_in_gggga(T88, T69, T71, T70))
U1_gggga(shanoi11_out_gggga) → shanoi11_out_gggga
U2_gggga(T88, T69, T70, T71, shanoi11_out_gggga) → U3_gggga(shanoi11_in_gggga(T88, T70, T69, T71))
U2_gggga(T88, T69, T70, T71, shanoi11_out_gggga) → U4_gggga(shanoi11_in_gggga(T88, T70, T69, T71))
U3_gggga(shanoi11_out_gggga) → shanoi11_out_gggga
U4_gggga(shanoi11_out_gggga) → U5_gggga(append28_in_aga(.([])))
U4_gggga(shanoi11_out_gggga) → U6_gggga(append28_in_aga(.([])))
U5_gggga(append28_out_aga(T95, X100)) → shanoi11_out_gggga
U6_gggga(append28_out_aga(T95, T119)) → U7_gggga(append28_in_gaa(T119))
append28_in_aga(T130) → append28_out_aga([], T130)
append28_in_aga(T139) → U8_aga(append28_in_aga(T139))
U7_gggga(append28_out_gaa) → shanoi11_out_gggga
U8_aga(append28_out_aga(T138, X178)) → append28_out_aga(.(T138), .(X178))
append28_in_gaa([]) → append28_out_gaa
append28_in_gaa(.(T138)) → U8_gaa(append28_in_gaa(T138))
U8_gaa(append28_out_gaa) → append28_out_gaa
shanoi11_in_gggga(x0, x1, x2, x3)
U1_gggga(x0)
U2_gggga(x0, x1, x2, x3, x4)
U3_gggga(x0)
U4_gggga(x0)
U5_gggga(x0)
U6_gggga(x0)
append28_in_aga(x0)
U7_gggga(x0)
U8_aga(x0)
append28_in_gaa(x0)
U8_gaa(x0)
From the DPs we obtained the following set of size-change graphs:
shanoi1_in_gggga(s(0), T9, T10, T11, .(mv(T9, T11), [])) → shanoi1_out_gggga(s(0), T9, T10, T11, .(mv(T9, T11), []))
shanoi1_in_gggga(s(s(T31)), T18, T19, T20, T22) → U10_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T18, T20, T19, X26))
shanoi11_in_gggga(0, T57, T58, T59, .(mv(T57, T59), [])) → shanoi11_out_gggga(0, T57, T58, T59, .(mv(T57, T59), []))
shanoi11_in_gggga(s(T88), T69, T70, T71, X101) → U1_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, X98))
shanoi11_in_gggga(s(T88), T69, T70, T71, X101) → U2_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, T95))
U2_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U3_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T70, T69, T71, X99))
U3_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T70, T69, T71, X99)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U2_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_in_gggga(T88, T70, T69, T71, T108))
U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U5_gggga(T88, T69, T70, T71, X101, append28_in_aga(T95, .(mv(T69, T71), []), X100))
append28_in_aga([], T130, T130) → append28_out_aga([], T130, T130)
append28_in_aga(.(T137, T138), T139, .(T137, X178)) → U8_aga(T137, T138, T139, X178, append28_in_aga(T138, T139, X178))
U8_aga(T137, T138, T139, X178, append28_out_aga(T138, T139, X178)) → append28_out_aga(.(T137, T138), T139, .(T137, X178))
U5_gggga(T88, T69, T70, T71, X101, append28_out_aga(T95, .(mv(T69, T71), []), X100)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U6_gggga(T88, T69, T70, T71, X101, T108, append28_in_aga(T95, .(mv(T69, T71), []), T119))
U6_gggga(T88, T69, T70, T71, X101, T108, append28_out_aga(T95, .(mv(T69, T71), []), T119)) → U7_gggga(T88, T69, T70, T71, X101, append28_in_gaa(T119, T108, X101))
append28_in_gaa([], T130, T130) → append28_out_gaa([], T130, T130)
append28_in_gaa(.(T137, T138), T139, .(T137, X178)) → U8_gaa(T137, T138, T139, X178, append28_in_gaa(T138, T139, X178))
U8_gaa(T137, T138, T139, X178, append28_out_gaa(T138, T139, X178)) → append28_out_gaa(.(T137, T138), T139, .(T137, X178))
U7_gggga(T88, T69, T70, T71, X101, append28_out_gaa(T119, T108, X101)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U1_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, X98)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U10_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, X26)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
shanoi1_in_gggga(s(s(T31)), T18, T19, T20, T22) → U11_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T18, T20, T19, T38))
U11_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → U12_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T20, T18, T20, X27))
U12_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T20, T18, T20, X27)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
U11_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_in_gggga(T31, T20, T18, T20, T148))
U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → U14_gggga(T31, T18, T19, T20, T22, append40_in_aga(T38, .(mv(T18, T20), []), X28))
append40_in_aga([], T170, T170) → append40_out_aga([], T170, T170)
append40_in_aga(.(T179, T180), T181, .(T179, T183)) → U9_aga(T179, T180, T181, T183, append40_in_aga(T180, T181, T183))
U9_aga(T179, T180, T181, T183, append40_out_aga(T180, T181, T183)) → append40_out_aga(.(T179, T180), T181, .(T179, T183))
U14_gggga(T31, T18, T19, T20, T22, append40_out_aga(T38, .(mv(T18, T20), []), X28)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → U15_gggga(T31, T18, T19, T20, T22, T148, append40_in_aga(T38, .(mv(T18, T20), []), T159))
U15_gggga(T31, T18, T19, T20, T22, T148, append40_out_aga(T38, .(mv(T18, T20), []), T159)) → U16_gggga(T31, T18, T19, T20, T22, append40_in_gaa(T159, T148, T22))
append40_in_gaa([], T170, T170) → append40_out_gaa([], T170, T170)
append40_in_gaa(.(T179, T180), T181, .(T179, T183)) → U9_gaa(T179, T180, T181, T183, append40_in_gaa(T180, T181, T183))
U9_gaa(T179, T180, T181, T183, append40_out_gaa(T180, T181, T183)) → append40_out_gaa(.(T179, T180), T181, .(T179, T183))
U16_gggga(T31, T18, T19, T20, T22, append40_out_gaa(T159, T148, T22)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
shanoi1_in_gggga(s(0), T9, T10, T11, .(mv(T9, T11), [])) → shanoi1_out_gggga(s(0), T9, T10, T11, .(mv(T9, T11), []))
shanoi1_in_gggga(s(s(T31)), T18, T19, T20, T22) → U10_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T18, T20, T19, X26))
shanoi11_in_gggga(0, T57, T58, T59, .(mv(T57, T59), [])) → shanoi11_out_gggga(0, T57, T58, T59, .(mv(T57, T59), []))
shanoi11_in_gggga(s(T88), T69, T70, T71, X101) → U1_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, X98))
shanoi11_in_gggga(s(T88), T69, T70, T71, X101) → U2_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, T95))
U2_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U3_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T70, T69, T71, X99))
U3_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T70, T69, T71, X99)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U2_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_in_gggga(T88, T70, T69, T71, T108))
U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U5_gggga(T88, T69, T70, T71, X101, append28_in_aga(T95, .(mv(T69, T71), []), X100))
append28_in_aga([], T130, T130) → append28_out_aga([], T130, T130)
append28_in_aga(.(T137, T138), T139, .(T137, X178)) → U8_aga(T137, T138, T139, X178, append28_in_aga(T138, T139, X178))
U8_aga(T137, T138, T139, X178, append28_out_aga(T138, T139, X178)) → append28_out_aga(.(T137, T138), T139, .(T137, X178))
U5_gggga(T88, T69, T70, T71, X101, append28_out_aga(T95, .(mv(T69, T71), []), X100)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U6_gggga(T88, T69, T70, T71, X101, T108, append28_in_aga(T95, .(mv(T69, T71), []), T119))
U6_gggga(T88, T69, T70, T71, X101, T108, append28_out_aga(T95, .(mv(T69, T71), []), T119)) → U7_gggga(T88, T69, T70, T71, X101, append28_in_gaa(T119, T108, X101))
append28_in_gaa([], T130, T130) → append28_out_gaa([], T130, T130)
append28_in_gaa(.(T137, T138), T139, .(T137, X178)) → U8_gaa(T137, T138, T139, X178, append28_in_gaa(T138, T139, X178))
U8_gaa(T137, T138, T139, X178, append28_out_gaa(T138, T139, X178)) → append28_out_gaa(.(T137, T138), T139, .(T137, X178))
U7_gggga(T88, T69, T70, T71, X101, append28_out_gaa(T119, T108, X101)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U1_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, X98)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U10_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, X26)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
shanoi1_in_gggga(s(s(T31)), T18, T19, T20, T22) → U11_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T18, T20, T19, T38))
U11_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → U12_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T20, T18, T20, X27))
U12_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T20, T18, T20, X27)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
U11_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_in_gggga(T31, T20, T18, T20, T148))
U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → U14_gggga(T31, T18, T19, T20, T22, append40_in_aga(T38, .(mv(T18, T20), []), X28))
append40_in_aga([], T170, T170) → append40_out_aga([], T170, T170)
append40_in_aga(.(T179, T180), T181, .(T179, T183)) → U9_aga(T179, T180, T181, T183, append40_in_aga(T180, T181, T183))
U9_aga(T179, T180, T181, T183, append40_out_aga(T180, T181, T183)) → append40_out_aga(.(T179, T180), T181, .(T179, T183))
U14_gggga(T31, T18, T19, T20, T22, append40_out_aga(T38, .(mv(T18, T20), []), X28)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → U15_gggga(T31, T18, T19, T20, T22, T148, append40_in_aga(T38, .(mv(T18, T20), []), T159))
U15_gggga(T31, T18, T19, T20, T22, T148, append40_out_aga(T38, .(mv(T18, T20), []), T159)) → U16_gggga(T31, T18, T19, T20, T22, append40_in_gaa(T159, T148, T22))
append40_in_gaa([], T170, T170) → append40_out_gaa([], T170, T170)
append40_in_gaa(.(T179, T180), T181, .(T179, T183)) → U9_gaa(T179, T180, T181, T183, append40_in_gaa(T180, T181, T183))
U9_gaa(T179, T180, T181, T183, append40_out_gaa(T180, T181, T183)) → append40_out_gaa(.(T179, T180), T181, .(T179, T183))
U16_gggga(T31, T18, T19, T20, T22, append40_out_gaa(T159, T148, T22)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
SHANOI1_IN_GGGGA(s(s(T31)), T18, T19, T20, T22) → U10_GGGGA(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T18, T20, T19, X26))
SHANOI1_IN_GGGGA(s(s(T31)), T18, T19, T20, T22) → SHANOI11_IN_GGGGA(T31, T18, T20, T19, X26)
SHANOI11_IN_GGGGA(s(T88), T69, T70, T71, X101) → U1_GGGGA(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, X98))
SHANOI11_IN_GGGGA(s(T88), T69, T70, T71, X101) → SHANOI11_IN_GGGGA(T88, T69, T71, T70, X98)
SHANOI11_IN_GGGGA(s(T88), T69, T70, T71, X101) → U2_GGGGA(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, T95))
U2_GGGGA(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U3_GGGGA(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T70, T69, T71, X99))
U2_GGGGA(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → SHANOI11_IN_GGGGA(T88, T70, T69, T71, X99)
U2_GGGGA(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U4_GGGGA(T88, T69, T70, T71, X101, T95, shanoi11_in_gggga(T88, T70, T69, T71, T108))
U4_GGGGA(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U5_GGGGA(T88, T69, T70, T71, X101, append28_in_aga(T95, .(mv(T69, T71), []), X100))
U4_GGGGA(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → APPEND28_IN_AGA(T95, .(mv(T69, T71), []), X100)
APPEND28_IN_AGA(.(T137, T138), T139, .(T137, X178)) → U8_AGA(T137, T138, T139, X178, append28_in_aga(T138, T139, X178))
APPEND28_IN_AGA(.(T137, T138), T139, .(T137, X178)) → APPEND28_IN_AGA(T138, T139, X178)
U4_GGGGA(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U6_GGGGA(T88, T69, T70, T71, X101, T108, append28_in_aga(T95, .(mv(T69, T71), []), T119))
U6_GGGGA(T88, T69, T70, T71, X101, T108, append28_out_aga(T95, .(mv(T69, T71), []), T119)) → U7_GGGGA(T88, T69, T70, T71, X101, append28_in_gaa(T119, T108, X101))
U6_GGGGA(T88, T69, T70, T71, X101, T108, append28_out_aga(T95, .(mv(T69, T71), []), T119)) → APPEND28_IN_GAA(T119, T108, X101)
APPEND28_IN_GAA(.(T137, T138), T139, .(T137, X178)) → U8_GAA(T137, T138, T139, X178, append28_in_gaa(T138, T139, X178))
APPEND28_IN_GAA(.(T137, T138), T139, .(T137, X178)) → APPEND28_IN_GAA(T138, T139, X178)
SHANOI1_IN_GGGGA(s(s(T31)), T18, T19, T20, T22) → U11_GGGGA(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T18, T20, T19, T38))
U11_GGGGA(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → U12_GGGGA(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T20, T18, T20, X27))
U11_GGGGA(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → SHANOI11_IN_GGGGA(T31, T20, T18, T20, X27)
U11_GGGGA(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → U13_GGGGA(T31, T18, T19, T20, T22, T38, shanoi11_in_gggga(T31, T20, T18, T20, T148))
U13_GGGGA(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → U14_GGGGA(T31, T18, T19, T20, T22, append40_in_aga(T38, .(mv(T18, T20), []), X28))
U13_GGGGA(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → APPEND40_IN_AGA(T38, .(mv(T18, T20), []), X28)
APPEND40_IN_AGA(.(T179, T180), T181, .(T179, T183)) → U9_AGA(T179, T180, T181, T183, append40_in_aga(T180, T181, T183))
APPEND40_IN_AGA(.(T179, T180), T181, .(T179, T183)) → APPEND40_IN_AGA(T180, T181, T183)
U13_GGGGA(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → U15_GGGGA(T31, T18, T19, T20, T22, T148, append40_in_aga(T38, .(mv(T18, T20), []), T159))
U15_GGGGA(T31, T18, T19, T20, T22, T148, append40_out_aga(T38, .(mv(T18, T20), []), T159)) → U16_GGGGA(T31, T18, T19, T20, T22, append40_in_gaa(T159, T148, T22))
U15_GGGGA(T31, T18, T19, T20, T22, T148, append40_out_aga(T38, .(mv(T18, T20), []), T159)) → APPEND40_IN_GAA(T159, T148, T22)
APPEND40_IN_GAA(.(T179, T180), T181, .(T179, T183)) → U9_GAA(T179, T180, T181, T183, append40_in_gaa(T180, T181, T183))
APPEND40_IN_GAA(.(T179, T180), T181, .(T179, T183)) → APPEND40_IN_GAA(T180, T181, T183)
shanoi1_in_gggga(s(0), T9, T10, T11, .(mv(T9, T11), [])) → shanoi1_out_gggga(s(0), T9, T10, T11, .(mv(T9, T11), []))
shanoi1_in_gggga(s(s(T31)), T18, T19, T20, T22) → U10_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T18, T20, T19, X26))
shanoi11_in_gggga(0, T57, T58, T59, .(mv(T57, T59), [])) → shanoi11_out_gggga(0, T57, T58, T59, .(mv(T57, T59), []))
shanoi11_in_gggga(s(T88), T69, T70, T71, X101) → U1_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, X98))
shanoi11_in_gggga(s(T88), T69, T70, T71, X101) → U2_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, T95))
U2_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U3_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T70, T69, T71, X99))
U3_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T70, T69, T71, X99)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U2_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_in_gggga(T88, T70, T69, T71, T108))
U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U5_gggga(T88, T69, T70, T71, X101, append28_in_aga(T95, .(mv(T69, T71), []), X100))
append28_in_aga([], T130, T130) → append28_out_aga([], T130, T130)
append28_in_aga(.(T137, T138), T139, .(T137, X178)) → U8_aga(T137, T138, T139, X178, append28_in_aga(T138, T139, X178))
U8_aga(T137, T138, T139, X178, append28_out_aga(T138, T139, X178)) → append28_out_aga(.(T137, T138), T139, .(T137, X178))
U5_gggga(T88, T69, T70, T71, X101, append28_out_aga(T95, .(mv(T69, T71), []), X100)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U6_gggga(T88, T69, T70, T71, X101, T108, append28_in_aga(T95, .(mv(T69, T71), []), T119))
U6_gggga(T88, T69, T70, T71, X101, T108, append28_out_aga(T95, .(mv(T69, T71), []), T119)) → U7_gggga(T88, T69, T70, T71, X101, append28_in_gaa(T119, T108, X101))
append28_in_gaa([], T130, T130) → append28_out_gaa([], T130, T130)
append28_in_gaa(.(T137, T138), T139, .(T137, X178)) → U8_gaa(T137, T138, T139, X178, append28_in_gaa(T138, T139, X178))
U8_gaa(T137, T138, T139, X178, append28_out_gaa(T138, T139, X178)) → append28_out_gaa(.(T137, T138), T139, .(T137, X178))
U7_gggga(T88, T69, T70, T71, X101, append28_out_gaa(T119, T108, X101)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U1_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, X98)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U10_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, X26)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
shanoi1_in_gggga(s(s(T31)), T18, T19, T20, T22) → U11_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T18, T20, T19, T38))
U11_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → U12_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T20, T18, T20, X27))
U12_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T20, T18, T20, X27)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
U11_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_in_gggga(T31, T20, T18, T20, T148))
U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → U14_gggga(T31, T18, T19, T20, T22, append40_in_aga(T38, .(mv(T18, T20), []), X28))
append40_in_aga([], T170, T170) → append40_out_aga([], T170, T170)
append40_in_aga(.(T179, T180), T181, .(T179, T183)) → U9_aga(T179, T180, T181, T183, append40_in_aga(T180, T181, T183))
U9_aga(T179, T180, T181, T183, append40_out_aga(T180, T181, T183)) → append40_out_aga(.(T179, T180), T181, .(T179, T183))
U14_gggga(T31, T18, T19, T20, T22, append40_out_aga(T38, .(mv(T18, T20), []), X28)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → U15_gggga(T31, T18, T19, T20, T22, T148, append40_in_aga(T38, .(mv(T18, T20), []), T159))
U15_gggga(T31, T18, T19, T20, T22, T148, append40_out_aga(T38, .(mv(T18, T20), []), T159)) → U16_gggga(T31, T18, T19, T20, T22, append40_in_gaa(T159, T148, T22))
append40_in_gaa([], T170, T170) → append40_out_gaa([], T170, T170)
append40_in_gaa(.(T179, T180), T181, .(T179, T183)) → U9_gaa(T179, T180, T181, T183, append40_in_gaa(T180, T181, T183))
U9_gaa(T179, T180, T181, T183, append40_out_gaa(T180, T181, T183)) → append40_out_gaa(.(T179, T180), T181, .(T179, T183))
U16_gggga(T31, T18, T19, T20, T22, append40_out_gaa(T159, T148, T22)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
SHANOI1_IN_GGGGA(s(s(T31)), T18, T19, T20, T22) → U10_GGGGA(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T18, T20, T19, X26))
SHANOI1_IN_GGGGA(s(s(T31)), T18, T19, T20, T22) → SHANOI11_IN_GGGGA(T31, T18, T20, T19, X26)
SHANOI11_IN_GGGGA(s(T88), T69, T70, T71, X101) → U1_GGGGA(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, X98))
SHANOI11_IN_GGGGA(s(T88), T69, T70, T71, X101) → SHANOI11_IN_GGGGA(T88, T69, T71, T70, X98)
SHANOI11_IN_GGGGA(s(T88), T69, T70, T71, X101) → U2_GGGGA(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, T95))
U2_GGGGA(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U3_GGGGA(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T70, T69, T71, X99))
U2_GGGGA(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → SHANOI11_IN_GGGGA(T88, T70, T69, T71, X99)
U2_GGGGA(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U4_GGGGA(T88, T69, T70, T71, X101, T95, shanoi11_in_gggga(T88, T70, T69, T71, T108))
U4_GGGGA(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U5_GGGGA(T88, T69, T70, T71, X101, append28_in_aga(T95, .(mv(T69, T71), []), X100))
U4_GGGGA(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → APPEND28_IN_AGA(T95, .(mv(T69, T71), []), X100)
APPEND28_IN_AGA(.(T137, T138), T139, .(T137, X178)) → U8_AGA(T137, T138, T139, X178, append28_in_aga(T138, T139, X178))
APPEND28_IN_AGA(.(T137, T138), T139, .(T137, X178)) → APPEND28_IN_AGA(T138, T139, X178)
U4_GGGGA(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U6_GGGGA(T88, T69, T70, T71, X101, T108, append28_in_aga(T95, .(mv(T69, T71), []), T119))
U6_GGGGA(T88, T69, T70, T71, X101, T108, append28_out_aga(T95, .(mv(T69, T71), []), T119)) → U7_GGGGA(T88, T69, T70, T71, X101, append28_in_gaa(T119, T108, X101))
U6_GGGGA(T88, T69, T70, T71, X101, T108, append28_out_aga(T95, .(mv(T69, T71), []), T119)) → APPEND28_IN_GAA(T119, T108, X101)
APPEND28_IN_GAA(.(T137, T138), T139, .(T137, X178)) → U8_GAA(T137, T138, T139, X178, append28_in_gaa(T138, T139, X178))
APPEND28_IN_GAA(.(T137, T138), T139, .(T137, X178)) → APPEND28_IN_GAA(T138, T139, X178)
SHANOI1_IN_GGGGA(s(s(T31)), T18, T19, T20, T22) → U11_GGGGA(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T18, T20, T19, T38))
U11_GGGGA(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → U12_GGGGA(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T20, T18, T20, X27))
U11_GGGGA(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → SHANOI11_IN_GGGGA(T31, T20, T18, T20, X27)
U11_GGGGA(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → U13_GGGGA(T31, T18, T19, T20, T22, T38, shanoi11_in_gggga(T31, T20, T18, T20, T148))
U13_GGGGA(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → U14_GGGGA(T31, T18, T19, T20, T22, append40_in_aga(T38, .(mv(T18, T20), []), X28))
U13_GGGGA(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → APPEND40_IN_AGA(T38, .(mv(T18, T20), []), X28)
APPEND40_IN_AGA(.(T179, T180), T181, .(T179, T183)) → U9_AGA(T179, T180, T181, T183, append40_in_aga(T180, T181, T183))
APPEND40_IN_AGA(.(T179, T180), T181, .(T179, T183)) → APPEND40_IN_AGA(T180, T181, T183)
U13_GGGGA(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → U15_GGGGA(T31, T18, T19, T20, T22, T148, append40_in_aga(T38, .(mv(T18, T20), []), T159))
U15_GGGGA(T31, T18, T19, T20, T22, T148, append40_out_aga(T38, .(mv(T18, T20), []), T159)) → U16_GGGGA(T31, T18, T19, T20, T22, append40_in_gaa(T159, T148, T22))
U15_GGGGA(T31, T18, T19, T20, T22, T148, append40_out_aga(T38, .(mv(T18, T20), []), T159)) → APPEND40_IN_GAA(T159, T148, T22)
APPEND40_IN_GAA(.(T179, T180), T181, .(T179, T183)) → U9_GAA(T179, T180, T181, T183, append40_in_gaa(T180, T181, T183))
APPEND40_IN_GAA(.(T179, T180), T181, .(T179, T183)) → APPEND40_IN_GAA(T180, T181, T183)
shanoi1_in_gggga(s(0), T9, T10, T11, .(mv(T9, T11), [])) → shanoi1_out_gggga(s(0), T9, T10, T11, .(mv(T9, T11), []))
shanoi1_in_gggga(s(s(T31)), T18, T19, T20, T22) → U10_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T18, T20, T19, X26))
shanoi11_in_gggga(0, T57, T58, T59, .(mv(T57, T59), [])) → shanoi11_out_gggga(0, T57, T58, T59, .(mv(T57, T59), []))
shanoi11_in_gggga(s(T88), T69, T70, T71, X101) → U1_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, X98))
shanoi11_in_gggga(s(T88), T69, T70, T71, X101) → U2_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, T95))
U2_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U3_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T70, T69, T71, X99))
U3_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T70, T69, T71, X99)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U2_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_in_gggga(T88, T70, T69, T71, T108))
U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U5_gggga(T88, T69, T70, T71, X101, append28_in_aga(T95, .(mv(T69, T71), []), X100))
append28_in_aga([], T130, T130) → append28_out_aga([], T130, T130)
append28_in_aga(.(T137, T138), T139, .(T137, X178)) → U8_aga(T137, T138, T139, X178, append28_in_aga(T138, T139, X178))
U8_aga(T137, T138, T139, X178, append28_out_aga(T138, T139, X178)) → append28_out_aga(.(T137, T138), T139, .(T137, X178))
U5_gggga(T88, T69, T70, T71, X101, append28_out_aga(T95, .(mv(T69, T71), []), X100)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U6_gggga(T88, T69, T70, T71, X101, T108, append28_in_aga(T95, .(mv(T69, T71), []), T119))
U6_gggga(T88, T69, T70, T71, X101, T108, append28_out_aga(T95, .(mv(T69, T71), []), T119)) → U7_gggga(T88, T69, T70, T71, X101, append28_in_gaa(T119, T108, X101))
append28_in_gaa([], T130, T130) → append28_out_gaa([], T130, T130)
append28_in_gaa(.(T137, T138), T139, .(T137, X178)) → U8_gaa(T137, T138, T139, X178, append28_in_gaa(T138, T139, X178))
U8_gaa(T137, T138, T139, X178, append28_out_gaa(T138, T139, X178)) → append28_out_gaa(.(T137, T138), T139, .(T137, X178))
U7_gggga(T88, T69, T70, T71, X101, append28_out_gaa(T119, T108, X101)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U1_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, X98)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U10_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, X26)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
shanoi1_in_gggga(s(s(T31)), T18, T19, T20, T22) → U11_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T18, T20, T19, T38))
U11_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → U12_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T20, T18, T20, X27))
U12_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T20, T18, T20, X27)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
U11_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_in_gggga(T31, T20, T18, T20, T148))
U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → U14_gggga(T31, T18, T19, T20, T22, append40_in_aga(T38, .(mv(T18, T20), []), X28))
append40_in_aga([], T170, T170) → append40_out_aga([], T170, T170)
append40_in_aga(.(T179, T180), T181, .(T179, T183)) → U9_aga(T179, T180, T181, T183, append40_in_aga(T180, T181, T183))
U9_aga(T179, T180, T181, T183, append40_out_aga(T180, T181, T183)) → append40_out_aga(.(T179, T180), T181, .(T179, T183))
U14_gggga(T31, T18, T19, T20, T22, append40_out_aga(T38, .(mv(T18, T20), []), X28)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → U15_gggga(T31, T18, T19, T20, T22, T148, append40_in_aga(T38, .(mv(T18, T20), []), T159))
U15_gggga(T31, T18, T19, T20, T22, T148, append40_out_aga(T38, .(mv(T18, T20), []), T159)) → U16_gggga(T31, T18, T19, T20, T22, append40_in_gaa(T159, T148, T22))
append40_in_gaa([], T170, T170) → append40_out_gaa([], T170, T170)
append40_in_gaa(.(T179, T180), T181, .(T179, T183)) → U9_gaa(T179, T180, T181, T183, append40_in_gaa(T180, T181, T183))
U9_gaa(T179, T180, T181, T183, append40_out_gaa(T180, T181, T183)) → append40_out_gaa(.(T179, T180), T181, .(T179, T183))
U16_gggga(T31, T18, T19, T20, T22, append40_out_gaa(T159, T148, T22)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
APPEND40_IN_GAA(.(T179, T180), T181, .(T179, T183)) → APPEND40_IN_GAA(T180, T181, T183)
shanoi1_in_gggga(s(0), T9, T10, T11, .(mv(T9, T11), [])) → shanoi1_out_gggga(s(0), T9, T10, T11, .(mv(T9, T11), []))
shanoi1_in_gggga(s(s(T31)), T18, T19, T20, T22) → U10_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T18, T20, T19, X26))
shanoi11_in_gggga(0, T57, T58, T59, .(mv(T57, T59), [])) → shanoi11_out_gggga(0, T57, T58, T59, .(mv(T57, T59), []))
shanoi11_in_gggga(s(T88), T69, T70, T71, X101) → U1_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, X98))
shanoi11_in_gggga(s(T88), T69, T70, T71, X101) → U2_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, T95))
U2_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U3_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T70, T69, T71, X99))
U3_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T70, T69, T71, X99)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U2_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_in_gggga(T88, T70, T69, T71, T108))
U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U5_gggga(T88, T69, T70, T71, X101, append28_in_aga(T95, .(mv(T69, T71), []), X100))
append28_in_aga([], T130, T130) → append28_out_aga([], T130, T130)
append28_in_aga(.(T137, T138), T139, .(T137, X178)) → U8_aga(T137, T138, T139, X178, append28_in_aga(T138, T139, X178))
U8_aga(T137, T138, T139, X178, append28_out_aga(T138, T139, X178)) → append28_out_aga(.(T137, T138), T139, .(T137, X178))
U5_gggga(T88, T69, T70, T71, X101, append28_out_aga(T95, .(mv(T69, T71), []), X100)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U6_gggga(T88, T69, T70, T71, X101, T108, append28_in_aga(T95, .(mv(T69, T71), []), T119))
U6_gggga(T88, T69, T70, T71, X101, T108, append28_out_aga(T95, .(mv(T69, T71), []), T119)) → U7_gggga(T88, T69, T70, T71, X101, append28_in_gaa(T119, T108, X101))
append28_in_gaa([], T130, T130) → append28_out_gaa([], T130, T130)
append28_in_gaa(.(T137, T138), T139, .(T137, X178)) → U8_gaa(T137, T138, T139, X178, append28_in_gaa(T138, T139, X178))
U8_gaa(T137, T138, T139, X178, append28_out_gaa(T138, T139, X178)) → append28_out_gaa(.(T137, T138), T139, .(T137, X178))
U7_gggga(T88, T69, T70, T71, X101, append28_out_gaa(T119, T108, X101)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U1_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, X98)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U10_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, X26)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
shanoi1_in_gggga(s(s(T31)), T18, T19, T20, T22) → U11_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T18, T20, T19, T38))
U11_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → U12_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T20, T18, T20, X27))
U12_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T20, T18, T20, X27)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
U11_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_in_gggga(T31, T20, T18, T20, T148))
U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → U14_gggga(T31, T18, T19, T20, T22, append40_in_aga(T38, .(mv(T18, T20), []), X28))
append40_in_aga([], T170, T170) → append40_out_aga([], T170, T170)
append40_in_aga(.(T179, T180), T181, .(T179, T183)) → U9_aga(T179, T180, T181, T183, append40_in_aga(T180, T181, T183))
U9_aga(T179, T180, T181, T183, append40_out_aga(T180, T181, T183)) → append40_out_aga(.(T179, T180), T181, .(T179, T183))
U14_gggga(T31, T18, T19, T20, T22, append40_out_aga(T38, .(mv(T18, T20), []), X28)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → U15_gggga(T31, T18, T19, T20, T22, T148, append40_in_aga(T38, .(mv(T18, T20), []), T159))
U15_gggga(T31, T18, T19, T20, T22, T148, append40_out_aga(T38, .(mv(T18, T20), []), T159)) → U16_gggga(T31, T18, T19, T20, T22, append40_in_gaa(T159, T148, T22))
append40_in_gaa([], T170, T170) → append40_out_gaa([], T170, T170)
append40_in_gaa(.(T179, T180), T181, .(T179, T183)) → U9_gaa(T179, T180, T181, T183, append40_in_gaa(T180, T181, T183))
U9_gaa(T179, T180, T181, T183, append40_out_gaa(T180, T181, T183)) → append40_out_gaa(.(T179, T180), T181, .(T179, T183))
U16_gggga(T31, T18, T19, T20, T22, append40_out_gaa(T159, T148, T22)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
APPEND40_IN_GAA(.(T179, T180), T181, .(T179, T183)) → APPEND40_IN_GAA(T180, T181, T183)
APPEND40_IN_GAA(.(T180)) → APPEND40_IN_GAA(T180)
From the DPs we obtained the following set of size-change graphs:
APPEND40_IN_AGA(.(T179, T180), T181, .(T179, T183)) → APPEND40_IN_AGA(T180, T181, T183)
shanoi1_in_gggga(s(0), T9, T10, T11, .(mv(T9, T11), [])) → shanoi1_out_gggga(s(0), T9, T10, T11, .(mv(T9, T11), []))
shanoi1_in_gggga(s(s(T31)), T18, T19, T20, T22) → U10_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T18, T20, T19, X26))
shanoi11_in_gggga(0, T57, T58, T59, .(mv(T57, T59), [])) → shanoi11_out_gggga(0, T57, T58, T59, .(mv(T57, T59), []))
shanoi11_in_gggga(s(T88), T69, T70, T71, X101) → U1_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, X98))
shanoi11_in_gggga(s(T88), T69, T70, T71, X101) → U2_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, T95))
U2_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U3_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T70, T69, T71, X99))
U3_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T70, T69, T71, X99)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U2_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_in_gggga(T88, T70, T69, T71, T108))
U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U5_gggga(T88, T69, T70, T71, X101, append28_in_aga(T95, .(mv(T69, T71), []), X100))
append28_in_aga([], T130, T130) → append28_out_aga([], T130, T130)
append28_in_aga(.(T137, T138), T139, .(T137, X178)) → U8_aga(T137, T138, T139, X178, append28_in_aga(T138, T139, X178))
U8_aga(T137, T138, T139, X178, append28_out_aga(T138, T139, X178)) → append28_out_aga(.(T137, T138), T139, .(T137, X178))
U5_gggga(T88, T69, T70, T71, X101, append28_out_aga(T95, .(mv(T69, T71), []), X100)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U6_gggga(T88, T69, T70, T71, X101, T108, append28_in_aga(T95, .(mv(T69, T71), []), T119))
U6_gggga(T88, T69, T70, T71, X101, T108, append28_out_aga(T95, .(mv(T69, T71), []), T119)) → U7_gggga(T88, T69, T70, T71, X101, append28_in_gaa(T119, T108, X101))
append28_in_gaa([], T130, T130) → append28_out_gaa([], T130, T130)
append28_in_gaa(.(T137, T138), T139, .(T137, X178)) → U8_gaa(T137, T138, T139, X178, append28_in_gaa(T138, T139, X178))
U8_gaa(T137, T138, T139, X178, append28_out_gaa(T138, T139, X178)) → append28_out_gaa(.(T137, T138), T139, .(T137, X178))
U7_gggga(T88, T69, T70, T71, X101, append28_out_gaa(T119, T108, X101)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U1_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, X98)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U10_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, X26)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
shanoi1_in_gggga(s(s(T31)), T18, T19, T20, T22) → U11_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T18, T20, T19, T38))
U11_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → U12_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T20, T18, T20, X27))
U12_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T20, T18, T20, X27)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
U11_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_in_gggga(T31, T20, T18, T20, T148))
U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → U14_gggga(T31, T18, T19, T20, T22, append40_in_aga(T38, .(mv(T18, T20), []), X28))
append40_in_aga([], T170, T170) → append40_out_aga([], T170, T170)
append40_in_aga(.(T179, T180), T181, .(T179, T183)) → U9_aga(T179, T180, T181, T183, append40_in_aga(T180, T181, T183))
U9_aga(T179, T180, T181, T183, append40_out_aga(T180, T181, T183)) → append40_out_aga(.(T179, T180), T181, .(T179, T183))
U14_gggga(T31, T18, T19, T20, T22, append40_out_aga(T38, .(mv(T18, T20), []), X28)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → U15_gggga(T31, T18, T19, T20, T22, T148, append40_in_aga(T38, .(mv(T18, T20), []), T159))
U15_gggga(T31, T18, T19, T20, T22, T148, append40_out_aga(T38, .(mv(T18, T20), []), T159)) → U16_gggga(T31, T18, T19, T20, T22, append40_in_gaa(T159, T148, T22))
append40_in_gaa([], T170, T170) → append40_out_gaa([], T170, T170)
append40_in_gaa(.(T179, T180), T181, .(T179, T183)) → U9_gaa(T179, T180, T181, T183, append40_in_gaa(T180, T181, T183))
U9_gaa(T179, T180, T181, T183, append40_out_gaa(T180, T181, T183)) → append40_out_gaa(.(T179, T180), T181, .(T179, T183))
U16_gggga(T31, T18, T19, T20, T22, append40_out_gaa(T159, T148, T22)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
APPEND40_IN_AGA(.(T179, T180), T181, .(T179, T183)) → APPEND40_IN_AGA(T180, T181, T183)
APPEND40_IN_AGA(T181) → APPEND40_IN_AGA(T181)
APPEND28_IN_GAA(.(T137, T138), T139, .(T137, X178)) → APPEND28_IN_GAA(T138, T139, X178)
shanoi1_in_gggga(s(0), T9, T10, T11, .(mv(T9, T11), [])) → shanoi1_out_gggga(s(0), T9, T10, T11, .(mv(T9, T11), []))
shanoi1_in_gggga(s(s(T31)), T18, T19, T20, T22) → U10_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T18, T20, T19, X26))
shanoi11_in_gggga(0, T57, T58, T59, .(mv(T57, T59), [])) → shanoi11_out_gggga(0, T57, T58, T59, .(mv(T57, T59), []))
shanoi11_in_gggga(s(T88), T69, T70, T71, X101) → U1_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, X98))
shanoi11_in_gggga(s(T88), T69, T70, T71, X101) → U2_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, T95))
U2_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U3_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T70, T69, T71, X99))
U3_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T70, T69, T71, X99)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U2_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_in_gggga(T88, T70, T69, T71, T108))
U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U5_gggga(T88, T69, T70, T71, X101, append28_in_aga(T95, .(mv(T69, T71), []), X100))
append28_in_aga([], T130, T130) → append28_out_aga([], T130, T130)
append28_in_aga(.(T137, T138), T139, .(T137, X178)) → U8_aga(T137, T138, T139, X178, append28_in_aga(T138, T139, X178))
U8_aga(T137, T138, T139, X178, append28_out_aga(T138, T139, X178)) → append28_out_aga(.(T137, T138), T139, .(T137, X178))
U5_gggga(T88, T69, T70, T71, X101, append28_out_aga(T95, .(mv(T69, T71), []), X100)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U6_gggga(T88, T69, T70, T71, X101, T108, append28_in_aga(T95, .(mv(T69, T71), []), T119))
U6_gggga(T88, T69, T70, T71, X101, T108, append28_out_aga(T95, .(mv(T69, T71), []), T119)) → U7_gggga(T88, T69, T70, T71, X101, append28_in_gaa(T119, T108, X101))
append28_in_gaa([], T130, T130) → append28_out_gaa([], T130, T130)
append28_in_gaa(.(T137, T138), T139, .(T137, X178)) → U8_gaa(T137, T138, T139, X178, append28_in_gaa(T138, T139, X178))
U8_gaa(T137, T138, T139, X178, append28_out_gaa(T138, T139, X178)) → append28_out_gaa(.(T137, T138), T139, .(T137, X178))
U7_gggga(T88, T69, T70, T71, X101, append28_out_gaa(T119, T108, X101)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U1_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, X98)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U10_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, X26)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
shanoi1_in_gggga(s(s(T31)), T18, T19, T20, T22) → U11_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T18, T20, T19, T38))
U11_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → U12_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T20, T18, T20, X27))
U12_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T20, T18, T20, X27)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
U11_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_in_gggga(T31, T20, T18, T20, T148))
U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → U14_gggga(T31, T18, T19, T20, T22, append40_in_aga(T38, .(mv(T18, T20), []), X28))
append40_in_aga([], T170, T170) → append40_out_aga([], T170, T170)
append40_in_aga(.(T179, T180), T181, .(T179, T183)) → U9_aga(T179, T180, T181, T183, append40_in_aga(T180, T181, T183))
U9_aga(T179, T180, T181, T183, append40_out_aga(T180, T181, T183)) → append40_out_aga(.(T179, T180), T181, .(T179, T183))
U14_gggga(T31, T18, T19, T20, T22, append40_out_aga(T38, .(mv(T18, T20), []), X28)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → U15_gggga(T31, T18, T19, T20, T22, T148, append40_in_aga(T38, .(mv(T18, T20), []), T159))
U15_gggga(T31, T18, T19, T20, T22, T148, append40_out_aga(T38, .(mv(T18, T20), []), T159)) → U16_gggga(T31, T18, T19, T20, T22, append40_in_gaa(T159, T148, T22))
append40_in_gaa([], T170, T170) → append40_out_gaa([], T170, T170)
append40_in_gaa(.(T179, T180), T181, .(T179, T183)) → U9_gaa(T179, T180, T181, T183, append40_in_gaa(T180, T181, T183))
U9_gaa(T179, T180, T181, T183, append40_out_gaa(T180, T181, T183)) → append40_out_gaa(.(T179, T180), T181, .(T179, T183))
U16_gggga(T31, T18, T19, T20, T22, append40_out_gaa(T159, T148, T22)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
APPEND28_IN_GAA(.(T137, T138), T139, .(T137, X178)) → APPEND28_IN_GAA(T138, T139, X178)
APPEND28_IN_GAA(.(T138)) → APPEND28_IN_GAA(T138)
From the DPs we obtained the following set of size-change graphs:
APPEND28_IN_AGA(.(T137, T138), T139, .(T137, X178)) → APPEND28_IN_AGA(T138, T139, X178)
shanoi1_in_gggga(s(0), T9, T10, T11, .(mv(T9, T11), [])) → shanoi1_out_gggga(s(0), T9, T10, T11, .(mv(T9, T11), []))
shanoi1_in_gggga(s(s(T31)), T18, T19, T20, T22) → U10_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T18, T20, T19, X26))
shanoi11_in_gggga(0, T57, T58, T59, .(mv(T57, T59), [])) → shanoi11_out_gggga(0, T57, T58, T59, .(mv(T57, T59), []))
shanoi11_in_gggga(s(T88), T69, T70, T71, X101) → U1_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, X98))
shanoi11_in_gggga(s(T88), T69, T70, T71, X101) → U2_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, T95))
U2_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U3_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T70, T69, T71, X99))
U3_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T70, T69, T71, X99)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U2_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_in_gggga(T88, T70, T69, T71, T108))
U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U5_gggga(T88, T69, T70, T71, X101, append28_in_aga(T95, .(mv(T69, T71), []), X100))
append28_in_aga([], T130, T130) → append28_out_aga([], T130, T130)
append28_in_aga(.(T137, T138), T139, .(T137, X178)) → U8_aga(T137, T138, T139, X178, append28_in_aga(T138, T139, X178))
U8_aga(T137, T138, T139, X178, append28_out_aga(T138, T139, X178)) → append28_out_aga(.(T137, T138), T139, .(T137, X178))
U5_gggga(T88, T69, T70, T71, X101, append28_out_aga(T95, .(mv(T69, T71), []), X100)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U6_gggga(T88, T69, T70, T71, X101, T108, append28_in_aga(T95, .(mv(T69, T71), []), T119))
U6_gggga(T88, T69, T70, T71, X101, T108, append28_out_aga(T95, .(mv(T69, T71), []), T119)) → U7_gggga(T88, T69, T70, T71, X101, append28_in_gaa(T119, T108, X101))
append28_in_gaa([], T130, T130) → append28_out_gaa([], T130, T130)
append28_in_gaa(.(T137, T138), T139, .(T137, X178)) → U8_gaa(T137, T138, T139, X178, append28_in_gaa(T138, T139, X178))
U8_gaa(T137, T138, T139, X178, append28_out_gaa(T138, T139, X178)) → append28_out_gaa(.(T137, T138), T139, .(T137, X178))
U7_gggga(T88, T69, T70, T71, X101, append28_out_gaa(T119, T108, X101)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U1_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, X98)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U10_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, X26)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
shanoi1_in_gggga(s(s(T31)), T18, T19, T20, T22) → U11_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T18, T20, T19, T38))
U11_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → U12_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T20, T18, T20, X27))
U12_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T20, T18, T20, X27)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
U11_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_in_gggga(T31, T20, T18, T20, T148))
U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → U14_gggga(T31, T18, T19, T20, T22, append40_in_aga(T38, .(mv(T18, T20), []), X28))
append40_in_aga([], T170, T170) → append40_out_aga([], T170, T170)
append40_in_aga(.(T179, T180), T181, .(T179, T183)) → U9_aga(T179, T180, T181, T183, append40_in_aga(T180, T181, T183))
U9_aga(T179, T180, T181, T183, append40_out_aga(T180, T181, T183)) → append40_out_aga(.(T179, T180), T181, .(T179, T183))
U14_gggga(T31, T18, T19, T20, T22, append40_out_aga(T38, .(mv(T18, T20), []), X28)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → U15_gggga(T31, T18, T19, T20, T22, T148, append40_in_aga(T38, .(mv(T18, T20), []), T159))
U15_gggga(T31, T18, T19, T20, T22, T148, append40_out_aga(T38, .(mv(T18, T20), []), T159)) → U16_gggga(T31, T18, T19, T20, T22, append40_in_gaa(T159, T148, T22))
append40_in_gaa([], T170, T170) → append40_out_gaa([], T170, T170)
append40_in_gaa(.(T179, T180), T181, .(T179, T183)) → U9_gaa(T179, T180, T181, T183, append40_in_gaa(T180, T181, T183))
U9_gaa(T179, T180, T181, T183, append40_out_gaa(T180, T181, T183)) → append40_out_gaa(.(T179, T180), T181, .(T179, T183))
U16_gggga(T31, T18, T19, T20, T22, append40_out_gaa(T159, T148, T22)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
APPEND28_IN_AGA(.(T137, T138), T139, .(T137, X178)) → APPEND28_IN_AGA(T138, T139, X178)
APPEND28_IN_AGA(T139) → APPEND28_IN_AGA(T139)
SHANOI11_IN_GGGGA(s(T88), T69, T70, T71, X101) → U2_GGGGA(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, T95))
U2_GGGGA(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → SHANOI11_IN_GGGGA(T88, T70, T69, T71, X99)
SHANOI11_IN_GGGGA(s(T88), T69, T70, T71, X101) → SHANOI11_IN_GGGGA(T88, T69, T71, T70, X98)
shanoi1_in_gggga(s(0), T9, T10, T11, .(mv(T9, T11), [])) → shanoi1_out_gggga(s(0), T9, T10, T11, .(mv(T9, T11), []))
shanoi1_in_gggga(s(s(T31)), T18, T19, T20, T22) → U10_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T18, T20, T19, X26))
shanoi11_in_gggga(0, T57, T58, T59, .(mv(T57, T59), [])) → shanoi11_out_gggga(0, T57, T58, T59, .(mv(T57, T59), []))
shanoi11_in_gggga(s(T88), T69, T70, T71, X101) → U1_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, X98))
shanoi11_in_gggga(s(T88), T69, T70, T71, X101) → U2_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, T95))
U2_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U3_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T70, T69, T71, X99))
U3_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T70, T69, T71, X99)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U2_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_in_gggga(T88, T70, T69, T71, T108))
U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U5_gggga(T88, T69, T70, T71, X101, append28_in_aga(T95, .(mv(T69, T71), []), X100))
append28_in_aga([], T130, T130) → append28_out_aga([], T130, T130)
append28_in_aga(.(T137, T138), T139, .(T137, X178)) → U8_aga(T137, T138, T139, X178, append28_in_aga(T138, T139, X178))
U8_aga(T137, T138, T139, X178, append28_out_aga(T138, T139, X178)) → append28_out_aga(.(T137, T138), T139, .(T137, X178))
U5_gggga(T88, T69, T70, T71, X101, append28_out_aga(T95, .(mv(T69, T71), []), X100)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U6_gggga(T88, T69, T70, T71, X101, T108, append28_in_aga(T95, .(mv(T69, T71), []), T119))
U6_gggga(T88, T69, T70, T71, X101, T108, append28_out_aga(T95, .(mv(T69, T71), []), T119)) → U7_gggga(T88, T69, T70, T71, X101, append28_in_gaa(T119, T108, X101))
append28_in_gaa([], T130, T130) → append28_out_gaa([], T130, T130)
append28_in_gaa(.(T137, T138), T139, .(T137, X178)) → U8_gaa(T137, T138, T139, X178, append28_in_gaa(T138, T139, X178))
U8_gaa(T137, T138, T139, X178, append28_out_gaa(T138, T139, X178)) → append28_out_gaa(.(T137, T138), T139, .(T137, X178))
U7_gggga(T88, T69, T70, T71, X101, append28_out_gaa(T119, T108, X101)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U1_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, X98)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U10_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, X26)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
shanoi1_in_gggga(s(s(T31)), T18, T19, T20, T22) → U11_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T18, T20, T19, T38))
U11_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → U12_gggga(T31, T18, T19, T20, T22, shanoi11_in_gggga(T31, T20, T18, T20, X27))
U12_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T20, T18, T20, X27)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
U11_gggga(T31, T18, T19, T20, T22, shanoi11_out_gggga(T31, T18, T20, T19, T38)) → U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_in_gggga(T31, T20, T18, T20, T148))
U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → U14_gggga(T31, T18, T19, T20, T22, append40_in_aga(T38, .(mv(T18, T20), []), X28))
append40_in_aga([], T170, T170) → append40_out_aga([], T170, T170)
append40_in_aga(.(T179, T180), T181, .(T179, T183)) → U9_aga(T179, T180, T181, T183, append40_in_aga(T180, T181, T183))
U9_aga(T179, T180, T181, T183, append40_out_aga(T180, T181, T183)) → append40_out_aga(.(T179, T180), T181, .(T179, T183))
U14_gggga(T31, T18, T19, T20, T22, append40_out_aga(T38, .(mv(T18, T20), []), X28)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
U13_gggga(T31, T18, T19, T20, T22, T38, shanoi11_out_gggga(T31, T20, T18, T20, T148)) → U15_gggga(T31, T18, T19, T20, T22, T148, append40_in_aga(T38, .(mv(T18, T20), []), T159))
U15_gggga(T31, T18, T19, T20, T22, T148, append40_out_aga(T38, .(mv(T18, T20), []), T159)) → U16_gggga(T31, T18, T19, T20, T22, append40_in_gaa(T159, T148, T22))
append40_in_gaa([], T170, T170) → append40_out_gaa([], T170, T170)
append40_in_gaa(.(T179, T180), T181, .(T179, T183)) → U9_gaa(T179, T180, T181, T183, append40_in_gaa(T180, T181, T183))
U9_gaa(T179, T180, T181, T183, append40_out_gaa(T180, T181, T183)) → append40_out_gaa(.(T179, T180), T181, .(T179, T183))
U16_gggga(T31, T18, T19, T20, T22, append40_out_gaa(T159, T148, T22)) → shanoi1_out_gggga(s(s(T31)), T18, T19, T20, T22)
SHANOI11_IN_GGGGA(s(T88), T69, T70, T71, X101) → U2_GGGGA(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, T95))
U2_GGGGA(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → SHANOI11_IN_GGGGA(T88, T70, T69, T71, X99)
SHANOI11_IN_GGGGA(s(T88), T69, T70, T71, X101) → SHANOI11_IN_GGGGA(T88, T69, T71, T70, X98)
shanoi11_in_gggga(0, T57, T58, T59, .(mv(T57, T59), [])) → shanoi11_out_gggga(0, T57, T58, T59, .(mv(T57, T59), []))
shanoi11_in_gggga(s(T88), T69, T70, T71, X101) → U1_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, X98))
shanoi11_in_gggga(s(T88), T69, T70, T71, X101) → U2_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T69, T71, T70, T95))
U1_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, X98)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U2_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U3_gggga(T88, T69, T70, T71, X101, shanoi11_in_gggga(T88, T70, T69, T71, X99))
U2_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T69, T71, T70, T95)) → U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_in_gggga(T88, T70, T69, T71, T108))
U3_gggga(T88, T69, T70, T71, X101, shanoi11_out_gggga(T88, T70, T69, T71, X99)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U5_gggga(T88, T69, T70, T71, X101, append28_in_aga(T95, .(mv(T69, T71), []), X100))
U4_gggga(T88, T69, T70, T71, X101, T95, shanoi11_out_gggga(T88, T70, T69, T71, T108)) → U6_gggga(T88, T69, T70, T71, X101, T108, append28_in_aga(T95, .(mv(T69, T71), []), T119))
U5_gggga(T88, T69, T70, T71, X101, append28_out_aga(T95, .(mv(T69, T71), []), X100)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U6_gggga(T88, T69, T70, T71, X101, T108, append28_out_aga(T95, .(mv(T69, T71), []), T119)) → U7_gggga(T88, T69, T70, T71, X101, append28_in_gaa(T119, T108, X101))
append28_in_aga([], T130, T130) → append28_out_aga([], T130, T130)
append28_in_aga(.(T137, T138), T139, .(T137, X178)) → U8_aga(T137, T138, T139, X178, append28_in_aga(T138, T139, X178))
U7_gggga(T88, T69, T70, T71, X101, append28_out_gaa(T119, T108, X101)) → shanoi11_out_gggga(s(T88), T69, T70, T71, X101)
U8_aga(T137, T138, T139, X178, append28_out_aga(T138, T139, X178)) → append28_out_aga(.(T137, T138), T139, .(T137, X178))
append28_in_gaa([], T130, T130) → append28_out_gaa([], T130, T130)
append28_in_gaa(.(T137, T138), T139, .(T137, X178)) → U8_gaa(T137, T138, T139, X178, append28_in_gaa(T138, T139, X178))
U8_gaa(T137, T138, T139, X178, append28_out_gaa(T138, T139, X178)) → append28_out_gaa(.(T137, T138), T139, .(T137, X178))
SHANOI11_IN_GGGGA(s(T88), T69, T70, T71) → U2_GGGGA(T88, T69, T70, T71, shanoi11_in_gggga(T88, T69, T71, T70))
U2_GGGGA(T88, T69, T70, T71, shanoi11_out_gggga(T88, T69, T71, T70)) → SHANOI11_IN_GGGGA(T88, T70, T69, T71)
SHANOI11_IN_GGGGA(s(T88), T69, T70, T71) → SHANOI11_IN_GGGGA(T88, T69, T71, T70)
shanoi11_in_gggga(0, T57, T58, T59) → shanoi11_out_gggga(0, T57, T58, T59)
shanoi11_in_gggga(s(T88), T69, T70, T71) → U1_gggga(T88, T69, T70, T71, shanoi11_in_gggga(T88, T69, T71, T70))
shanoi11_in_gggga(s(T88), T69, T70, T71) → U2_gggga(T88, T69, T70, T71, shanoi11_in_gggga(T88, T69, T71, T70))
U1_gggga(T88, T69, T70, T71, shanoi11_out_gggga(T88, T69, T71, T70)) → shanoi11_out_gggga(s(T88), T69, T70, T71)
U2_gggga(T88, T69, T70, T71, shanoi11_out_gggga(T88, T69, T71, T70)) → U3_gggga(T88, T69, T70, T71, shanoi11_in_gggga(T88, T70, T69, T71))
U2_gggga(T88, T69, T70, T71, shanoi11_out_gggga(T88, T69, T71, T70)) → U4_gggga(T88, T69, T70, T71, shanoi11_in_gggga(T88, T70, T69, T71))
U3_gggga(T88, T69, T70, T71, shanoi11_out_gggga(T88, T70, T69, T71)) → shanoi11_out_gggga(s(T88), T69, T70, T71)
U4_gggga(T88, T69, T70, T71, shanoi11_out_gggga(T88, T70, T69, T71)) → U5_gggga(T88, T69, T70, T71, append28_in_aga(.([])))
U4_gggga(T88, T69, T70, T71, shanoi11_out_gggga(T88, T70, T69, T71)) → U6_gggga(T88, T69, T70, T71, append28_in_aga(.([])))
U5_gggga(T88, T69, T70, T71, append28_out_aga(T95, .([]), X100)) → shanoi11_out_gggga(s(T88), T69, T70, T71)
U6_gggga(T88, T69, T70, T71, append28_out_aga(T95, .([]), T119)) → U7_gggga(T88, T69, T70, T71, append28_in_gaa(T119))
append28_in_aga(T130) → append28_out_aga([], T130, T130)
append28_in_aga(T139) → U8_aga(T139, append28_in_aga(T139))
U7_gggga(T88, T69, T70, T71, append28_out_gaa(T119)) → shanoi11_out_gggga(s(T88), T69, T70, T71)
U8_aga(T139, append28_out_aga(T138, T139, X178)) → append28_out_aga(.(T138), T139, .(X178))
append28_in_gaa([]) → append28_out_gaa([])
append28_in_gaa(.(T138)) → U8_gaa(T138, append28_in_gaa(T138))
U8_gaa(T138, append28_out_gaa(T138)) → append28_out_gaa(.(T138))
shanoi11_in_gggga(x0, x1, x2, x3)
U1_gggga(x0, x1, x2, x3, x4)
U2_gggga(x0, x1, x2, x3, x4)
U3_gggga(x0, x1, x2, x3, x4)
U4_gggga(x0, x1, x2, x3, x4)
U5_gggga(x0, x1, x2, x3, x4)
U6_gggga(x0, x1, x2, x3, x4)
append28_in_aga(x0)
U7_gggga(x0, x1, x2, x3, x4)
U8_aga(x0, x1)
append28_in_gaa(x0)
U8_gaa(x0, x1)
From the DPs we obtained the following set of size-change graphs: