(0) Obligation:

Clauses:

ss(Xs, Ys) :- ','(perm(Xs, Ys), ordered(Ys)).
perm([], []).
perm(Xs, .(X, Ys)) :- ','(app(X1s, .(X, X2s), Xs), ','(app(X1s, X2s, Zs), perm(Zs, Ys))).
app([], X, X).
app(.(X, Xs), Ys, .(X, Zs)) :- app(Xs, Ys, Zs).
ordered([]).
ordered(.(X1, [])).
ordered(.(X, .(Y, Xs))) :- ','(less(X, s(Y)), ordered(.(Y, Xs))).
less(0, s(X2)).
less(s(X), s(Y)) :- less(X, Y).

Queries:

ss(g,g).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

app18(.(X66, X67), T31, X68, .(X66, T32)) :- app18(X67, T31, X68, T32).
app28(.(T51, T52), T53, .(T51, X101)) :- app28(T52, T53, X101).
perm38(T62, .(T63, T64)) :- app18(X120, T63, X121, T62).
perm38(T62, .(T63, T64)) :- ','(appc18(T67, T63, T68, T62), app28(T67, T68, X122)).
perm38(T62, .(T63, T64)) :- ','(appc18(T67, T63, T68, T62), ','(appc28(T67, T68, T73), perm38(T73, T64))).
ordered39(s(T105), .(T106, T91)) :- less69(T105, T106).
ordered39(T89, .(T90, T91)) :- ','(lessc61(T89, T90), ordered39(T90, T91)).
less69(s(T118), s(T119)) :- less69(T118, T119).
ss1(T13, .(T14, T15)) :- app18(X23, T14, X24, T13).
ss1(T13, .(T14, T15)) :- ','(appc18(T18, T14, T19, T13), app28(T18, T19, X25)).
ss1(T13, .(T14, T15)) :- ','(appc18(T18, T14, T19, T13), ','(appc28(T18, T19, T37), perm38(T37, T15))).
ss1(T13, .(T14, T15)) :- ','(appc18(T18, T14, T19, T13), ','(appc28(T18, T19, T37), ','(permc38(T37, T15), ordered39(T14, T15)))).

Clauses:

appc18([], T26, X46, .(T26, X46)).
appc18(.(X66, X67), T31, X68, .(X66, T32)) :- appc18(X67, T31, X68, T32).
appc28([], T44, T44).
appc28(.(T51, T52), T53, .(T51, X101)) :- appc28(T52, T53, X101).
permc38([], []).
permc38(T62, .(T63, T64)) :- ','(appc18(T67, T63, T68, T62), ','(appc28(T67, T68, T73), permc38(T73, T64))).
orderedc39(T82, []).
orderedc39(T89, .(T90, T91)) :- ','(lessc61(T89, T90), orderedc39(T90, T91)).
lessc69(0, s(T113)).
lessc69(s(T118), s(T119)) :- lessc69(T118, T119).
lessc61(0, T100).
lessc61(s(T105), T106) :- lessc69(T105, T106).

Afs:

ss1(x1, x2)  =  ss1(x1, x2)

(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:
ss1_in: (b,b)
app18_in: (f,b,f,b)
appc18_in: (f,b,f,b)
app28_in: (b,b,f)
appc28_in: (b,b,f)
perm38_in: (b,b)
permc38_in: (b,b)
ordered39_in: (b,b)
less69_in: (b,b)
lessc61_in: (b,b)
lessc69_in: (b,b)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

SS1_IN_GG(T13, .(T14, T15)) → U12_GG(T13, T14, T15, app18_in_agag(X23, T14, X24, T13))
SS1_IN_GG(T13, .(T14, T15)) → APP18_IN_AGAG(X23, T14, X24, T13)
APP18_IN_AGAG(.(X66, X67), T31, X68, .(X66, T32)) → U1_AGAG(X66, X67, T31, X68, T32, app18_in_agag(X67, T31, X68, T32))
APP18_IN_AGAG(.(X66, X67), T31, X68, .(X66, T32)) → APP18_IN_AGAG(X67, T31, X68, T32)
SS1_IN_GG(T13, .(T14, T15)) → U13_GG(T13, T14, T15, appc18_in_agag(T18, T14, T19, T13))
U13_GG(T13, T14, T15, appc18_out_agag(T18, T14, T19, T13)) → U14_GG(T13, T14, T15, app28_in_gga(T18, T19, X25))
U13_GG(T13, T14, T15, appc18_out_agag(T18, T14, T19, T13)) → APP28_IN_GGA(T18, T19, X25)
APP28_IN_GGA(.(T51, T52), T53, .(T51, X101)) → U2_GGA(T51, T52, T53, X101, app28_in_gga(T52, T53, X101))
APP28_IN_GGA(.(T51, T52), T53, .(T51, X101)) → APP28_IN_GGA(T52, T53, X101)
U13_GG(T13, T14, T15, appc18_out_agag(T18, T14, T19, T13)) → U15_GG(T13, T14, T15, appc28_in_gga(T18, T19, T37))
U15_GG(T13, T14, T15, appc28_out_gga(T18, T19, T37)) → U16_GG(T13, T14, T15, perm38_in_gg(T37, T15))
U15_GG(T13, T14, T15, appc28_out_gga(T18, T19, T37)) → PERM38_IN_GG(T37, T15)
PERM38_IN_GG(T62, .(T63, T64)) → U3_GG(T62, T63, T64, app18_in_agag(X120, T63, X121, T62))
PERM38_IN_GG(T62, .(T63, T64)) → APP18_IN_AGAG(X120, T63, X121, T62)
PERM38_IN_GG(T62, .(T63, T64)) → U4_GG(T62, T63, T64, appc18_in_agag(T67, T63, T68, T62))
U4_GG(T62, T63, T64, appc18_out_agag(T67, T63, T68, T62)) → U5_GG(T62, T63, T64, app28_in_gga(T67, T68, X122))
U4_GG(T62, T63, T64, appc18_out_agag(T67, T63, T68, T62)) → APP28_IN_GGA(T67, T68, X122)
U4_GG(T62, T63, T64, appc18_out_agag(T67, T63, T68, T62)) → U6_GG(T62, T63, T64, appc28_in_gga(T67, T68, T73))
U6_GG(T62, T63, T64, appc28_out_gga(T67, T68, T73)) → U7_GG(T62, T63, T64, perm38_in_gg(T73, T64))
U6_GG(T62, T63, T64, appc28_out_gga(T67, T68, T73)) → PERM38_IN_GG(T73, T64)
U15_GG(T13, T14, T15, appc28_out_gga(T18, T19, T37)) → U17_GG(T13, T14, T15, permc38_in_gg(T37, T15))
U17_GG(T13, T14, T15, permc38_out_gg(T37, T15)) → U18_GG(T13, T14, T15, ordered39_in_gg(T14, T15))
U17_GG(T13, T14, T15, permc38_out_gg(T37, T15)) → ORDERED39_IN_GG(T14, T15)
ORDERED39_IN_GG(s(T105), .(T106, T91)) → U8_GG(T105, T106, T91, less69_in_gg(T105, T106))
ORDERED39_IN_GG(s(T105), .(T106, T91)) → LESS69_IN_GG(T105, T106)
LESS69_IN_GG(s(T118), s(T119)) → U11_GG(T118, T119, less69_in_gg(T118, T119))
LESS69_IN_GG(s(T118), s(T119)) → LESS69_IN_GG(T118, T119)
ORDERED39_IN_GG(T89, .(T90, T91)) → U9_GG(T89, T90, T91, lessc61_in_gg(T89, T90))
U9_GG(T89, T90, T91, lessc61_out_gg(T89, T90)) → U10_GG(T89, T90, T91, ordered39_in_gg(T90, T91))
U9_GG(T89, T90, T91, lessc61_out_gg(T89, T90)) → ORDERED39_IN_GG(T90, T91)

The TRS R consists of the following rules:

appc18_in_agag([], T26, X46, .(T26, X46)) → appc18_out_agag([], T26, X46, .(T26, X46))
appc18_in_agag(.(X66, X67), T31, X68, .(X66, T32)) → U20_agag(X66, X67, T31, X68, T32, appc18_in_agag(X67, T31, X68, T32))
U20_agag(X66, X67, T31, X68, T32, appc18_out_agag(X67, T31, X68, T32)) → appc18_out_agag(.(X66, X67), T31, X68, .(X66, T32))
appc28_in_gga([], T44, T44) → appc28_out_gga([], T44, T44)
appc28_in_gga(.(T51, T52), T53, .(T51, X101)) → U21_gga(T51, T52, T53, X101, appc28_in_gga(T52, T53, X101))
U21_gga(T51, T52, T53, X101, appc28_out_gga(T52, T53, X101)) → appc28_out_gga(.(T51, T52), T53, .(T51, X101))
permc38_in_gg([], []) → permc38_out_gg([], [])
permc38_in_gg(T62, .(T63, T64)) → U22_gg(T62, T63, T64, appc18_in_agag(T67, T63, T68, T62))
U22_gg(T62, T63, T64, appc18_out_agag(T67, T63, T68, T62)) → U23_gg(T62, T63, T64, appc28_in_gga(T67, T68, T73))
U23_gg(T62, T63, T64, appc28_out_gga(T67, T68, T73)) → U24_gg(T62, T63, T64, permc38_in_gg(T73, T64))
U24_gg(T62, T63, T64, permc38_out_gg(T73, T64)) → permc38_out_gg(T62, .(T63, T64))
lessc61_in_gg(0, T100) → lessc61_out_gg(0, T100)
lessc61_in_gg(s(T105), T106) → U28_gg(T105, T106, lessc69_in_gg(T105, T106))
lessc69_in_gg(0, s(T113)) → lessc69_out_gg(0, s(T113))
lessc69_in_gg(s(T118), s(T119)) → U27_gg(T118, T119, lessc69_in_gg(T118, T119))
U27_gg(T118, T119, lessc69_out_gg(T118, T119)) → lessc69_out_gg(s(T118), s(T119))
U28_gg(T105, T106, lessc69_out_gg(T105, T106)) → lessc61_out_gg(s(T105), T106)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
app18_in_agag(x1, x2, x3, x4)  =  app18_in_agag(x2, x4)
appc18_in_agag(x1, x2, x3, x4)  =  appc18_in_agag(x2, x4)
appc18_out_agag(x1, x2, x3, x4)  =  appc18_out_agag(x1, x2, x3, x4)
U20_agag(x1, x2, x3, x4, x5, x6)  =  U20_agag(x1, x3, x5, x6)
app28_in_gga(x1, x2, x3)  =  app28_in_gga(x1, x2)
appc28_in_gga(x1, x2, x3)  =  appc28_in_gga(x1, x2)
[]  =  []
appc28_out_gga(x1, x2, x3)  =  appc28_out_gga(x1, x2, x3)
U21_gga(x1, x2, x3, x4, x5)  =  U21_gga(x1, x2, x3, x5)
perm38_in_gg(x1, x2)  =  perm38_in_gg(x1, x2)
permc38_in_gg(x1, x2)  =  permc38_in_gg(x1, x2)
permc38_out_gg(x1, x2)  =  permc38_out_gg(x1, x2)
U22_gg(x1, x2, x3, x4)  =  U22_gg(x1, x2, x3, x4)
U23_gg(x1, x2, x3, x4)  =  U23_gg(x1, x2, x3, x4)
U24_gg(x1, x2, x3, x4)  =  U24_gg(x1, x2, x3, x4)
ordered39_in_gg(x1, x2)  =  ordered39_in_gg(x1, x2)
s(x1)  =  s(x1)
less69_in_gg(x1, x2)  =  less69_in_gg(x1, x2)
lessc61_in_gg(x1, x2)  =  lessc61_in_gg(x1, x2)
0  =  0
lessc61_out_gg(x1, x2)  =  lessc61_out_gg(x1, x2)
U28_gg(x1, x2, x3)  =  U28_gg(x1, x2, x3)
lessc69_in_gg(x1, x2)  =  lessc69_in_gg(x1, x2)
lessc69_out_gg(x1, x2)  =  lessc69_out_gg(x1, x2)
U27_gg(x1, x2, x3)  =  U27_gg(x1, x2, x3)
SS1_IN_GG(x1, x2)  =  SS1_IN_GG(x1, x2)
U12_GG(x1, x2, x3, x4)  =  U12_GG(x1, x2, x3, x4)
APP18_IN_AGAG(x1, x2, x3, x4)  =  APP18_IN_AGAG(x2, x4)
U1_AGAG(x1, x2, x3, x4, x5, x6)  =  U1_AGAG(x1, x3, x5, x6)
U13_GG(x1, x2, x3, x4)  =  U13_GG(x1, x2, x3, x4)
U14_GG(x1, x2, x3, x4)  =  U14_GG(x1, x2, x3, x4)
APP28_IN_GGA(x1, x2, x3)  =  APP28_IN_GGA(x1, x2)
U2_GGA(x1, x2, x3, x4, x5)  =  U2_GGA(x1, x2, x3, x5)
U15_GG(x1, x2, x3, x4)  =  U15_GG(x1, x2, x3, x4)
U16_GG(x1, x2, x3, x4)  =  U16_GG(x1, x2, x3, x4)
PERM38_IN_GG(x1, x2)  =  PERM38_IN_GG(x1, x2)
U3_GG(x1, x2, x3, x4)  =  U3_GG(x1, x2, x3, x4)
U4_GG(x1, x2, x3, x4)  =  U4_GG(x1, x2, x3, x4)
U5_GG(x1, x2, x3, x4)  =  U5_GG(x1, x2, x3, x4)
U6_GG(x1, x2, x3, x4)  =  U6_GG(x1, x2, x3, x4)
U7_GG(x1, x2, x3, x4)  =  U7_GG(x1, x2, x3, x4)
U17_GG(x1, x2, x3, x4)  =  U17_GG(x1, x2, x3, x4)
U18_GG(x1, x2, x3, x4)  =  U18_GG(x1, x2, x3, x4)
ORDERED39_IN_GG(x1, x2)  =  ORDERED39_IN_GG(x1, x2)
U8_GG(x1, x2, x3, x4)  =  U8_GG(x1, x2, x3, x4)
LESS69_IN_GG(x1, x2)  =  LESS69_IN_GG(x1, x2)
U11_GG(x1, x2, x3)  =  U11_GG(x1, x2, x3)
U9_GG(x1, x2, x3, x4)  =  U9_GG(x1, x2, x3, x4)
U10_GG(x1, x2, x3, x4)  =  U10_GG(x1, x2, x3, x4)

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:

SS1_IN_GG(T13, .(T14, T15)) → U12_GG(T13, T14, T15, app18_in_agag(X23, T14, X24, T13))
SS1_IN_GG(T13, .(T14, T15)) → APP18_IN_AGAG(X23, T14, X24, T13)
APP18_IN_AGAG(.(X66, X67), T31, X68, .(X66, T32)) → U1_AGAG(X66, X67, T31, X68, T32, app18_in_agag(X67, T31, X68, T32))
APP18_IN_AGAG(.(X66, X67), T31, X68, .(X66, T32)) → APP18_IN_AGAG(X67, T31, X68, T32)
SS1_IN_GG(T13, .(T14, T15)) → U13_GG(T13, T14, T15, appc18_in_agag(T18, T14, T19, T13))
U13_GG(T13, T14, T15, appc18_out_agag(T18, T14, T19, T13)) → U14_GG(T13, T14, T15, app28_in_gga(T18, T19, X25))
U13_GG(T13, T14, T15, appc18_out_agag(T18, T14, T19, T13)) → APP28_IN_GGA(T18, T19, X25)
APP28_IN_GGA(.(T51, T52), T53, .(T51, X101)) → U2_GGA(T51, T52, T53, X101, app28_in_gga(T52, T53, X101))
APP28_IN_GGA(.(T51, T52), T53, .(T51, X101)) → APP28_IN_GGA(T52, T53, X101)
U13_GG(T13, T14, T15, appc18_out_agag(T18, T14, T19, T13)) → U15_GG(T13, T14, T15, appc28_in_gga(T18, T19, T37))
U15_GG(T13, T14, T15, appc28_out_gga(T18, T19, T37)) → U16_GG(T13, T14, T15, perm38_in_gg(T37, T15))
U15_GG(T13, T14, T15, appc28_out_gga(T18, T19, T37)) → PERM38_IN_GG(T37, T15)
PERM38_IN_GG(T62, .(T63, T64)) → U3_GG(T62, T63, T64, app18_in_agag(X120, T63, X121, T62))
PERM38_IN_GG(T62, .(T63, T64)) → APP18_IN_AGAG(X120, T63, X121, T62)
PERM38_IN_GG(T62, .(T63, T64)) → U4_GG(T62, T63, T64, appc18_in_agag(T67, T63, T68, T62))
U4_GG(T62, T63, T64, appc18_out_agag(T67, T63, T68, T62)) → U5_GG(T62, T63, T64, app28_in_gga(T67, T68, X122))
U4_GG(T62, T63, T64, appc18_out_agag(T67, T63, T68, T62)) → APP28_IN_GGA(T67, T68, X122)
U4_GG(T62, T63, T64, appc18_out_agag(T67, T63, T68, T62)) → U6_GG(T62, T63, T64, appc28_in_gga(T67, T68, T73))
U6_GG(T62, T63, T64, appc28_out_gga(T67, T68, T73)) → U7_GG(T62, T63, T64, perm38_in_gg(T73, T64))
U6_GG(T62, T63, T64, appc28_out_gga(T67, T68, T73)) → PERM38_IN_GG(T73, T64)
U15_GG(T13, T14, T15, appc28_out_gga(T18, T19, T37)) → U17_GG(T13, T14, T15, permc38_in_gg(T37, T15))
U17_GG(T13, T14, T15, permc38_out_gg(T37, T15)) → U18_GG(T13, T14, T15, ordered39_in_gg(T14, T15))
U17_GG(T13, T14, T15, permc38_out_gg(T37, T15)) → ORDERED39_IN_GG(T14, T15)
ORDERED39_IN_GG(s(T105), .(T106, T91)) → U8_GG(T105, T106, T91, less69_in_gg(T105, T106))
ORDERED39_IN_GG(s(T105), .(T106, T91)) → LESS69_IN_GG(T105, T106)
LESS69_IN_GG(s(T118), s(T119)) → U11_GG(T118, T119, less69_in_gg(T118, T119))
LESS69_IN_GG(s(T118), s(T119)) → LESS69_IN_GG(T118, T119)
ORDERED39_IN_GG(T89, .(T90, T91)) → U9_GG(T89, T90, T91, lessc61_in_gg(T89, T90))
U9_GG(T89, T90, T91, lessc61_out_gg(T89, T90)) → U10_GG(T89, T90, T91, ordered39_in_gg(T90, T91))
U9_GG(T89, T90, T91, lessc61_out_gg(T89, T90)) → ORDERED39_IN_GG(T90, T91)

The TRS R consists of the following rules:

appc18_in_agag([], T26, X46, .(T26, X46)) → appc18_out_agag([], T26, X46, .(T26, X46))
appc18_in_agag(.(X66, X67), T31, X68, .(X66, T32)) → U20_agag(X66, X67, T31, X68, T32, appc18_in_agag(X67, T31, X68, T32))
U20_agag(X66, X67, T31, X68, T32, appc18_out_agag(X67, T31, X68, T32)) → appc18_out_agag(.(X66, X67), T31, X68, .(X66, T32))
appc28_in_gga([], T44, T44) → appc28_out_gga([], T44, T44)
appc28_in_gga(.(T51, T52), T53, .(T51, X101)) → U21_gga(T51, T52, T53, X101, appc28_in_gga(T52, T53, X101))
U21_gga(T51, T52, T53, X101, appc28_out_gga(T52, T53, X101)) → appc28_out_gga(.(T51, T52), T53, .(T51, X101))
permc38_in_gg([], []) → permc38_out_gg([], [])
permc38_in_gg(T62, .(T63, T64)) → U22_gg(T62, T63, T64, appc18_in_agag(T67, T63, T68, T62))
U22_gg(T62, T63, T64, appc18_out_agag(T67, T63, T68, T62)) → U23_gg(T62, T63, T64, appc28_in_gga(T67, T68, T73))
U23_gg(T62, T63, T64, appc28_out_gga(T67, T68, T73)) → U24_gg(T62, T63, T64, permc38_in_gg(T73, T64))
U24_gg(T62, T63, T64, permc38_out_gg(T73, T64)) → permc38_out_gg(T62, .(T63, T64))
lessc61_in_gg(0, T100) → lessc61_out_gg(0, T100)
lessc61_in_gg(s(T105), T106) → U28_gg(T105, T106, lessc69_in_gg(T105, T106))
lessc69_in_gg(0, s(T113)) → lessc69_out_gg(0, s(T113))
lessc69_in_gg(s(T118), s(T119)) → U27_gg(T118, T119, lessc69_in_gg(T118, T119))
U27_gg(T118, T119, lessc69_out_gg(T118, T119)) → lessc69_out_gg(s(T118), s(T119))
U28_gg(T105, T106, lessc69_out_gg(T105, T106)) → lessc61_out_gg(s(T105), T106)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
app18_in_agag(x1, x2, x3, x4)  =  app18_in_agag(x2, x4)
appc18_in_agag(x1, x2, x3, x4)  =  appc18_in_agag(x2, x4)
appc18_out_agag(x1, x2, x3, x4)  =  appc18_out_agag(x1, x2, x3, x4)
U20_agag(x1, x2, x3, x4, x5, x6)  =  U20_agag(x1, x3, x5, x6)
app28_in_gga(x1, x2, x3)  =  app28_in_gga(x1, x2)
appc28_in_gga(x1, x2, x3)  =  appc28_in_gga(x1, x2)
[]  =  []
appc28_out_gga(x1, x2, x3)  =  appc28_out_gga(x1, x2, x3)
U21_gga(x1, x2, x3, x4, x5)  =  U21_gga(x1, x2, x3, x5)
perm38_in_gg(x1, x2)  =  perm38_in_gg(x1, x2)
permc38_in_gg(x1, x2)  =  permc38_in_gg(x1, x2)
permc38_out_gg(x1, x2)  =  permc38_out_gg(x1, x2)
U22_gg(x1, x2, x3, x4)  =  U22_gg(x1, x2, x3, x4)
U23_gg(x1, x2, x3, x4)  =  U23_gg(x1, x2, x3, x4)
U24_gg(x1, x2, x3, x4)  =  U24_gg(x1, x2, x3, x4)
ordered39_in_gg(x1, x2)  =  ordered39_in_gg(x1, x2)
s(x1)  =  s(x1)
less69_in_gg(x1, x2)  =  less69_in_gg(x1, x2)
lessc61_in_gg(x1, x2)  =  lessc61_in_gg(x1, x2)
0  =  0
lessc61_out_gg(x1, x2)  =  lessc61_out_gg(x1, x2)
U28_gg(x1, x2, x3)  =  U28_gg(x1, x2, x3)
lessc69_in_gg(x1, x2)  =  lessc69_in_gg(x1, x2)
lessc69_out_gg(x1, x2)  =  lessc69_out_gg(x1, x2)
U27_gg(x1, x2, x3)  =  U27_gg(x1, x2, x3)
SS1_IN_GG(x1, x2)  =  SS1_IN_GG(x1, x2)
U12_GG(x1, x2, x3, x4)  =  U12_GG(x1, x2, x3, x4)
APP18_IN_AGAG(x1, x2, x3, x4)  =  APP18_IN_AGAG(x2, x4)
U1_AGAG(x1, x2, x3, x4, x5, x6)  =  U1_AGAG(x1, x3, x5, x6)
U13_GG(x1, x2, x3, x4)  =  U13_GG(x1, x2, x3, x4)
U14_GG(x1, x2, x3, x4)  =  U14_GG(x1, x2, x3, x4)
APP28_IN_GGA(x1, x2, x3)  =  APP28_IN_GGA(x1, x2)
U2_GGA(x1, x2, x3, x4, x5)  =  U2_GGA(x1, x2, x3, x5)
U15_GG(x1, x2, x3, x4)  =  U15_GG(x1, x2, x3, x4)
U16_GG(x1, x2, x3, x4)  =  U16_GG(x1, x2, x3, x4)
PERM38_IN_GG(x1, x2)  =  PERM38_IN_GG(x1, x2)
U3_GG(x1, x2, x3, x4)  =  U3_GG(x1, x2, x3, x4)
U4_GG(x1, x2, x3, x4)  =  U4_GG(x1, x2, x3, x4)
U5_GG(x1, x2, x3, x4)  =  U5_GG(x1, x2, x3, x4)
U6_GG(x1, x2, x3, x4)  =  U6_GG(x1, x2, x3, x4)
U7_GG(x1, x2, x3, x4)  =  U7_GG(x1, x2, x3, x4)
U17_GG(x1, x2, x3, x4)  =  U17_GG(x1, x2, x3, x4)
U18_GG(x1, x2, x3, x4)  =  U18_GG(x1, x2, x3, x4)
ORDERED39_IN_GG(x1, x2)  =  ORDERED39_IN_GG(x1, x2)
U8_GG(x1, x2, x3, x4)  =  U8_GG(x1, x2, x3, x4)
LESS69_IN_GG(x1, x2)  =  LESS69_IN_GG(x1, x2)
U11_GG(x1, x2, x3)  =  U11_GG(x1, x2, x3)
U9_GG(x1, x2, x3, x4)  =  U9_GG(x1, x2, x3, x4)
U10_GG(x1, x2, x3, x4)  =  U10_GG(x1, x2, x3, x4)

We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 5 SCCs with 22 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESS69_IN_GG(s(T118), s(T119)) → LESS69_IN_GG(T118, T119)

The TRS R consists of the following rules:

appc18_in_agag([], T26, X46, .(T26, X46)) → appc18_out_agag([], T26, X46, .(T26, X46))
appc18_in_agag(.(X66, X67), T31, X68, .(X66, T32)) → U20_agag(X66, X67, T31, X68, T32, appc18_in_agag(X67, T31, X68, T32))
U20_agag(X66, X67, T31, X68, T32, appc18_out_agag(X67, T31, X68, T32)) → appc18_out_agag(.(X66, X67), T31, X68, .(X66, T32))
appc28_in_gga([], T44, T44) → appc28_out_gga([], T44, T44)
appc28_in_gga(.(T51, T52), T53, .(T51, X101)) → U21_gga(T51, T52, T53, X101, appc28_in_gga(T52, T53, X101))
U21_gga(T51, T52, T53, X101, appc28_out_gga(T52, T53, X101)) → appc28_out_gga(.(T51, T52), T53, .(T51, X101))
permc38_in_gg([], []) → permc38_out_gg([], [])
permc38_in_gg(T62, .(T63, T64)) → U22_gg(T62, T63, T64, appc18_in_agag(T67, T63, T68, T62))
U22_gg(T62, T63, T64, appc18_out_agag(T67, T63, T68, T62)) → U23_gg(T62, T63, T64, appc28_in_gga(T67, T68, T73))
U23_gg(T62, T63, T64, appc28_out_gga(T67, T68, T73)) → U24_gg(T62, T63, T64, permc38_in_gg(T73, T64))
U24_gg(T62, T63, T64, permc38_out_gg(T73, T64)) → permc38_out_gg(T62, .(T63, T64))
lessc61_in_gg(0, T100) → lessc61_out_gg(0, T100)
lessc61_in_gg(s(T105), T106) → U28_gg(T105, T106, lessc69_in_gg(T105, T106))
lessc69_in_gg(0, s(T113)) → lessc69_out_gg(0, s(T113))
lessc69_in_gg(s(T118), s(T119)) → U27_gg(T118, T119, lessc69_in_gg(T118, T119))
U27_gg(T118, T119, lessc69_out_gg(T118, T119)) → lessc69_out_gg(s(T118), s(T119))
U28_gg(T105, T106, lessc69_out_gg(T105, T106)) → lessc61_out_gg(s(T105), T106)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
appc18_in_agag(x1, x2, x3, x4)  =  appc18_in_agag(x2, x4)
appc18_out_agag(x1, x2, x3, x4)  =  appc18_out_agag(x1, x2, x3, x4)
U20_agag(x1, x2, x3, x4, x5, x6)  =  U20_agag(x1, x3, x5, x6)
appc28_in_gga(x1, x2, x3)  =  appc28_in_gga(x1, x2)
[]  =  []
appc28_out_gga(x1, x2, x3)  =  appc28_out_gga(x1, x2, x3)
U21_gga(x1, x2, x3, x4, x5)  =  U21_gga(x1, x2, x3, x5)
permc38_in_gg(x1, x2)  =  permc38_in_gg(x1, x2)
permc38_out_gg(x1, x2)  =  permc38_out_gg(x1, x2)
U22_gg(x1, x2, x3, x4)  =  U22_gg(x1, x2, x3, x4)
U23_gg(x1, x2, x3, x4)  =  U23_gg(x1, x2, x3, x4)
U24_gg(x1, x2, x3, x4)  =  U24_gg(x1, x2, x3, x4)
s(x1)  =  s(x1)
lessc61_in_gg(x1, x2)  =  lessc61_in_gg(x1, x2)
0  =  0
lessc61_out_gg(x1, x2)  =  lessc61_out_gg(x1, x2)
U28_gg(x1, x2, x3)  =  U28_gg(x1, x2, x3)
lessc69_in_gg(x1, x2)  =  lessc69_in_gg(x1, x2)
lessc69_out_gg(x1, x2)  =  lessc69_out_gg(x1, x2)
U27_gg(x1, x2, x3)  =  U27_gg(x1, x2, x3)
LESS69_IN_GG(x1, x2)  =  LESS69_IN_GG(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:

LESS69_IN_GG(s(T118), s(T119)) → LESS69_IN_GG(T118, T119)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(10) PiDPToQDPProof (EQUIVALENT 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:

LESS69_IN_GG(s(T118), s(T119)) → LESS69_IN_GG(T118, T119)

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:

  • LESS69_IN_GG(s(T118), s(T119)) → LESS69_IN_GG(T118, T119)
    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:

ORDERED39_IN_GG(T89, .(T90, T91)) → U9_GG(T89, T90, T91, lessc61_in_gg(T89, T90))
U9_GG(T89, T90, T91, lessc61_out_gg(T89, T90)) → ORDERED39_IN_GG(T90, T91)

The TRS R consists of the following rules:

appc18_in_agag([], T26, X46, .(T26, X46)) → appc18_out_agag([], T26, X46, .(T26, X46))
appc18_in_agag(.(X66, X67), T31, X68, .(X66, T32)) → U20_agag(X66, X67, T31, X68, T32, appc18_in_agag(X67, T31, X68, T32))
U20_agag(X66, X67, T31, X68, T32, appc18_out_agag(X67, T31, X68, T32)) → appc18_out_agag(.(X66, X67), T31, X68, .(X66, T32))
appc28_in_gga([], T44, T44) → appc28_out_gga([], T44, T44)
appc28_in_gga(.(T51, T52), T53, .(T51, X101)) → U21_gga(T51, T52, T53, X101, appc28_in_gga(T52, T53, X101))
U21_gga(T51, T52, T53, X101, appc28_out_gga(T52, T53, X101)) → appc28_out_gga(.(T51, T52), T53, .(T51, X101))
permc38_in_gg([], []) → permc38_out_gg([], [])
permc38_in_gg(T62, .(T63, T64)) → U22_gg(T62, T63, T64, appc18_in_agag(T67, T63, T68, T62))
U22_gg(T62, T63, T64, appc18_out_agag(T67, T63, T68, T62)) → U23_gg(T62, T63, T64, appc28_in_gga(T67, T68, T73))
U23_gg(T62, T63, T64, appc28_out_gga(T67, T68, T73)) → U24_gg(T62, T63, T64, permc38_in_gg(T73, T64))
U24_gg(T62, T63, T64, permc38_out_gg(T73, T64)) → permc38_out_gg(T62, .(T63, T64))
lessc61_in_gg(0, T100) → lessc61_out_gg(0, T100)
lessc61_in_gg(s(T105), T106) → U28_gg(T105, T106, lessc69_in_gg(T105, T106))
lessc69_in_gg(0, s(T113)) → lessc69_out_gg(0, s(T113))
lessc69_in_gg(s(T118), s(T119)) → U27_gg(T118, T119, lessc69_in_gg(T118, T119))
U27_gg(T118, T119, lessc69_out_gg(T118, T119)) → lessc69_out_gg(s(T118), s(T119))
U28_gg(T105, T106, lessc69_out_gg(T105, T106)) → lessc61_out_gg(s(T105), T106)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
appc18_in_agag(x1, x2, x3, x4)  =  appc18_in_agag(x2, x4)
appc18_out_agag(x1, x2, x3, x4)  =  appc18_out_agag(x1, x2, x3, x4)
U20_agag(x1, x2, x3, x4, x5, x6)  =  U20_agag(x1, x3, x5, x6)
appc28_in_gga(x1, x2, x3)  =  appc28_in_gga(x1, x2)
[]  =  []
appc28_out_gga(x1, x2, x3)  =  appc28_out_gga(x1, x2, x3)
U21_gga(x1, x2, x3, x4, x5)  =  U21_gga(x1, x2, x3, x5)
permc38_in_gg(x1, x2)  =  permc38_in_gg(x1, x2)
permc38_out_gg(x1, x2)  =  permc38_out_gg(x1, x2)
U22_gg(x1, x2, x3, x4)  =  U22_gg(x1, x2, x3, x4)
U23_gg(x1, x2, x3, x4)  =  U23_gg(x1, x2, x3, x4)
U24_gg(x1, x2, x3, x4)  =  U24_gg(x1, x2, x3, x4)
s(x1)  =  s(x1)
lessc61_in_gg(x1, x2)  =  lessc61_in_gg(x1, x2)
0  =  0
lessc61_out_gg(x1, x2)  =  lessc61_out_gg(x1, x2)
U28_gg(x1, x2, x3)  =  U28_gg(x1, x2, x3)
lessc69_in_gg(x1, x2)  =  lessc69_in_gg(x1, x2)
lessc69_out_gg(x1, x2)  =  lessc69_out_gg(x1, x2)
U27_gg(x1, x2, x3)  =  U27_gg(x1, x2, x3)
ORDERED39_IN_GG(x1, x2)  =  ORDERED39_IN_GG(x1, x2)
U9_GG(x1, x2, x3, x4)  =  U9_GG(x1, x2, x3, x4)

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:

ORDERED39_IN_GG(T89, .(T90, T91)) → U9_GG(T89, T90, T91, lessc61_in_gg(T89, T90))
U9_GG(T89, T90, T91, lessc61_out_gg(T89, T90)) → ORDERED39_IN_GG(T90, T91)

The TRS R consists of the following rules:

lessc61_in_gg(0, T100) → lessc61_out_gg(0, T100)
lessc61_in_gg(s(T105), T106) → U28_gg(T105, T106, lessc69_in_gg(T105, T106))
U28_gg(T105, T106, lessc69_out_gg(T105, T106)) → lessc61_out_gg(s(T105), T106)
lessc69_in_gg(0, s(T113)) → lessc69_out_gg(0, s(T113))
lessc69_in_gg(s(T118), s(T119)) → U27_gg(T118, T119, lessc69_in_gg(T118, T119))
U27_gg(T118, T119, lessc69_out_gg(T118, T119)) → lessc69_out_gg(s(T118), s(T119))

Pi is empty.
We have to consider all (P,R,Pi)-chains

(17) PiDPToQDPProof (EQUIVALENT 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:

ORDERED39_IN_GG(T89, .(T90, T91)) → U9_GG(T89, T90, T91, lessc61_in_gg(T89, T90))
U9_GG(T89, T90, T91, lessc61_out_gg(T89, T90)) → ORDERED39_IN_GG(T90, T91)

The TRS R consists of the following rules:

lessc61_in_gg(0, T100) → lessc61_out_gg(0, T100)
lessc61_in_gg(s(T105), T106) → U28_gg(T105, T106, lessc69_in_gg(T105, T106))
U28_gg(T105, T106, lessc69_out_gg(T105, T106)) → lessc61_out_gg(s(T105), T106)
lessc69_in_gg(0, s(T113)) → lessc69_out_gg(0, s(T113))
lessc69_in_gg(s(T118), s(T119)) → U27_gg(T118, T119, lessc69_in_gg(T118, T119))
U27_gg(T118, T119, lessc69_out_gg(T118, T119)) → lessc69_out_gg(s(T118), s(T119))

The set Q consists of the following terms:

lessc61_in_gg(x0, x1)
U28_gg(x0, x1, x2)
lessc69_in_gg(x0, x1)
U27_gg(x0, x1, x2)

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:

  • U9_GG(T89, T90, T91, lessc61_out_gg(T89, T90)) → ORDERED39_IN_GG(T90, T91)
    The graph contains the following edges 2 >= 1, 4 > 1, 3 >= 2

  • ORDERED39_IN_GG(T89, .(T90, T91)) → U9_GG(T89, T90, T91, lessc61_in_gg(T89, T90))
    The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3

(20) YES

(21) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APP28_IN_GGA(.(T51, T52), T53, .(T51, X101)) → APP28_IN_GGA(T52, T53, X101)

The TRS R consists of the following rules:

appc18_in_agag([], T26, X46, .(T26, X46)) → appc18_out_agag([], T26, X46, .(T26, X46))
appc18_in_agag(.(X66, X67), T31, X68, .(X66, T32)) → U20_agag(X66, X67, T31, X68, T32, appc18_in_agag(X67, T31, X68, T32))
U20_agag(X66, X67, T31, X68, T32, appc18_out_agag(X67, T31, X68, T32)) → appc18_out_agag(.(X66, X67), T31, X68, .(X66, T32))
appc28_in_gga([], T44, T44) → appc28_out_gga([], T44, T44)
appc28_in_gga(.(T51, T52), T53, .(T51, X101)) → U21_gga(T51, T52, T53, X101, appc28_in_gga(T52, T53, X101))
U21_gga(T51, T52, T53, X101, appc28_out_gga(T52, T53, X101)) → appc28_out_gga(.(T51, T52), T53, .(T51, X101))
permc38_in_gg([], []) → permc38_out_gg([], [])
permc38_in_gg(T62, .(T63, T64)) → U22_gg(T62, T63, T64, appc18_in_agag(T67, T63, T68, T62))
U22_gg(T62, T63, T64, appc18_out_agag(T67, T63, T68, T62)) → U23_gg(T62, T63, T64, appc28_in_gga(T67, T68, T73))
U23_gg(T62, T63, T64, appc28_out_gga(T67, T68, T73)) → U24_gg(T62, T63, T64, permc38_in_gg(T73, T64))
U24_gg(T62, T63, T64, permc38_out_gg(T73, T64)) → permc38_out_gg(T62, .(T63, T64))
lessc61_in_gg(0, T100) → lessc61_out_gg(0, T100)
lessc61_in_gg(s(T105), T106) → U28_gg(T105, T106, lessc69_in_gg(T105, T106))
lessc69_in_gg(0, s(T113)) → lessc69_out_gg(0, s(T113))
lessc69_in_gg(s(T118), s(T119)) → U27_gg(T118, T119, lessc69_in_gg(T118, T119))
U27_gg(T118, T119, lessc69_out_gg(T118, T119)) → lessc69_out_gg(s(T118), s(T119))
U28_gg(T105, T106, lessc69_out_gg(T105, T106)) → lessc61_out_gg(s(T105), T106)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
appc18_in_agag(x1, x2, x3, x4)  =  appc18_in_agag(x2, x4)
appc18_out_agag(x1, x2, x3, x4)  =  appc18_out_agag(x1, x2, x3, x4)
U20_agag(x1, x2, x3, x4, x5, x6)  =  U20_agag(x1, x3, x5, x6)
appc28_in_gga(x1, x2, x3)  =  appc28_in_gga(x1, x2)
[]  =  []
appc28_out_gga(x1, x2, x3)  =  appc28_out_gga(x1, x2, x3)
U21_gga(x1, x2, x3, x4, x5)  =  U21_gga(x1, x2, x3, x5)
permc38_in_gg(x1, x2)  =  permc38_in_gg(x1, x2)
permc38_out_gg(x1, x2)  =  permc38_out_gg(x1, x2)
U22_gg(x1, x2, x3, x4)  =  U22_gg(x1, x2, x3, x4)
U23_gg(x1, x2, x3, x4)  =  U23_gg(x1, x2, x3, x4)
U24_gg(x1, x2, x3, x4)  =  U24_gg(x1, x2, x3, x4)
s(x1)  =  s(x1)
lessc61_in_gg(x1, x2)  =  lessc61_in_gg(x1, x2)
0  =  0
lessc61_out_gg(x1, x2)  =  lessc61_out_gg(x1, x2)
U28_gg(x1, x2, x3)  =  U28_gg(x1, x2, x3)
lessc69_in_gg(x1, x2)  =  lessc69_in_gg(x1, x2)
lessc69_out_gg(x1, x2)  =  lessc69_out_gg(x1, x2)
U27_gg(x1, x2, x3)  =  U27_gg(x1, x2, x3)
APP28_IN_GGA(x1, x2, x3)  =  APP28_IN_GGA(x1, x2)

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:

APP28_IN_GGA(.(T51, T52), T53, .(T51, X101)) → APP28_IN_GGA(T52, T53, X101)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
APP28_IN_GGA(x1, x2, x3)  =  APP28_IN_GGA(x1, x2)

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:

APP28_IN_GGA(.(T51, T52), T53) → APP28_IN_GGA(T52, T53)

R is empty.
Q is empty.
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:

  • APP28_IN_GGA(.(T51, T52), T53) → APP28_IN_GGA(T52, T53)
    The graph contains the following edges 1 > 1, 2 >= 2

(27) YES

(28) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APP18_IN_AGAG(.(X66, X67), T31, X68, .(X66, T32)) → APP18_IN_AGAG(X67, T31, X68, T32)

The TRS R consists of the following rules:

appc18_in_agag([], T26, X46, .(T26, X46)) → appc18_out_agag([], T26, X46, .(T26, X46))
appc18_in_agag(.(X66, X67), T31, X68, .(X66, T32)) → U20_agag(X66, X67, T31, X68, T32, appc18_in_agag(X67, T31, X68, T32))
U20_agag(X66, X67, T31, X68, T32, appc18_out_agag(X67, T31, X68, T32)) → appc18_out_agag(.(X66, X67), T31, X68, .(X66, T32))
appc28_in_gga([], T44, T44) → appc28_out_gga([], T44, T44)
appc28_in_gga(.(T51, T52), T53, .(T51, X101)) → U21_gga(T51, T52, T53, X101, appc28_in_gga(T52, T53, X101))
U21_gga(T51, T52, T53, X101, appc28_out_gga(T52, T53, X101)) → appc28_out_gga(.(T51, T52), T53, .(T51, X101))
permc38_in_gg([], []) → permc38_out_gg([], [])
permc38_in_gg(T62, .(T63, T64)) → U22_gg(T62, T63, T64, appc18_in_agag(T67, T63, T68, T62))
U22_gg(T62, T63, T64, appc18_out_agag(T67, T63, T68, T62)) → U23_gg(T62, T63, T64, appc28_in_gga(T67, T68, T73))
U23_gg(T62, T63, T64, appc28_out_gga(T67, T68, T73)) → U24_gg(T62, T63, T64, permc38_in_gg(T73, T64))
U24_gg(T62, T63, T64, permc38_out_gg(T73, T64)) → permc38_out_gg(T62, .(T63, T64))
lessc61_in_gg(0, T100) → lessc61_out_gg(0, T100)
lessc61_in_gg(s(T105), T106) → U28_gg(T105, T106, lessc69_in_gg(T105, T106))
lessc69_in_gg(0, s(T113)) → lessc69_out_gg(0, s(T113))
lessc69_in_gg(s(T118), s(T119)) → U27_gg(T118, T119, lessc69_in_gg(T118, T119))
U27_gg(T118, T119, lessc69_out_gg(T118, T119)) → lessc69_out_gg(s(T118), s(T119))
U28_gg(T105, T106, lessc69_out_gg(T105, T106)) → lessc61_out_gg(s(T105), T106)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
appc18_in_agag(x1, x2, x3, x4)  =  appc18_in_agag(x2, x4)
appc18_out_agag(x1, x2, x3, x4)  =  appc18_out_agag(x1, x2, x3, x4)
U20_agag(x1, x2, x3, x4, x5, x6)  =  U20_agag(x1, x3, x5, x6)
appc28_in_gga(x1, x2, x3)  =  appc28_in_gga(x1, x2)
[]  =  []
appc28_out_gga(x1, x2, x3)  =  appc28_out_gga(x1, x2, x3)
U21_gga(x1, x2, x3, x4, x5)  =  U21_gga(x1, x2, x3, x5)
permc38_in_gg(x1, x2)  =  permc38_in_gg(x1, x2)
permc38_out_gg(x1, x2)  =  permc38_out_gg(x1, x2)
U22_gg(x1, x2, x3, x4)  =  U22_gg(x1, x2, x3, x4)
U23_gg(x1, x2, x3, x4)  =  U23_gg(x1, x2, x3, x4)
U24_gg(x1, x2, x3, x4)  =  U24_gg(x1, x2, x3, x4)
s(x1)  =  s(x1)
lessc61_in_gg(x1, x2)  =  lessc61_in_gg(x1, x2)
0  =  0
lessc61_out_gg(x1, x2)  =  lessc61_out_gg(x1, x2)
U28_gg(x1, x2, x3)  =  U28_gg(x1, x2, x3)
lessc69_in_gg(x1, x2)  =  lessc69_in_gg(x1, x2)
lessc69_out_gg(x1, x2)  =  lessc69_out_gg(x1, x2)
U27_gg(x1, x2, x3)  =  U27_gg(x1, x2, x3)
APP18_IN_AGAG(x1, x2, x3, x4)  =  APP18_IN_AGAG(x2, x4)

We have to consider all (P,R,Pi)-chains

(29) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(30) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APP18_IN_AGAG(.(X66, X67), T31, X68, .(X66, T32)) → APP18_IN_AGAG(X67, T31, X68, T32)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
APP18_IN_AGAG(x1, x2, x3, x4)  =  APP18_IN_AGAG(x2, x4)

We have to consider all (P,R,Pi)-chains

(31) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(32) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APP18_IN_AGAG(T31, .(X66, T32)) → APP18_IN_AGAG(T31, T32)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(33) 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:

  • APP18_IN_AGAG(T31, .(X66, T32)) → APP18_IN_AGAG(T31, T32)
    The graph contains the following edges 1 >= 1, 2 > 2

(34) YES

(35) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

PERM38_IN_GG(T62, .(T63, T64)) → U4_GG(T62, T63, T64, appc18_in_agag(T67, T63, T68, T62))
U4_GG(T62, T63, T64, appc18_out_agag(T67, T63, T68, T62)) → U6_GG(T62, T63, T64, appc28_in_gga(T67, T68, T73))
U6_GG(T62, T63, T64, appc28_out_gga(T67, T68, T73)) → PERM38_IN_GG(T73, T64)

The TRS R consists of the following rules:

appc18_in_agag([], T26, X46, .(T26, X46)) → appc18_out_agag([], T26, X46, .(T26, X46))
appc18_in_agag(.(X66, X67), T31, X68, .(X66, T32)) → U20_agag(X66, X67, T31, X68, T32, appc18_in_agag(X67, T31, X68, T32))
U20_agag(X66, X67, T31, X68, T32, appc18_out_agag(X67, T31, X68, T32)) → appc18_out_agag(.(X66, X67), T31, X68, .(X66, T32))
appc28_in_gga([], T44, T44) → appc28_out_gga([], T44, T44)
appc28_in_gga(.(T51, T52), T53, .(T51, X101)) → U21_gga(T51, T52, T53, X101, appc28_in_gga(T52, T53, X101))
U21_gga(T51, T52, T53, X101, appc28_out_gga(T52, T53, X101)) → appc28_out_gga(.(T51, T52), T53, .(T51, X101))
permc38_in_gg([], []) → permc38_out_gg([], [])
permc38_in_gg(T62, .(T63, T64)) → U22_gg(T62, T63, T64, appc18_in_agag(T67, T63, T68, T62))
U22_gg(T62, T63, T64, appc18_out_agag(T67, T63, T68, T62)) → U23_gg(T62, T63, T64, appc28_in_gga(T67, T68, T73))
U23_gg(T62, T63, T64, appc28_out_gga(T67, T68, T73)) → U24_gg(T62, T63, T64, permc38_in_gg(T73, T64))
U24_gg(T62, T63, T64, permc38_out_gg(T73, T64)) → permc38_out_gg(T62, .(T63, T64))
lessc61_in_gg(0, T100) → lessc61_out_gg(0, T100)
lessc61_in_gg(s(T105), T106) → U28_gg(T105, T106, lessc69_in_gg(T105, T106))
lessc69_in_gg(0, s(T113)) → lessc69_out_gg(0, s(T113))
lessc69_in_gg(s(T118), s(T119)) → U27_gg(T118, T119, lessc69_in_gg(T118, T119))
U27_gg(T118, T119, lessc69_out_gg(T118, T119)) → lessc69_out_gg(s(T118), s(T119))
U28_gg(T105, T106, lessc69_out_gg(T105, T106)) → lessc61_out_gg(s(T105), T106)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
appc18_in_agag(x1, x2, x3, x4)  =  appc18_in_agag(x2, x4)
appc18_out_agag(x1, x2, x3, x4)  =  appc18_out_agag(x1, x2, x3, x4)
U20_agag(x1, x2, x3, x4, x5, x6)  =  U20_agag(x1, x3, x5, x6)
appc28_in_gga(x1, x2, x3)  =  appc28_in_gga(x1, x2)
[]  =  []
appc28_out_gga(x1, x2, x3)  =  appc28_out_gga(x1, x2, x3)
U21_gga(x1, x2, x3, x4, x5)  =  U21_gga(x1, x2, x3, x5)
permc38_in_gg(x1, x2)  =  permc38_in_gg(x1, x2)
permc38_out_gg(x1, x2)  =  permc38_out_gg(x1, x2)
U22_gg(x1, x2, x3, x4)  =  U22_gg(x1, x2, x3, x4)
U23_gg(x1, x2, x3, x4)  =  U23_gg(x1, x2, x3, x4)
U24_gg(x1, x2, x3, x4)  =  U24_gg(x1, x2, x3, x4)
s(x1)  =  s(x1)
lessc61_in_gg(x1, x2)  =  lessc61_in_gg(x1, x2)
0  =  0
lessc61_out_gg(x1, x2)  =  lessc61_out_gg(x1, x2)
U28_gg(x1, x2, x3)  =  U28_gg(x1, x2, x3)
lessc69_in_gg(x1, x2)  =  lessc69_in_gg(x1, x2)
lessc69_out_gg(x1, x2)  =  lessc69_out_gg(x1, x2)
U27_gg(x1, x2, x3)  =  U27_gg(x1, x2, x3)
PERM38_IN_GG(x1, x2)  =  PERM38_IN_GG(x1, x2)
U4_GG(x1, x2, x3, x4)  =  U4_GG(x1, x2, x3, x4)
U6_GG(x1, x2, x3, x4)  =  U6_GG(x1, x2, x3, x4)

We have to consider all (P,R,Pi)-chains

(36) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(37) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

PERM38_IN_GG(T62, .(T63, T64)) → U4_GG(T62, T63, T64, appc18_in_agag(T67, T63, T68, T62))
U4_GG(T62, T63, T64, appc18_out_agag(T67, T63, T68, T62)) → U6_GG(T62, T63, T64, appc28_in_gga(T67, T68, T73))
U6_GG(T62, T63, T64, appc28_out_gga(T67, T68, T73)) → PERM38_IN_GG(T73, T64)

The TRS R consists of the following rules:

appc18_in_agag([], T26, X46, .(T26, X46)) → appc18_out_agag([], T26, X46, .(T26, X46))
appc18_in_agag(.(X66, X67), T31, X68, .(X66, T32)) → U20_agag(X66, X67, T31, X68, T32, appc18_in_agag(X67, T31, X68, T32))
appc28_in_gga([], T44, T44) → appc28_out_gga([], T44, T44)
appc28_in_gga(.(T51, T52), T53, .(T51, X101)) → U21_gga(T51, T52, T53, X101, appc28_in_gga(T52, T53, X101))
U20_agag(X66, X67, T31, X68, T32, appc18_out_agag(X67, T31, X68, T32)) → appc18_out_agag(.(X66, X67), T31, X68, .(X66, T32))
U21_gga(T51, T52, T53, X101, appc28_out_gga(T52, T53, X101)) → appc28_out_gga(.(T51, T52), T53, .(T51, X101))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
appc18_in_agag(x1, x2, x3, x4)  =  appc18_in_agag(x2, x4)
appc18_out_agag(x1, x2, x3, x4)  =  appc18_out_agag(x1, x2, x3, x4)
U20_agag(x1, x2, x3, x4, x5, x6)  =  U20_agag(x1, x3, x5, x6)
appc28_in_gga(x1, x2, x3)  =  appc28_in_gga(x1, x2)
[]  =  []
appc28_out_gga(x1, x2, x3)  =  appc28_out_gga(x1, x2, x3)
U21_gga(x1, x2, x3, x4, x5)  =  U21_gga(x1, x2, x3, x5)
PERM38_IN_GG(x1, x2)  =  PERM38_IN_GG(x1, x2)
U4_GG(x1, x2, x3, x4)  =  U4_GG(x1, x2, x3, x4)
U6_GG(x1, x2, x3, x4)  =  U6_GG(x1, x2, x3, x4)

We have to consider all (P,R,Pi)-chains

(38) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(39) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PERM38_IN_GG(T62, .(T63, T64)) → U4_GG(T62, T63, T64, appc18_in_agag(T63, T62))
U4_GG(T62, T63, T64, appc18_out_agag(T67, T63, T68, T62)) → U6_GG(T62, T63, T64, appc28_in_gga(T67, T68))
U6_GG(T62, T63, T64, appc28_out_gga(T67, T68, T73)) → PERM38_IN_GG(T73, T64)

The TRS R consists of the following rules:

appc18_in_agag(T26, .(T26, X46)) → appc18_out_agag([], T26, X46, .(T26, X46))
appc18_in_agag(T31, .(X66, T32)) → U20_agag(X66, T31, T32, appc18_in_agag(T31, T32))
appc28_in_gga([], T44) → appc28_out_gga([], T44, T44)
appc28_in_gga(.(T51, T52), T53) → U21_gga(T51, T52, T53, appc28_in_gga(T52, T53))
U20_agag(X66, T31, T32, appc18_out_agag(X67, T31, X68, T32)) → appc18_out_agag(.(X66, X67), T31, X68, .(X66, T32))
U21_gga(T51, T52, T53, appc28_out_gga(T52, T53, X101)) → appc28_out_gga(.(T51, T52), T53, .(T51, X101))

The set Q consists of the following terms:

appc18_in_agag(x0, x1)
appc28_in_gga(x0, x1)
U20_agag(x0, x1, x2, x3)
U21_gga(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.

(40) 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:

  • U4_GG(T62, T63, T64, appc18_out_agag(T67, T63, T68, T62)) → U6_GG(T62, T63, T64, appc28_in_gga(T67, T68))
    The graph contains the following edges 1 >= 1, 4 > 1, 2 >= 2, 4 > 2, 3 >= 3

  • U6_GG(T62, T63, T64, appc28_out_gga(T67, T68, T73)) → PERM38_IN_GG(T73, T64)
    The graph contains the following edges 4 > 1, 3 >= 2

  • PERM38_IN_GG(T62, .(T63, T64)) → U4_GG(T62, T63, T64, appc18_in_agag(T63, T62))
    The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3

(41) YES