(0) Obligation:
Clauses:shanoi(s(0), A, B, C, .(mv(A, C), [])).
shanoi(s(s(X)), A, B, C, M) :- ','(eq(N1, s(X)), ','(shanoi(N1, A, C, B, M1), ','(shanoi(N1, B, A, C, M2), ','(append(M1, .(mv(A, C), []), T), append(T, M2, M))))).
append([], L, L).
append(.(H, L), L1, .(H, R)) :- append(L, L1, R).
eq(X, X).
Queries:
shanoi(g,g,g,g,a).
(1) PrologToDTProblemTransformerProof (SOUND transformation)
Built DT problem from termination graph.
(2) Obligation:
Triples:shanoi11(s(T88), T69, T70, T71, X101) :- shanoi11(T88, T69, T71, T70, X98).
shanoi11(s(T88), T69, T70, T71, X101) :- ','(shanoic11(T88, T69, T71, T70, T95), shanoi11(T88, T70, T69, T71, X99)).
shanoi11(s(T88), T69, T70, T71, X101) :- ','(shanoic11(T88, T69, T71, T70, T95), ','(shanoic11(T88, T70, T69, T71, T108), append28(T95, .(mv(T69, T71), []), X100))).
shanoi11(s(T88), T69, T70, T71, X101) :- ','(shanoic11(T88, T69, T71, T70, T95), ','(shanoic11(T88, T70, T69, T71, T108), ','(appendc28(T95, .(mv(T69, T71), []), T119), append28(T119, T108, X101)))).
append28(.(T137, T138), T139, .(T137, X178)) :- append28(T138, T139, X178).
append40(.(T179, T180), T181, .(T179, T183)) :- append40(T180, T181, T183).
shanoi1(s(s(T31)), T18, T19, T20, T22) :- shanoi11(T31, T18, T20, T19, X26).
shanoi1(s(s(T31)), T18, T19, T20, T22) :- ','(shanoic11(T31, T18, T20, T19, T38), shanoi11(T31, T20, T18, T20, X27)).
shanoi1(s(s(T31)), T18, T19, T20, T22) :- ','(shanoic11(T31, T18, T20, T19, T38), ','(shanoic11(T31, T20, T18, T20, T148), append40(T38, .(mv(T18, T20), []), X28))).
shanoi1(s(s(T31)), T18, T19, T20, T22) :- ','(shanoic11(T31, T18, T20, T19, T38), ','(shanoic11(T31, T20, T18, T20, T148), ','(appendc40(T38, .(mv(T18, T20), []), T159), append40(T159, T148, T22)))).
Clauses:
shanoic11(0, T57, T58, T59, .(mv(T57, T59), [])).
shanoic11(s(T88), T69, T70, T71, X101) :- ','(shanoic11(T88, T69, T71, T70, T95), ','(shanoic11(T88, T70, T69, T71, T108), ','(appendc28(T95, .(mv(T69, T71), []), T119), appendc28(T119, T108, X101)))).
appendc28([], T130, T130).
appendc28(.(T137, T138), T139, .(T137, X178)) :- appendc28(T138, T139, X178).
appendc40([], T170, T170).
appendc40(.(T179, T180), T181, .(T179, T183)) :- appendc40(T180, T181, T183).
Afs:
shanoi1(x1, x2, x3, x4, x5) = shanoi1(x1, x2, x3, x4)
(3) TriplesToPiDPProof (SOUND transformation)
We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:shanoi1_in: (b,b,b,b,f)
shanoi11_in: (b,b,b,b,f)
shanoic11_in: (b,b,b,b,f)
appendc28_in: (b,b,f)
append28_in: (b,b,f)
append40_in: (b,b,f)
appendc40_in: (b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:
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, shanoic11_in_gggga(T88, T69, T71, T70, T95))
U2_GGGGA(T88, T69, T70, T71, X101, shanoic11_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, shanoic11_out_gggga(T88, T69, T71, T70, T95)) → SHANOI11_IN_GGGGA(T88, T70, T69, T71, X99)
U2_GGGGA(T88, T69, T70, T71, X101, shanoic11_out_gggga(T88, T69, T71, T70, T95)) → U4_GGGGA(T88, T69, T70, T71, X101, T95, shanoic11_in_gggga(T88, T70, T69, T71, T108))
U4_GGGGA(T88, T69, T70, T71, X101, T95, shanoic11_out_gggga(T88, T70, T69, T71, T108)) → U5_GGGGA(T88, T69, T70, T71, X101, append28_in_gga(T95, .(mv(T69, T71), []), X100))
U4_GGGGA(T88, T69, T70, T71, X101, T95, shanoic11_out_gggga(T88, T70, T69, T71, T108)) → APPEND28_IN_GGA(T95, .(mv(T69, T71), []), X100)
APPEND28_IN_GGA(.(T137, T138), T139, .(T137, X178)) → U8_GGA(T137, T138, T139, X178, append28_in_gga(T138, T139, X178))
APPEND28_IN_GGA(.(T137, T138), T139, .(T137, X178)) → APPEND28_IN_GGA(T138, T139, X178)
U4_GGGGA(T88, T69, T70, T71, X101, T95, shanoic11_out_gggga(T88, T70, T69, T71, T108)) → U6_GGGGA(T88, T69, T70, T71, X101, T108, appendc28_in_gga(T95, .(mv(T69, T71), []), T119))
U6_GGGGA(T88, T69, T70, T71, X101, T108, appendc28_out_gga(T95, .(mv(T69, T71), []), T119)) → U7_GGGGA(T88, T69, T70, T71, X101, append28_in_gga(T119, T108, X101))
U6_GGGGA(T88, T69, T70, T71, X101, T108, appendc28_out_gga(T95, .(mv(T69, T71), []), T119)) → APPEND28_IN_GGA(T119, T108, X101)
SHANOI1_IN_GGGGA(s(s(T31)), T18, T19, T20, T22) → U11_GGGGA(T31, T18, T19, T20, T22, shanoic11_in_gggga(T31, T18, T20, T19, T38))
U11_GGGGA(T31, T18, T19, T20, T22, shanoic11_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, shanoic11_out_gggga(T31, T18, T20, T19, T38)) → SHANOI11_IN_GGGGA(T31, T20, T18, T20, X27)
U11_GGGGA(T31, T18, T19, T20, T22, shanoic11_out_gggga(T31, T18, T20, T19, T38)) → U13_GGGGA(T31, T18, T19, T20, T22, T38, shanoic11_in_gggga(T31, T20, T18, T20, T148))
U13_GGGGA(T31, T18, T19, T20, T22, T38, shanoic11_out_gggga(T31, T20, T18, T20, T148)) → U14_GGGGA(T31, T18, T19, T20, T22, append40_in_gga(T38, .(mv(T18, T20), []), X28))
U13_GGGGA(T31, T18, T19, T20, T22, T38, shanoic11_out_gggga(T31, T20, T18, T20, T148)) → APPEND40_IN_GGA(T38, .(mv(T18, T20), []), X28)
APPEND40_IN_GGA(.(T179, T180), T181, .(T179, T183)) → U9_GGA(T179, T180, T181, T183, append40_in_gga(T180, T181, T183))
APPEND40_IN_GGA(.(T179, T180), T181, .(T179, T183)) → APPEND40_IN_GGA(T180, T181, T183)
U13_GGGGA(T31, T18, T19, T20, T22, T38, shanoic11_out_gggga(T31, T20, T18, T20, T148)) → U15_GGGGA(T31, T18, T19, T20, T22, T148, appendc40_in_gga(T38, .(mv(T18, T20), []), T159))
U15_GGGGA(T31, T18, T19, T20, T22, T148, appendc40_out_gga(T38, .(mv(T18, T20), []), T159)) → U16_GGGGA(T31, T18, T19, T20, T22, append40_in_gga(T159, T148, T22))
U15_GGGGA(T31, T18, T19, T20, T22, T148, appendc40_out_gga(T38, .(mv(T18, T20), []), T159)) → APPEND40_IN_GGA(T159, T148, T22)
The TRS R consists of the following rules:
shanoic11_in_gggga(0, T57, T58, T59, .(mv(T57, T59), [])) → shanoic11_out_gggga(0, T57, T58, T59, .(mv(T57, T59), []))
shanoic11_in_gggga(s(T88), T69, T70, T71, X101) → U18_gggga(T88, T69, T70, T71, X101, shanoic11_in_gggga(T88, T69, T71, T70, T95))
U18_gggga(T88, T69, T70, T71, X101, shanoic11_out_gggga(T88, T69, T71, T70, T95)) → U19_gggga(T88, T69, T70, T71, X101, T95, shanoic11_in_gggga(T88, T70, T69, T71, T108))
U19_gggga(T88, T69, T70, T71, X101, T95, shanoic11_out_gggga(T88, T70, T69, T71, T108)) → U20_gggga(T88, T69, T70, T71, X101, T108, appendc28_in_gga(T95, .(mv(T69, T71), []), T119))
appendc28_in_gga([], T130, T130) → appendc28_out_gga([], T130, T130)
appendc28_in_gga(.(T137, T138), T139, .(T137, X178)) → U22_gga(T137, T138, T139, X178, appendc28_in_gga(T138, T139, X178))
U22_gga(T137, T138, T139, X178, appendc28_out_gga(T138, T139, X178)) → appendc28_out_gga(.(T137, T138), T139, .(T137, X178))
U20_gggga(T88, T69, T70, T71, X101, T108, appendc28_out_gga(T95, .(mv(T69, T71), []), T119)) → U21_gggga(T88, T69, T70, T71, X101, appendc28_in_gga(T119, T108, X101))
U21_gggga(T88, T69, T70, T71, X101, appendc28_out_gga(T119, T108, X101)) → shanoic11_out_gggga(s(T88), T69, T70, T71, X101)
appendc40_in_gga([], T170, T170) → appendc40_out_gga([], T170, T170)
appendc40_in_gga(.(T179, T180), T181, .(T179, T183)) → U23_gga(T179, T180, T181, T183, appendc40_in_gga(T180, T181, T183))
U23_gga(T179, T180, T181, T183, appendc40_out_gga(T180, T181, T183)) → appendc40_out_gga(.(T179, T180), T181, .(T179, T183))
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
shanoi11_in_gggga(x1, x2, x3, x4, x5) = shanoi11_in_gggga(x1, x2, x3, x4)
shanoic11_in_gggga(x1, x2, x3, x4, x5) = shanoic11_in_gggga(x1, x2, x3, x4)
0 = 0
shanoic11_out_gggga(x1, x2, x3, x4, x5) = shanoic11_out_gggga(x1, x2, x3, x4, x5)
U18_gggga(x1, x2, x3, x4, x5, x6) = U18_gggga(x1, x2, x3, x4, x6)
U19_gggga(x1, x2, x3, x4, x5, x6, x7) = U19_gggga(x1, x2, x3, x4, x6, x7)
U20_gggga(x1, x2, x3, x4, x5, x6, x7) = U20_gggga(x1, x2, x3, x4, x6, x7)
appendc28_in_gga(x1, x2, x3) = appendc28_in_gga(x1, x2)
[] = []
appendc28_out_gga(x1, x2, x3) = appendc28_out_gga(x1, x2, x3)
.(x1, x2) = .(x1, x2)
U22_gga(x1, x2, x3, x4, x5) = U22_gga(x1, x2, x3, x5)
mv(x1, x2) = mv(x1, x2)
U21_gggga(x1, x2, x3, x4, x5, x6) = U21_gggga(x1, x2, x3, x4, x6)
append28_in_gga(x1, x2, x3) = append28_in_gga(x1, x2)
append40_in_gga(x1, x2, x3) = append40_in_gga(x1, x2)
appendc40_in_gga(x1, x2, x3) = appendc40_in_gga(x1, x2)
appendc40_out_gga(x1, x2, x3) = appendc40_out_gga(x1, x2, x3)
U23_gga(x1, x2, x3, x4, x5) = U23_gga(x1, x2, x3, x5)
SHANOI1_IN_GGGGA(x1, x2, x3, x4, x5) = SHANOI1_IN_GGGGA(x1, x2, x3, x4)
U10_GGGGA(x1, x2, x3, x4, x5, x6) = U10_GGGGA(x1, x2, x3, x4, x6)
SHANOI11_IN_GGGGA(x1, x2, x3, x4, x5) = SHANOI11_IN_GGGGA(x1, x2, x3, x4)
U1_GGGGA(x1, x2, x3, x4, x5, x6) = U1_GGGGA(x1, x2, x3, x4, x6)
U2_GGGGA(x1, x2, x3, x4, x5, x6) = U2_GGGGA(x1, x2, x3, x4, x6)
U3_GGGGA(x1, x2, x3, x4, x5, x6) = U3_GGGGA(x1, x2, x3, x4, x6)
U4_GGGGA(x1, x2, x3, x4, x5, x6, x7) = U4_GGGGA(x1, x2, x3, x4, x6, x7)
U5_GGGGA(x1, x2, x3, x4, x5, x6) = U5_GGGGA(x1, x2, x3, x4, x6)
APPEND28_IN_GGA(x1, x2, x3) = APPEND28_IN_GGA(x1, x2)
U8_GGA(x1, x2, x3, x4, x5) = U8_GGA(x1, x2, x3, x5)
U6_GGGGA(x1, x2, x3, x4, x5, x6, x7) = U6_GGGGA(x1, x2, x3, x4, x6, x7)
U7_GGGGA(x1, x2, x3, x4, x5, x6) = U7_GGGGA(x1, x2, x3, x4, x6)
U11_GGGGA(x1, x2, x3, x4, x5, x6) = U11_GGGGA(x1, x2, x3, x4, x6)
U12_GGGGA(x1, x2, x3, x4, x5, x6) = U12_GGGGA(x1, x2, x3, x4, x6)
U13_GGGGA(x1, x2, x3, x4, x5, x6, x7) = U13_GGGGA(x1, x2, x3, x4, x6, x7)
U14_GGGGA(x1, x2, x3, x4, x5, x6) = U14_GGGGA(x1, x2, x3, x4, x6)
APPEND40_IN_GGA(x1, x2, x3) = APPEND40_IN_GGA(x1, x2)
U9_GGA(x1, x2, x3, x4, x5) = U9_GGA(x1, x2, x3, x5)
U15_GGGGA(x1, x2, x3, x4, x5, x6, x7) = U15_GGGGA(x1, x2, x3, x4, x6, x7)
U16_GGGGA(x1, x2, x3, x4, x5, x6) = U16_GGGGA(x1, x2, x3, x4, x6)
We have to consider all (P,R,Pi)-chains
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
(4) Obligation:
Pi DP problem:The TRS P consists of the following rules:
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, shanoic11_in_gggga(T88, T69, T71, T70, T95))
U2_GGGGA(T88, T69, T70, T71, X101, shanoic11_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, shanoic11_out_gggga(T88, T69, T71, T70, T95)) → SHANOI11_IN_GGGGA(T88, T70, T69, T71, X99)
U2_GGGGA(T88, T69, T70, T71, X101, shanoic11_out_gggga(T88, T69, T71, T70, T95)) → U4_GGGGA(T88, T69, T70, T71, X101, T95, shanoic11_in_gggga(T88, T70, T69, T71, T108))
U4_GGGGA(T88, T69, T70, T71, X101, T95, shanoic11_out_gggga(T88, T70, T69, T71, T108)) → U5_GGGGA(T88, T69, T70, T71, X101, append28_in_gga(T95, .(mv(T69, T71), []), X100))
U4_GGGGA(T88, T69, T70, T71, X101, T95, shanoic11_out_gggga(T88, T70, T69, T71, T108)) → APPEND28_IN_GGA(T95, .(mv(T69, T71), []), X100)
APPEND28_IN_GGA(.(T137, T138), T139, .(T137, X178)) → U8_GGA(T137, T138, T139, X178, append28_in_gga(T138, T139, X178))
APPEND28_IN_GGA(.(T137, T138), T139, .(T137, X178)) → APPEND28_IN_GGA(T138, T139, X178)
U4_GGGGA(T88, T69, T70, T71, X101, T95, shanoic11_out_gggga(T88, T70, T69, T71, T108)) → U6_GGGGA(T88, T69, T70, T71, X101, T108, appendc28_in_gga(T95, .(mv(T69, T71), []), T119))
U6_GGGGA(T88, T69, T70, T71, X101, T108, appendc28_out_gga(T95, .(mv(T69, T71), []), T119)) → U7_GGGGA(T88, T69, T70, T71, X101, append28_in_gga(T119, T108, X101))
U6_GGGGA(T88, T69, T70, T71, X101, T108, appendc28_out_gga(T95, .(mv(T69, T71), []), T119)) → APPEND28_IN_GGA(T119, T108, X101)
SHANOI1_IN_GGGGA(s(s(T31)), T18, T19, T20, T22) → U11_GGGGA(T31, T18, T19, T20, T22, shanoic11_in_gggga(T31, T18, T20, T19, T38))
U11_GGGGA(T31, T18, T19, T20, T22, shanoic11_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, shanoic11_out_gggga(T31, T18, T20, T19, T38)) → SHANOI11_IN_GGGGA(T31, T20, T18, T20, X27)
U11_GGGGA(T31, T18, T19, T20, T22, shanoic11_out_gggga(T31, T18, T20, T19, T38)) → U13_GGGGA(T31, T18, T19, T20, T22, T38, shanoic11_in_gggga(T31, T20, T18, T20, T148))
U13_GGGGA(T31, T18, T19, T20, T22, T38, shanoic11_out_gggga(T31, T20, T18, T20, T148)) → U14_GGGGA(T31, T18, T19, T20, T22, append40_in_gga(T38, .(mv(T18, T20), []), X28))
U13_GGGGA(T31, T18, T19, T20, T22, T38, shanoic11_out_gggga(T31, T20, T18, T20, T148)) → APPEND40_IN_GGA(T38, .(mv(T18, T20), []), X28)
APPEND40_IN_GGA(.(T179, T180), T181, .(T179, T183)) → U9_GGA(T179, T180, T181, T183, append40_in_gga(T180, T181, T183))
APPEND40_IN_GGA(.(T179, T180), T181, .(T179, T183)) → APPEND40_IN_GGA(T180, T181, T183)
U13_GGGGA(T31, T18, T19, T20, T22, T38, shanoic11_out_gggga(T31, T20, T18, T20, T148)) → U15_GGGGA(T31, T18, T19, T20, T22, T148, appendc40_in_gga(T38, .(mv(T18, T20), []), T159))
U15_GGGGA(T31, T18, T19, T20, T22, T148, appendc40_out_gga(T38, .(mv(T18, T20), []), T159)) → U16_GGGGA(T31, T18, T19, T20, T22, append40_in_gga(T159, T148, T22))
U15_GGGGA(T31, T18, T19, T20, T22, T148, appendc40_out_gga(T38, .(mv(T18, T20), []), T159)) → APPEND40_IN_GGA(T159, T148, T22)
The TRS R consists of the following rules:
shanoic11_in_gggga(0, T57, T58, T59, .(mv(T57, T59), [])) → shanoic11_out_gggga(0, T57, T58, T59, .(mv(T57, T59), []))
shanoic11_in_gggga(s(T88), T69, T70, T71, X101) → U18_gggga(T88, T69, T70, T71, X101, shanoic11_in_gggga(T88, T69, T71, T70, T95))
U18_gggga(T88, T69, T70, T71, X101, shanoic11_out_gggga(T88, T69, T71, T70, T95)) → U19_gggga(T88, T69, T70, T71, X101, T95, shanoic11_in_gggga(T88, T70, T69, T71, T108))
U19_gggga(T88, T69, T70, T71, X101, T95, shanoic11_out_gggga(T88, T70, T69, T71, T108)) → U20_gggga(T88, T69, T70, T71, X101, T108, appendc28_in_gga(T95, .(mv(T69, T71), []), T119))
appendc28_in_gga([], T130, T130) → appendc28_out_gga([], T130, T130)
appendc28_in_gga(.(T137, T138), T139, .(T137, X178)) → U22_gga(T137, T138, T139, X178, appendc28_in_gga(T138, T139, X178))
U22_gga(T137, T138, T139, X178, appendc28_out_gga(T138, T139, X178)) → appendc28_out_gga(.(T137, T138), T139, .(T137, X178))
U20_gggga(T88, T69, T70, T71, X101, T108, appendc28_out_gga(T95, .(mv(T69, T71), []), T119)) → U21_gggga(T88, T69, T70, T71, X101, appendc28_in_gga(T119, T108, X101))
U21_gggga(T88, T69, T70, T71, X101, appendc28_out_gga(T119, T108, X101)) → shanoic11_out_gggga(s(T88), T69, T70, T71, X101)
appendc40_in_gga([], T170, T170) → appendc40_out_gga([], T170, T170)
appendc40_in_gga(.(T179, T180), T181, .(T179, T183)) → U23_gga(T179, T180, T181, T183, appendc40_in_gga(T180, T181, T183))
U23_gga(T179, T180, T181, T183, appendc40_out_gga(T180, T181, T183)) → appendc40_out_gga(.(T179, T180), T181, .(T179, T183))
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
shanoi11_in_gggga(x1, x2, x3, x4, x5) = shanoi11_in_gggga(x1, x2, x3, x4)
shanoic11_in_gggga(x1, x2, x3, x4, x5) = shanoic11_in_gggga(x1, x2, x3, x4)
0 = 0
shanoic11_out_gggga(x1, x2, x3, x4, x5) = shanoic11_out_gggga(x1, x2, x3, x4, x5)
U18_gggga(x1, x2, x3, x4, x5, x6) = U18_gggga(x1, x2, x3, x4, x6)
U19_gggga(x1, x2, x3, x4, x5, x6, x7) = U19_gggga(x1, x2, x3, x4, x6, x7)
U20_gggga(x1, x2, x3, x4, x5, x6, x7) = U20_gggga(x1, x2, x3, x4, x6, x7)
appendc28_in_gga(x1, x2, x3) = appendc28_in_gga(x1, x2)
[] = []
appendc28_out_gga(x1, x2, x3) = appendc28_out_gga(x1, x2, x3)
.(x1, x2) = .(x1, x2)
U22_gga(x1, x2, x3, x4, x5) = U22_gga(x1, x2, x3, x5)
mv(x1, x2) = mv(x1, x2)
U21_gggga(x1, x2, x3, x4, x5, x6) = U21_gggga(x1, x2, x3, x4, x6)
append28_in_gga(x1, x2, x3) = append28_in_gga(x1, x2)
append40_in_gga(x1, x2, x3) = append40_in_gga(x1, x2)
appendc40_in_gga(x1, x2, x3) = appendc40_in_gga(x1, x2)
appendc40_out_gga(x1, x2, x3) = appendc40_out_gga(x1, x2, x3)
U23_gga(x1, x2, x3, x4, x5) = U23_gga(x1, x2, x3, x5)
SHANOI1_IN_GGGGA(x1, x2, x3, x4, x5) = SHANOI1_IN_GGGGA(x1, x2, x3, x4)
U10_GGGGA(x1, x2, x3, x4, x5, x6) = U10_GGGGA(x1, x2, x3, x4, x6)
SHANOI11_IN_GGGGA(x1, x2, x3, x4, x5) = SHANOI11_IN_GGGGA(x1, x2, x3, x4)
U1_GGGGA(x1, x2, x3, x4, x5, x6) = U1_GGGGA(x1, x2, x3, x4, x6)
U2_GGGGA(x1, x2, x3, x4, x5, x6) = U2_GGGGA(x1, x2, x3, x4, x6)
U3_GGGGA(x1, x2, x3, x4, x5, x6) = U3_GGGGA(x1, x2, x3, x4, x6)
U4_GGGGA(x1, x2, x3, x4, x5, x6, x7) = U4_GGGGA(x1, x2, x3, x4, x6, x7)
U5_GGGGA(x1, x2, x3, x4, x5, x6) = U5_GGGGA(x1, x2, x3, x4, x6)
APPEND28_IN_GGA(x1, x2, x3) = APPEND28_IN_GGA(x1, x2)
U8_GGA(x1, x2, x3, x4, x5) = U8_GGA(x1, x2, x3, x5)
U6_GGGGA(x1, x2, x3, x4, x5, x6, x7) = U6_GGGGA(x1, x2, x3, x4, x6, x7)
U7_GGGGA(x1, x2, x3, x4, x5, x6) = U7_GGGGA(x1, x2, x3, x4, x6)
U11_GGGGA(x1, x2, x3, x4, x5, x6) = U11_GGGGA(x1, x2, x3, x4, x6)
U12_GGGGA(x1, x2, x3, x4, x5, x6) = U12_GGGGA(x1, x2, x3, x4, x6)
U13_GGGGA(x1, x2, x3, x4, x5, x6, x7) = U13_GGGGA(x1, x2, x3, x4, x6, x7)
U14_GGGGA(x1, x2, x3, x4, x5, x6) = U14_GGGGA(x1, x2, x3, x4, x6)
APPEND40_IN_GGA(x1, x2, x3) = APPEND40_IN_GGA(x1, x2)
U9_GGA(x1, x2, x3, x4, x5) = U9_GGA(x1, x2, x3, x5)
U15_GGGGA(x1, x2, x3, x4, x5, x6, x7) = U15_GGGGA(x1, x2, x3, x4, x6, x7)
U16_GGGGA(x1, x2, x3, x4, x5, x6) = U16_GGGGA(x1, x2, x3, x4, x6)
We have to consider all (P,R,Pi)-chains
(5) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 21 less nodes.(6) Complex Obligation (AND)
(7) Obligation:
Pi DP problem:The TRS P consists of the following rules:
APPEND40_IN_GGA(.(T179, T180), T181, .(T179, T183)) → APPEND40_IN_GGA(T180, T181, T183)
The TRS R consists of the following rules:
shanoic11_in_gggga(0, T57, T58, T59, .(mv(T57, T59), [])) → shanoic11_out_gggga(0, T57, T58, T59, .(mv(T57, T59), []))
shanoic11_in_gggga(s(T88), T69, T70, T71, X101) → U18_gggga(T88, T69, T70, T71, X101, shanoic11_in_gggga(T88, T69, T71, T70, T95))
U18_gggga(T88, T69, T70, T71, X101, shanoic11_out_gggga(T88, T69, T71, T70, T95)) → U19_gggga(T88, T69, T70, T71, X101, T95, shanoic11_in_gggga(T88, T70, T69, T71, T108))
U19_gggga(T88, T69, T70, T71, X101, T95, shanoic11_out_gggga(T88, T70, T69, T71, T108)) → U20_gggga(T88, T69, T70, T71, X101, T108, appendc28_in_gga(T95, .(mv(T69, T71), []), T119))
appendc28_in_gga([], T130, T130) → appendc28_out_gga([], T130, T130)
appendc28_in_gga(.(T137, T138), T139, .(T137, X178)) → U22_gga(T137, T138, T139, X178, appendc28_in_gga(T138, T139, X178))
U22_gga(T137, T138, T139, X178, appendc28_out_gga(T138, T139, X178)) → appendc28_out_gga(.(T137, T138), T139, .(T137, X178))
U20_gggga(T88, T69, T70, T71, X101, T108, appendc28_out_gga(T95, .(mv(T69, T71), []), T119)) → U21_gggga(T88, T69, T70, T71, X101, appendc28_in_gga(T119, T108, X101))
U21_gggga(T88, T69, T70, T71, X101, appendc28_out_gga(T119, T108, X101)) → shanoic11_out_gggga(s(T88), T69, T70, T71, X101)
appendc40_in_gga([], T170, T170) → appendc40_out_gga([], T170, T170)
appendc40_in_gga(.(T179, T180), T181, .(T179, T183)) → U23_gga(T179, T180, T181, T183, appendc40_in_gga(T180, T181, T183))
U23_gga(T179, T180, T181, T183, appendc40_out_gga(T180, T181, T183)) → appendc40_out_gga(.(T179, T180), T181, .(T179, T183))
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
shanoic11_in_gggga(x1, x2, x3, x4, x5) = shanoic11_in_gggga(x1, x2, x3, x4)
0 = 0
shanoic11_out_gggga(x1, x2, x3, x4, x5) = shanoic11_out_gggga(x1, x2, x3, x4, x5)
U18_gggga(x1, x2, x3, x4, x5, x6) = U18_gggga(x1, x2, x3, x4, x6)
U19_gggga(x1, x2, x3, x4, x5, x6, x7) = U19_gggga(x1, x2, x3, x4, x6, x7)
U20_gggga(x1, x2, x3, x4, x5, x6, x7) = U20_gggga(x1, x2, x3, x4, x6, x7)
appendc28_in_gga(x1, x2, x3) = appendc28_in_gga(x1, x2)
[] = []
appendc28_out_gga(x1, x2, x3) = appendc28_out_gga(x1, x2, x3)
.(x1, x2) = .(x1, x2)
U22_gga(x1, x2, x3, x4, x5) = U22_gga(x1, x2, x3, x5)
mv(x1, x2) = mv(x1, x2)
U21_gggga(x1, x2, x3, x4, x5, x6) = U21_gggga(x1, x2, x3, x4, x6)
appendc40_in_gga(x1, x2, x3) = appendc40_in_gga(x1, x2)
appendc40_out_gga(x1, x2, x3) = appendc40_out_gga(x1, x2, x3)
U23_gga(x1, x2, x3, x4, x5) = U23_gga(x1, x2, x3, x5)
APPEND40_IN_GGA(x1, x2, x3) = APPEND40_IN_GGA(x1, x2)
We have to consider all (P,R,Pi)-chains
(8) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.(9) Obligation:
Pi DP problem:The TRS P consists of the following rules:
APPEND40_IN_GGA(.(T179, T180), T181, .(T179, T183)) → APPEND40_IN_GGA(T180, T181, T183)
R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
APPEND40_IN_GGA(x1, x2, x3) = APPEND40_IN_GGA(x1, x2)
We have to consider all (P,R,Pi)-chains
(10) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.(11) Obligation:
Q DP problem:The TRS P consists of the following rules:
APPEND40_IN_GGA(.(T179, T180), T181) → APPEND40_IN_GGA(T180, T181)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(12) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.From the DPs we obtained the following set of size-change graphs:
- APPEND40_IN_GGA(.(T179, T180), T181) → APPEND40_IN_GGA(T180, T181)
The graph contains the following edges 1 > 1, 2 >= 2
(13) YES
(14) Obligation:
Pi DP problem:The TRS P consists of the following rules:
APPEND28_IN_GGA(.(T137, T138), T139, .(T137, X178)) → APPEND28_IN_GGA(T138, T139, X178)
The TRS R consists of the following rules:
shanoic11_in_gggga(0, T57, T58, T59, .(mv(T57, T59), [])) → shanoic11_out_gggga(0, T57, T58, T59, .(mv(T57, T59), []))
shanoic11_in_gggga(s(T88), T69, T70, T71, X101) → U18_gggga(T88, T69, T70, T71, X101, shanoic11_in_gggga(T88, T69, T71, T70, T95))
U18_gggga(T88, T69, T70, T71, X101, shanoic11_out_gggga(T88, T69, T71, T70, T95)) → U19_gggga(T88, T69, T70, T71, X101, T95, shanoic11_in_gggga(T88, T70, T69, T71, T108))
U19_gggga(T88, T69, T70, T71, X101, T95, shanoic11_out_gggga(T88, T70, T69, T71, T108)) → U20_gggga(T88, T69, T70, T71, X101, T108, appendc28_in_gga(T95, .(mv(T69, T71), []), T119))
appendc28_in_gga([], T130, T130) → appendc28_out_gga([], T130, T130)
appendc28_in_gga(.(T137, T138), T139, .(T137, X178)) → U22_gga(T137, T138, T139, X178, appendc28_in_gga(T138, T139, X178))
U22_gga(T137, T138, T139, X178, appendc28_out_gga(T138, T139, X178)) → appendc28_out_gga(.(T137, T138), T139, .(T137, X178))
U20_gggga(T88, T69, T70, T71, X101, T108, appendc28_out_gga(T95, .(mv(T69, T71), []), T119)) → U21_gggga(T88, T69, T70, T71, X101, appendc28_in_gga(T119, T108, X101))
U21_gggga(T88, T69, T70, T71, X101, appendc28_out_gga(T119, T108, X101)) → shanoic11_out_gggga(s(T88), T69, T70, T71, X101)
appendc40_in_gga([], T170, T170) → appendc40_out_gga([], T170, T170)
appendc40_in_gga(.(T179, T180), T181, .(T179, T183)) → U23_gga(T179, T180, T181, T183, appendc40_in_gga(T180, T181, T183))
U23_gga(T179, T180, T181, T183, appendc40_out_gga(T180, T181, T183)) → appendc40_out_gga(.(T179, T180), T181, .(T179, T183))
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
shanoic11_in_gggga(x1, x2, x3, x4, x5) = shanoic11_in_gggga(x1, x2, x3, x4)
0 = 0
shanoic11_out_gggga(x1, x2, x3, x4, x5) = shanoic11_out_gggga(x1, x2, x3, x4, x5)
U18_gggga(x1, x2, x3, x4, x5, x6) = U18_gggga(x1, x2, x3, x4, x6)
U19_gggga(x1, x2, x3, x4, x5, x6, x7) = U19_gggga(x1, x2, x3, x4, x6, x7)
U20_gggga(x1, x2, x3, x4, x5, x6, x7) = U20_gggga(x1, x2, x3, x4, x6, x7)
appendc28_in_gga(x1, x2, x3) = appendc28_in_gga(x1, x2)
[] = []
appendc28_out_gga(x1, x2, x3) = appendc28_out_gga(x1, x2, x3)
.(x1, x2) = .(x1, x2)
U22_gga(x1, x2, x3, x4, x5) = U22_gga(x1, x2, x3, x5)
mv(x1, x2) = mv(x1, x2)
U21_gggga(x1, x2, x3, x4, x5, x6) = U21_gggga(x1, x2, x3, x4, x6)
appendc40_in_gga(x1, x2, x3) = appendc40_in_gga(x1, x2)
appendc40_out_gga(x1, x2, x3) = appendc40_out_gga(x1, x2, x3)
U23_gga(x1, x2, x3, x4, x5) = U23_gga(x1, x2, x3, x5)
APPEND28_IN_GGA(x1, x2, x3) = APPEND28_IN_GGA(x1, x2)
We have to consider all (P,R,Pi)-chains
(15) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.(16) Obligation:
Pi DP problem:The TRS P consists of the following rules:
APPEND28_IN_GGA(.(T137, T138), T139, .(T137, X178)) → APPEND28_IN_GGA(T138, T139, X178)
R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
APPEND28_IN_GGA(x1, x2, x3) = APPEND28_IN_GGA(x1, x2)
We have to consider all (P,R,Pi)-chains
(17) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.(18) Obligation:
Q DP problem:The TRS P consists of the following rules:
APPEND28_IN_GGA(.(T137, T138), T139) → APPEND28_IN_GGA(T138, T139)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(19) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.From the DPs we obtained the following set of size-change graphs:
- APPEND28_IN_GGA(.(T137, T138), T139) → APPEND28_IN_GGA(T138, T139)
The graph contains the following edges 1 > 1, 2 >= 2
(20) YES
(21) Obligation:
Pi DP problem:The TRS P consists of the following rules:
SHANOI11_IN_GGGGA(s(T88), T69, T70, T71, X101) → U2_GGGGA(T88, T69, T70, T71, X101, shanoic11_in_gggga(T88, T69, T71, T70, T95))
U2_GGGGA(T88, T69, T70, T71, X101, shanoic11_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)
The TRS R consists of the following rules:
shanoic11_in_gggga(0, T57, T58, T59, .(mv(T57, T59), [])) → shanoic11_out_gggga(0, T57, T58, T59, .(mv(T57, T59), []))
shanoic11_in_gggga(s(T88), T69, T70, T71, X101) → U18_gggga(T88, T69, T70, T71, X101, shanoic11_in_gggga(T88, T69, T71, T70, T95))
U18_gggga(T88, T69, T70, T71, X101, shanoic11_out_gggga(T88, T69, T71, T70, T95)) → U19_gggga(T88, T69, T70, T71, X101, T95, shanoic11_in_gggga(T88, T70, T69, T71, T108))
U19_gggga(T88, T69, T70, T71, X101, T95, shanoic11_out_gggga(T88, T70, T69, T71, T108)) → U20_gggga(T88, T69, T70, T71, X101, T108, appendc28_in_gga(T95, .(mv(T69, T71), []), T119))
appendc28_in_gga([], T130, T130) → appendc28_out_gga([], T130, T130)
appendc28_in_gga(.(T137, T138), T139, .(T137, X178)) → U22_gga(T137, T138, T139, X178, appendc28_in_gga(T138, T139, X178))
U22_gga(T137, T138, T139, X178, appendc28_out_gga(T138, T139, X178)) → appendc28_out_gga(.(T137, T138), T139, .(T137, X178))
U20_gggga(T88, T69, T70, T71, X101, T108, appendc28_out_gga(T95, .(mv(T69, T71), []), T119)) → U21_gggga(T88, T69, T70, T71, X101, appendc28_in_gga(T119, T108, X101))
U21_gggga(T88, T69, T70, T71, X101, appendc28_out_gga(T119, T108, X101)) → shanoic11_out_gggga(s(T88), T69, T70, T71, X101)
appendc40_in_gga([], T170, T170) → appendc40_out_gga([], T170, T170)
appendc40_in_gga(.(T179, T180), T181, .(T179, T183)) → U23_gga(T179, T180, T181, T183, appendc40_in_gga(T180, T181, T183))
U23_gga(T179, T180, T181, T183, appendc40_out_gga(T180, T181, T183)) → appendc40_out_gga(.(T179, T180), T181, .(T179, T183))
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
shanoic11_in_gggga(x1, x2, x3, x4, x5) = shanoic11_in_gggga(x1, x2, x3, x4)
0 = 0
shanoic11_out_gggga(x1, x2, x3, x4, x5) = shanoic11_out_gggga(x1, x2, x3, x4, x5)
U18_gggga(x1, x2, x3, x4, x5, x6) = U18_gggga(x1, x2, x3, x4, x6)
U19_gggga(x1, x2, x3, x4, x5, x6, x7) = U19_gggga(x1, x2, x3, x4, x6, x7)
U20_gggga(x1, x2, x3, x4, x5, x6, x7) = U20_gggga(x1, x2, x3, x4, x6, x7)
appendc28_in_gga(x1, x2, x3) = appendc28_in_gga(x1, x2)
[] = []
appendc28_out_gga(x1, x2, x3) = appendc28_out_gga(x1, x2, x3)
.(x1, x2) = .(x1, x2)
U22_gga(x1, x2, x3, x4, x5) = U22_gga(x1, x2, x3, x5)
mv(x1, x2) = mv(x1, x2)
U21_gggga(x1, x2, x3, x4, x5, x6) = U21_gggga(x1, x2, x3, x4, x6)
appendc40_in_gga(x1, x2, x3) = appendc40_in_gga(x1, x2)
appendc40_out_gga(x1, x2, x3) = appendc40_out_gga(x1, x2, x3)
U23_gga(x1, x2, x3, x4, x5) = U23_gga(x1, x2, x3, x5)
SHANOI11_IN_GGGGA(x1, x2, x3, x4, x5) = SHANOI11_IN_GGGGA(x1, x2, x3, x4)
U2_GGGGA(x1, x2, x3, x4, x5, x6) = U2_GGGGA(x1, x2, x3, x4, x6)
We have to consider all (P,R,Pi)-chains
(22) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.(23) Obligation:
Pi DP problem:The TRS P consists of the following rules:
SHANOI11_IN_GGGGA(s(T88), T69, T70, T71, X101) → U2_GGGGA(T88, T69, T70, T71, X101, shanoic11_in_gggga(T88, T69, T71, T70, T95))
U2_GGGGA(T88, T69, T70, T71, X101, shanoic11_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)
The TRS R consists of the following rules:
shanoic11_in_gggga(0, T57, T58, T59, .(mv(T57, T59), [])) → shanoic11_out_gggga(0, T57, T58, T59, .(mv(T57, T59), []))
shanoic11_in_gggga(s(T88), T69, T70, T71, X101) → U18_gggga(T88, T69, T70, T71, X101, shanoic11_in_gggga(T88, T69, T71, T70, T95))
U18_gggga(T88, T69, T70, T71, X101, shanoic11_out_gggga(T88, T69, T71, T70, T95)) → U19_gggga(T88, T69, T70, T71, X101, T95, shanoic11_in_gggga(T88, T70, T69, T71, T108))
U19_gggga(T88, T69, T70, T71, X101, T95, shanoic11_out_gggga(T88, T70, T69, T71, T108)) → U20_gggga(T88, T69, T70, T71, X101, T108, appendc28_in_gga(T95, .(mv(T69, T71), []), T119))
U20_gggga(T88, T69, T70, T71, X101, T108, appendc28_out_gga(T95, .(mv(T69, T71), []), T119)) → U21_gggga(T88, T69, T70, T71, X101, appendc28_in_gga(T119, T108, X101))
appendc28_in_gga([], T130, T130) → appendc28_out_gga([], T130, T130)
appendc28_in_gga(.(T137, T138), T139, .(T137, X178)) → U22_gga(T137, T138, T139, X178, appendc28_in_gga(T138, T139, X178))
U21_gggga(T88, T69, T70, T71, X101, appendc28_out_gga(T119, T108, X101)) → shanoic11_out_gggga(s(T88), T69, T70, T71, X101)
U22_gga(T137, T138, T139, X178, appendc28_out_gga(T138, T139, X178)) → appendc28_out_gga(.(T137, T138), T139, .(T137, X178))
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
shanoic11_in_gggga(x1, x2, x3, x4, x5) = shanoic11_in_gggga(x1, x2, x3, x4)
0 = 0
shanoic11_out_gggga(x1, x2, x3, x4, x5) = shanoic11_out_gggga(x1, x2, x3, x4, x5)
U18_gggga(x1, x2, x3, x4, x5, x6) = U18_gggga(x1, x2, x3, x4, x6)
U19_gggga(x1, x2, x3, x4, x5, x6, x7) = U19_gggga(x1, x2, x3, x4, x6, x7)
U20_gggga(x1, x2, x3, x4, x5, x6, x7) = U20_gggga(x1, x2, x3, x4, x6, x7)
appendc28_in_gga(x1, x2, x3) = appendc28_in_gga(x1, x2)
[] = []
appendc28_out_gga(x1, x2, x3) = appendc28_out_gga(x1, x2, x3)
.(x1, x2) = .(x1, x2)
U22_gga(x1, x2, x3, x4, x5) = U22_gga(x1, x2, x3, x5)
mv(x1, x2) = mv(x1, x2)
U21_gggga(x1, x2, x3, x4, x5, x6) = U21_gggga(x1, x2, x3, x4, x6)
SHANOI11_IN_GGGGA(x1, x2, x3, x4, x5) = SHANOI11_IN_GGGGA(x1, x2, x3, x4)
U2_GGGGA(x1, x2, x3, x4, x5, x6) = U2_GGGGA(x1, x2, x3, x4, x6)
We have to consider all (P,R,Pi)-chains
(24) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.(25) Obligation:
Q DP problem:The TRS P consists of the following rules:
SHANOI11_IN_GGGGA(s(T88), T69, T70, T71) → U2_GGGGA(T88, T69, T70, T71, shanoic11_in_gggga(T88, T69, T71, T70))
U2_GGGGA(T88, T69, T70, T71, shanoic11_out_gggga(T88, T69, T71, T70, T95)) → SHANOI11_IN_GGGGA(T88, T70, T69, T71)
SHANOI11_IN_GGGGA(s(T88), T69, T70, T71) → SHANOI11_IN_GGGGA(T88, T69, T71, T70)
The TRS R consists of the following rules:
shanoic11_in_gggga(0, T57, T58, T59) → shanoic11_out_gggga(0, T57, T58, T59, .(mv(T57, T59), []))
shanoic11_in_gggga(s(T88), T69, T70, T71) → U18_gggga(T88, T69, T70, T71, shanoic11_in_gggga(T88, T69, T71, T70))
U18_gggga(T88, T69, T70, T71, shanoic11_out_gggga(T88, T69, T71, T70, T95)) → U19_gggga(T88, T69, T70, T71, T95, shanoic11_in_gggga(T88, T70, T69, T71))
U19_gggga(T88, T69, T70, T71, T95, shanoic11_out_gggga(T88, T70, T69, T71, T108)) → U20_gggga(T88, T69, T70, T71, T108, appendc28_in_gga(T95, .(mv(T69, T71), [])))
U20_gggga(T88, T69, T70, T71, T108, appendc28_out_gga(T95, .(mv(T69, T71), []), T119)) → U21_gggga(T88, T69, T70, T71, appendc28_in_gga(T119, T108))
appendc28_in_gga([], T130) → appendc28_out_gga([], T130, T130)
appendc28_in_gga(.(T137, T138), T139) → U22_gga(T137, T138, T139, appendc28_in_gga(T138, T139))
U21_gggga(T88, T69, T70, T71, appendc28_out_gga(T119, T108, X101)) → shanoic11_out_gggga(s(T88), T69, T70, T71, X101)
U22_gga(T137, T138, T139, appendc28_out_gga(T138, T139, X178)) → appendc28_out_gga(.(T137, T138), T139, .(T137, X178))
The set Q consists of the following terms:
shanoic11_in_gggga(x0, x1, x2, x3)
U18_gggga(x0, x1, x2, x3, x4)
U19_gggga(x0, x1, x2, x3, x4, x5)
U20_gggga(x0, x1, x2, x3, x4, x5)
appendc28_in_gga(x0, x1)
U21_gggga(x0, x1, x2, x3, x4)
U22_gga(x0, x1, x2, x3)
We have to consider all (P,Q,R)-chains.
(26) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.From the DPs we obtained the following set of size-change graphs:
- U2_GGGGA(T88, T69, T70, T71, shanoic11_out_gggga(T88, T69, T71, T70, T95)) → SHANOI11_IN_GGGGA(T88, T70, T69, T71)
The graph contains the following edges 1 >= 1, 5 > 1, 3 >= 2, 5 > 2, 2 >= 3, 5 > 3, 4 >= 4, 5 > 4 - SHANOI11_IN_GGGGA(s(T88), T69, T70, T71) → SHANOI11_IN_GGGGA(T88, T69, T71, T70)
The graph contains the following edges 1 > 1, 2 >= 2, 4 >= 3, 3 >= 4 - SHANOI11_IN_GGGGA(s(T88), T69, T70, T71) → U2_GGGGA(T88, T69, T70, T71, shanoic11_in_gggga(T88, T69, T71, T70))
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3, 4 >= 4