(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) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph.

(2) Obligation:

Clauses:

app18([], T26, X46, .(T26, X46)).
app18(.(X66, X67), T31, X68, .(X66, T32)) :- app18(X67, T31, X68, T32).
app28([], T44, T44).
app28(.(T51, T52), T53, .(T51, X101)) :- app28(T52, T53, X101).
perm38([], []).
perm38(T62, .(T63, T64)) :- app18(X120, T63, X121, T62).
perm38(T62, .(T63, T64)) :- ','(app18(T67, T63, T68, T62), app28(T67, T68, X122)).
perm38(T62, .(T63, T64)) :- ','(app18(T67, T63, T68, T62), ','(app28(T67, T68, T73), perm38(T73, T64))).
ordered39(T82, []).
ordered39(T89, .(T90, T91)) :- less61(T89, T90).
ordered39(T89, .(T90, T91)) :- ','(less61(T89, T90), ordered39(T90, T91)).
less69(0, s(T113)).
less69(s(T118), s(T119)) :- less69(T118, T119).
less61(0, T100).
less61(s(T105), T106) :- less69(T105, T106).
ss1([], []).
ss1(T13, .(T14, T15)) :- app18(X23, T14, X24, T13).
ss1(T13, .(T14, T15)) :- ','(app18(T18, T14, T19, T13), app28(T18, T19, X25)).
ss1(T13, .(T14, T15)) :- ','(app18(T18, T14, T19, T13), ','(app28(T18, T19, T37), perm38(T37, T15))).
ss1(T13, .(T14, T15)) :- ','(app18(T18, T14, T19, T13), ','(app28(T18, T19, T37), ','(perm38(T37, T15), ordered39(T14, T15)))).

Queries:

ss1(g,g).

(3) PrologToPiTRSProof (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)
app28_in: (b,b,f)
perm38_in: (b,b)
ordered39_in: (b,b)
less61_in: (b,b)
less69_in: (b,b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

ss1_in_gg([], []) → ss1_out_gg([], [])
ss1_in_gg(T13, .(T14, T15)) → U12_gg(T13, T14, T15, app18_in_agag(X23, T14, X24, T13))
app18_in_agag([], T26, X46, .(T26, X46)) → app18_out_agag([], T26, X46, .(T26, X46))
app18_in_agag(.(X66, X67), T31, X68, .(X66, T32)) → U1_agag(X66, X67, T31, X68, T32, app18_in_agag(X67, T31, X68, T32))
U1_agag(X66, X67, T31, X68, T32, app18_out_agag(X67, T31, X68, T32)) → app18_out_agag(.(X66, X67), T31, X68, .(X66, T32))
U12_gg(T13, T14, T15, app18_out_agag(X23, T14, X24, T13)) → ss1_out_gg(T13, .(T14, T15))
ss1_in_gg(T13, .(T14, T15)) → U13_gg(T13, T14, T15, app18_in_agag(T18, T14, T19, T13))
U13_gg(T13, T14, T15, app18_out_agag(T18, T14, T19, T13)) → U14_gg(T13, T14, T15, app28_in_gga(T18, T19, X25))
app28_in_gga([], T44, T44) → app28_out_gga([], T44, T44)
app28_in_gga(.(T51, T52), T53, .(T51, X101)) → U2_gga(T51, T52, T53, X101, app28_in_gga(T52, T53, X101))
U2_gga(T51, T52, T53, X101, app28_out_gga(T52, T53, X101)) → app28_out_gga(.(T51, T52), T53, .(T51, X101))
U14_gg(T13, T14, T15, app28_out_gga(T18, T19, X25)) → ss1_out_gg(T13, .(T14, T15))
U13_gg(T13, T14, T15, app18_out_agag(T18, T14, T19, T13)) → U15_gg(T13, T14, T15, app28_in_gga(T18, T19, T37))
U15_gg(T13, T14, T15, app28_out_gga(T18, T19, T37)) → U16_gg(T13, T14, T15, perm38_in_gg(T37, T15))
perm38_in_gg([], []) → perm38_out_gg([], [])
perm38_in_gg(T62, .(T63, T64)) → U3_gg(T62, T63, T64, app18_in_agag(X120, T63, X121, T62))
U3_gg(T62, T63, T64, app18_out_agag(X120, T63, X121, T62)) → perm38_out_gg(T62, .(T63, T64))
perm38_in_gg(T62, .(T63, T64)) → U4_gg(T62, T63, T64, app18_in_agag(T67, T63, T68, T62))
U4_gg(T62, T63, T64, app18_out_agag(T67, T63, T68, T62)) → U5_gg(T62, T63, T64, app28_in_gga(T67, T68, X122))
U5_gg(T62, T63, T64, app28_out_gga(T67, T68, X122)) → perm38_out_gg(T62, .(T63, T64))
U4_gg(T62, T63, T64, app18_out_agag(T67, T63, T68, T62)) → U6_gg(T62, T63, T64, app28_in_gga(T67, T68, T73))
U6_gg(T62, T63, T64, app28_out_gga(T67, T68, T73)) → U7_gg(T62, T63, T64, perm38_in_gg(T73, T64))
U7_gg(T62, T63, T64, perm38_out_gg(T73, T64)) → perm38_out_gg(T62, .(T63, T64))
U16_gg(T13, T14, T15, perm38_out_gg(T37, T15)) → ss1_out_gg(T13, .(T14, T15))
U16_gg(T13, T14, T15, perm38_out_gg(T37, T15)) → U17_gg(T13, T14, T15, ordered39_in_gg(T14, T15))
ordered39_in_gg(T82, []) → ordered39_out_gg(T82, [])
ordered39_in_gg(T89, .(T90, T91)) → U8_gg(T89, T90, T91, less61_in_gg(T89, T90))
less61_in_gg(0, T100) → less61_out_gg(0, T100)
less61_in_gg(s(T105), T106) → U11_gg(T105, T106, less69_in_gg(T105, T106))
less69_in_gg(0, s(T113)) → less69_out_gg(0, s(T113))
less69_in_gg(s(T118), s(T119)) → U10_gg(T118, T119, less69_in_gg(T118, T119))
U10_gg(T118, T119, less69_out_gg(T118, T119)) → less69_out_gg(s(T118), s(T119))
U11_gg(T105, T106, less69_out_gg(T105, T106)) → less61_out_gg(s(T105), T106)
U8_gg(T89, T90, T91, less61_out_gg(T89, T90)) → ordered39_out_gg(T89, .(T90, T91))
U8_gg(T89, T90, T91, less61_out_gg(T89, T90)) → U9_gg(T89, T90, T91, ordered39_in_gg(T90, T91))
U9_gg(T89, T90, T91, ordered39_out_gg(T90, T91)) → ordered39_out_gg(T89, .(T90, T91))
U17_gg(T13, T14, T15, ordered39_out_gg(T14, T15)) → ss1_out_gg(T13, .(T14, T15))

The argument filtering Pi contains the following mapping:
ss1_in_gg(x1, x2)  =  ss1_in_gg(x1, x2)
[]  =  []
ss1_out_gg(x1, x2)  =  ss1_out_gg
.(x1, x2)  =  .(x1, x2)
U12_gg(x1, x2, x3, x4)  =  U12_gg(x4)
app18_in_agag(x1, x2, x3, x4)  =  app18_in_agag(x2, x4)
app18_out_agag(x1, x2, x3, x4)  =  app18_out_agag(x1, x3)
U1_agag(x1, x2, x3, x4, x5, x6)  =  U1_agag(x1, x6)
U13_gg(x1, x2, x3, x4)  =  U13_gg(x2, x3, x4)
U14_gg(x1, x2, x3, x4)  =  U14_gg(x4)
app28_in_gga(x1, x2, x3)  =  app28_in_gga(x1, x2)
app28_out_gga(x1, x2, x3)  =  app28_out_gga(x3)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x5)
U15_gg(x1, x2, x3, x4)  =  U15_gg(x2, x3, x4)
U16_gg(x1, x2, x3, x4)  =  U16_gg(x2, x3, x4)
perm38_in_gg(x1, x2)  =  perm38_in_gg(x1, x2)
perm38_out_gg(x1, x2)  =  perm38_out_gg
U3_gg(x1, x2, x3, x4)  =  U3_gg(x4)
U4_gg(x1, x2, x3, x4)  =  U4_gg(x3, x4)
U5_gg(x1, x2, x3, x4)  =  U5_gg(x4)
U6_gg(x1, x2, x3, x4)  =  U6_gg(x3, x4)
U7_gg(x1, x2, x3, x4)  =  U7_gg(x4)
U17_gg(x1, x2, x3, x4)  =  U17_gg(x4)
ordered39_in_gg(x1, x2)  =  ordered39_in_gg(x1, x2)
ordered39_out_gg(x1, x2)  =  ordered39_out_gg
U8_gg(x1, x2, x3, x4)  =  U8_gg(x2, x3, x4)
less61_in_gg(x1, x2)  =  less61_in_gg(x1, x2)
0  =  0
less61_out_gg(x1, x2)  =  less61_out_gg
s(x1)  =  s(x1)
U11_gg(x1, x2, x3)  =  U11_gg(x3)
less69_in_gg(x1, x2)  =  less69_in_gg(x1, x2)
less69_out_gg(x1, x2)  =  less69_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
U9_gg(x1, x2, x3, x4)  =  U9_gg(x4)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

ss1_in_gg([], []) → ss1_out_gg([], [])
ss1_in_gg(T13, .(T14, T15)) → U12_gg(T13, T14, T15, app18_in_agag(X23, T14, X24, T13))
app18_in_agag([], T26, X46, .(T26, X46)) → app18_out_agag([], T26, X46, .(T26, X46))
app18_in_agag(.(X66, X67), T31, X68, .(X66, T32)) → U1_agag(X66, X67, T31, X68, T32, app18_in_agag(X67, T31, X68, T32))
U1_agag(X66, X67, T31, X68, T32, app18_out_agag(X67, T31, X68, T32)) → app18_out_agag(.(X66, X67), T31, X68, .(X66, T32))
U12_gg(T13, T14, T15, app18_out_agag(X23, T14, X24, T13)) → ss1_out_gg(T13, .(T14, T15))
ss1_in_gg(T13, .(T14, T15)) → U13_gg(T13, T14, T15, app18_in_agag(T18, T14, T19, T13))
U13_gg(T13, T14, T15, app18_out_agag(T18, T14, T19, T13)) → U14_gg(T13, T14, T15, app28_in_gga(T18, T19, X25))
app28_in_gga([], T44, T44) → app28_out_gga([], T44, T44)
app28_in_gga(.(T51, T52), T53, .(T51, X101)) → U2_gga(T51, T52, T53, X101, app28_in_gga(T52, T53, X101))
U2_gga(T51, T52, T53, X101, app28_out_gga(T52, T53, X101)) → app28_out_gga(.(T51, T52), T53, .(T51, X101))
U14_gg(T13, T14, T15, app28_out_gga(T18, T19, X25)) → ss1_out_gg(T13, .(T14, T15))
U13_gg(T13, T14, T15, app18_out_agag(T18, T14, T19, T13)) → U15_gg(T13, T14, T15, app28_in_gga(T18, T19, T37))
U15_gg(T13, T14, T15, app28_out_gga(T18, T19, T37)) → U16_gg(T13, T14, T15, perm38_in_gg(T37, T15))
perm38_in_gg([], []) → perm38_out_gg([], [])
perm38_in_gg(T62, .(T63, T64)) → U3_gg(T62, T63, T64, app18_in_agag(X120, T63, X121, T62))
U3_gg(T62, T63, T64, app18_out_agag(X120, T63, X121, T62)) → perm38_out_gg(T62, .(T63, T64))
perm38_in_gg(T62, .(T63, T64)) → U4_gg(T62, T63, T64, app18_in_agag(T67, T63, T68, T62))
U4_gg(T62, T63, T64, app18_out_agag(T67, T63, T68, T62)) → U5_gg(T62, T63, T64, app28_in_gga(T67, T68, X122))
U5_gg(T62, T63, T64, app28_out_gga(T67, T68, X122)) → perm38_out_gg(T62, .(T63, T64))
U4_gg(T62, T63, T64, app18_out_agag(T67, T63, T68, T62)) → U6_gg(T62, T63, T64, app28_in_gga(T67, T68, T73))
U6_gg(T62, T63, T64, app28_out_gga(T67, T68, T73)) → U7_gg(T62, T63, T64, perm38_in_gg(T73, T64))
U7_gg(T62, T63, T64, perm38_out_gg(T73, T64)) → perm38_out_gg(T62, .(T63, T64))
U16_gg(T13, T14, T15, perm38_out_gg(T37, T15)) → ss1_out_gg(T13, .(T14, T15))
U16_gg(T13, T14, T15, perm38_out_gg(T37, T15)) → U17_gg(T13, T14, T15, ordered39_in_gg(T14, T15))
ordered39_in_gg(T82, []) → ordered39_out_gg(T82, [])
ordered39_in_gg(T89, .(T90, T91)) → U8_gg(T89, T90, T91, less61_in_gg(T89, T90))
less61_in_gg(0, T100) → less61_out_gg(0, T100)
less61_in_gg(s(T105), T106) → U11_gg(T105, T106, less69_in_gg(T105, T106))
less69_in_gg(0, s(T113)) → less69_out_gg(0, s(T113))
less69_in_gg(s(T118), s(T119)) → U10_gg(T118, T119, less69_in_gg(T118, T119))
U10_gg(T118, T119, less69_out_gg(T118, T119)) → less69_out_gg(s(T118), s(T119))
U11_gg(T105, T106, less69_out_gg(T105, T106)) → less61_out_gg(s(T105), T106)
U8_gg(T89, T90, T91, less61_out_gg(T89, T90)) → ordered39_out_gg(T89, .(T90, T91))
U8_gg(T89, T90, T91, less61_out_gg(T89, T90)) → U9_gg(T89, T90, T91, ordered39_in_gg(T90, T91))
U9_gg(T89, T90, T91, ordered39_out_gg(T90, T91)) → ordered39_out_gg(T89, .(T90, T91))
U17_gg(T13, T14, T15, ordered39_out_gg(T14, T15)) → ss1_out_gg(T13, .(T14, T15))

The argument filtering Pi contains the following mapping:
ss1_in_gg(x1, x2)  =  ss1_in_gg(x1, x2)
[]  =  []
ss1_out_gg(x1, x2)  =  ss1_out_gg
.(x1, x2)  =  .(x1, x2)
U12_gg(x1, x2, x3, x4)  =  U12_gg(x4)
app18_in_agag(x1, x2, x3, x4)  =  app18_in_agag(x2, x4)
app18_out_agag(x1, x2, x3, x4)  =  app18_out_agag(x1, x3)
U1_agag(x1, x2, x3, x4, x5, x6)  =  U1_agag(x1, x6)
U13_gg(x1, x2, x3, x4)  =  U13_gg(x2, x3, x4)
U14_gg(x1, x2, x3, x4)  =  U14_gg(x4)
app28_in_gga(x1, x2, x3)  =  app28_in_gga(x1, x2)
app28_out_gga(x1, x2, x3)  =  app28_out_gga(x3)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x5)
U15_gg(x1, x2, x3, x4)  =  U15_gg(x2, x3, x4)
U16_gg(x1, x2, x3, x4)  =  U16_gg(x2, x3, x4)
perm38_in_gg(x1, x2)  =  perm38_in_gg(x1, x2)
perm38_out_gg(x1, x2)  =  perm38_out_gg
U3_gg(x1, x2, x3, x4)  =  U3_gg(x4)
U4_gg(x1, x2, x3, x4)  =  U4_gg(x3, x4)
U5_gg(x1, x2, x3, x4)  =  U5_gg(x4)
U6_gg(x1, x2, x3, x4)  =  U6_gg(x3, x4)
U7_gg(x1, x2, x3, x4)  =  U7_gg(x4)
U17_gg(x1, x2, x3, x4)  =  U17_gg(x4)
ordered39_in_gg(x1, x2)  =  ordered39_in_gg(x1, x2)
ordered39_out_gg(x1, x2)  =  ordered39_out_gg
U8_gg(x1, x2, x3, x4)  =  U8_gg(x2, x3, x4)
less61_in_gg(x1, x2)  =  less61_in_gg(x1, x2)
0  =  0
less61_out_gg(x1, x2)  =  less61_out_gg
s(x1)  =  s(x1)
U11_gg(x1, x2, x3)  =  U11_gg(x3)
less69_in_gg(x1, x2)  =  less69_in_gg(x1, x2)
less69_out_gg(x1, x2)  =  less69_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
U9_gg(x1, x2, x3, x4)  =  U9_gg(x4)

(5) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
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, app18_in_agag(T18, T14, T19, T13))
U13_GG(T13, T14, T15, app18_out_agag(T18, T14, T19, T13)) → U14_GG(T13, T14, T15, app28_in_gga(T18, T19, X25))
U13_GG(T13, T14, T15, app18_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, app18_out_agag(T18, T14, T19, T13)) → U15_GG(T13, T14, T15, app28_in_gga(T18, T19, T37))
U15_GG(T13, T14, T15, app28_out_gga(T18, T19, T37)) → U16_GG(T13, T14, T15, perm38_in_gg(T37, T15))
U15_GG(T13, T14, T15, app28_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, app18_in_agag(T67, T63, T68, T62))
U4_GG(T62, T63, T64, app18_out_agag(T67, T63, T68, T62)) → U5_GG(T62, T63, T64, app28_in_gga(T67, T68, X122))
U4_GG(T62, T63, T64, app18_out_agag(T67, T63, T68, T62)) → APP28_IN_GGA(T67, T68, X122)
U4_GG(T62, T63, T64, app18_out_agag(T67, T63, T68, T62)) → U6_GG(T62, T63, T64, app28_in_gga(T67, T68, T73))
U6_GG(T62, T63, T64, app28_out_gga(T67, T68, T73)) → U7_GG(T62, T63, T64, perm38_in_gg(T73, T64))
U6_GG(T62, T63, T64, app28_out_gga(T67, T68, T73)) → PERM38_IN_GG(T73, T64)
U16_GG(T13, T14, T15, perm38_out_gg(T37, T15)) → U17_GG(T13, T14, T15, ordered39_in_gg(T14, T15))
U16_GG(T13, T14, T15, perm38_out_gg(T37, T15)) → ORDERED39_IN_GG(T14, T15)
ORDERED39_IN_GG(T89, .(T90, T91)) → U8_GG(T89, T90, T91, less61_in_gg(T89, T90))
ORDERED39_IN_GG(T89, .(T90, T91)) → LESS61_IN_GG(T89, T90)
LESS61_IN_GG(s(T105), T106) → U11_GG(T105, T106, less69_in_gg(T105, T106))
LESS61_IN_GG(s(T105), T106) → LESS69_IN_GG(T105, T106)
LESS69_IN_GG(s(T118), s(T119)) → U10_GG(T118, T119, less69_in_gg(T118, T119))
LESS69_IN_GG(s(T118), s(T119)) → LESS69_IN_GG(T118, T119)
U8_GG(T89, T90, T91, less61_out_gg(T89, T90)) → U9_GG(T89, T90, T91, ordered39_in_gg(T90, T91))
U8_GG(T89, T90, T91, less61_out_gg(T89, T90)) → ORDERED39_IN_GG(T90, T91)

The TRS R consists of the following rules:

ss1_in_gg([], []) → ss1_out_gg([], [])
ss1_in_gg(T13, .(T14, T15)) → U12_gg(T13, T14, T15, app18_in_agag(X23, T14, X24, T13))
app18_in_agag([], T26, X46, .(T26, X46)) → app18_out_agag([], T26, X46, .(T26, X46))
app18_in_agag(.(X66, X67), T31, X68, .(X66, T32)) → U1_agag(X66, X67, T31, X68, T32, app18_in_agag(X67, T31, X68, T32))
U1_agag(X66, X67, T31, X68, T32, app18_out_agag(X67, T31, X68, T32)) → app18_out_agag(.(X66, X67), T31, X68, .(X66, T32))
U12_gg(T13, T14, T15, app18_out_agag(X23, T14, X24, T13)) → ss1_out_gg(T13, .(T14, T15))
ss1_in_gg(T13, .(T14, T15)) → U13_gg(T13, T14, T15, app18_in_agag(T18, T14, T19, T13))
U13_gg(T13, T14, T15, app18_out_agag(T18, T14, T19, T13)) → U14_gg(T13, T14, T15, app28_in_gga(T18, T19, X25))
app28_in_gga([], T44, T44) → app28_out_gga([], T44, T44)
app28_in_gga(.(T51, T52), T53, .(T51, X101)) → U2_gga(T51, T52, T53, X101, app28_in_gga(T52, T53, X101))
U2_gga(T51, T52, T53, X101, app28_out_gga(T52, T53, X101)) → app28_out_gga(.(T51, T52), T53, .(T51, X101))
U14_gg(T13, T14, T15, app28_out_gga(T18, T19, X25)) → ss1_out_gg(T13, .(T14, T15))
U13_gg(T13, T14, T15, app18_out_agag(T18, T14, T19, T13)) → U15_gg(T13, T14, T15, app28_in_gga(T18, T19, T37))
U15_gg(T13, T14, T15, app28_out_gga(T18, T19, T37)) → U16_gg(T13, T14, T15, perm38_in_gg(T37, T15))
perm38_in_gg([], []) → perm38_out_gg([], [])
perm38_in_gg(T62, .(T63, T64)) → U3_gg(T62, T63, T64, app18_in_agag(X120, T63, X121, T62))
U3_gg(T62, T63, T64, app18_out_agag(X120, T63, X121, T62)) → perm38_out_gg(T62, .(T63, T64))
perm38_in_gg(T62, .(T63, T64)) → U4_gg(T62, T63, T64, app18_in_agag(T67, T63, T68, T62))
U4_gg(T62, T63, T64, app18_out_agag(T67, T63, T68, T62)) → U5_gg(T62, T63, T64, app28_in_gga(T67, T68, X122))
U5_gg(T62, T63, T64, app28_out_gga(T67, T68, X122)) → perm38_out_gg(T62, .(T63, T64))
U4_gg(T62, T63, T64, app18_out_agag(T67, T63, T68, T62)) → U6_gg(T62, T63, T64, app28_in_gga(T67, T68, T73))
U6_gg(T62, T63, T64, app28_out_gga(T67, T68, T73)) → U7_gg(T62, T63, T64, perm38_in_gg(T73, T64))
U7_gg(T62, T63, T64, perm38_out_gg(T73, T64)) → perm38_out_gg(T62, .(T63, T64))
U16_gg(T13, T14, T15, perm38_out_gg(T37, T15)) → ss1_out_gg(T13, .(T14, T15))
U16_gg(T13, T14, T15, perm38_out_gg(T37, T15)) → U17_gg(T13, T14, T15, ordered39_in_gg(T14, T15))
ordered39_in_gg(T82, []) → ordered39_out_gg(T82, [])
ordered39_in_gg(T89, .(T90, T91)) → U8_gg(T89, T90, T91, less61_in_gg(T89, T90))
less61_in_gg(0, T100) → less61_out_gg(0, T100)
less61_in_gg(s(T105), T106) → U11_gg(T105, T106, less69_in_gg(T105, T106))
less69_in_gg(0, s(T113)) → less69_out_gg(0, s(T113))
less69_in_gg(s(T118), s(T119)) → U10_gg(T118, T119, less69_in_gg(T118, T119))
U10_gg(T118, T119, less69_out_gg(T118, T119)) → less69_out_gg(s(T118), s(T119))
U11_gg(T105, T106, less69_out_gg(T105, T106)) → less61_out_gg(s(T105), T106)
U8_gg(T89, T90, T91, less61_out_gg(T89, T90)) → ordered39_out_gg(T89, .(T90, T91))
U8_gg(T89, T90, T91, less61_out_gg(T89, T90)) → U9_gg(T89, T90, T91, ordered39_in_gg(T90, T91))
U9_gg(T89, T90, T91, ordered39_out_gg(T90, T91)) → ordered39_out_gg(T89, .(T90, T91))
U17_gg(T13, T14, T15, ordered39_out_gg(T14, T15)) → ss1_out_gg(T13, .(T14, T15))

The argument filtering Pi contains the following mapping:
ss1_in_gg(x1, x2)  =  ss1_in_gg(x1, x2)
[]  =  []
ss1_out_gg(x1, x2)  =  ss1_out_gg
.(x1, x2)  =  .(x1, x2)
U12_gg(x1, x2, x3, x4)  =  U12_gg(x4)
app18_in_agag(x1, x2, x3, x4)  =  app18_in_agag(x2, x4)
app18_out_agag(x1, x2, x3, x4)  =  app18_out_agag(x1, x3)
U1_agag(x1, x2, x3, x4, x5, x6)  =  U1_agag(x1, x6)
U13_gg(x1, x2, x3, x4)  =  U13_gg(x2, x3, x4)
U14_gg(x1, x2, x3, x4)  =  U14_gg(x4)
app28_in_gga(x1, x2, x3)  =  app28_in_gga(x1, x2)
app28_out_gga(x1, x2, x3)  =  app28_out_gga(x3)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x5)
U15_gg(x1, x2, x3, x4)  =  U15_gg(x2, x3, x4)
U16_gg(x1, x2, x3, x4)  =  U16_gg(x2, x3, x4)
perm38_in_gg(x1, x2)  =  perm38_in_gg(x1, x2)
perm38_out_gg(x1, x2)  =  perm38_out_gg
U3_gg(x1, x2, x3, x4)  =  U3_gg(x4)
U4_gg(x1, x2, x3, x4)  =  U4_gg(x3, x4)
U5_gg(x1, x2, x3, x4)  =  U5_gg(x4)
U6_gg(x1, x2, x3, x4)  =  U6_gg(x3, x4)
U7_gg(x1, x2, x3, x4)  =  U7_gg(x4)
U17_gg(x1, x2, x3, x4)  =  U17_gg(x4)
ordered39_in_gg(x1, x2)  =  ordered39_in_gg(x1, x2)
ordered39_out_gg(x1, x2)  =  ordered39_out_gg
U8_gg(x1, x2, x3, x4)  =  U8_gg(x2, x3, x4)
less61_in_gg(x1, x2)  =  less61_in_gg(x1, x2)
0  =  0
less61_out_gg(x1, x2)  =  less61_out_gg
s(x1)  =  s(x1)
U11_gg(x1, x2, x3)  =  U11_gg(x3)
less69_in_gg(x1, x2)  =  less69_in_gg(x1, x2)
less69_out_gg(x1, x2)  =  less69_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
U9_gg(x1, x2, x3, x4)  =  U9_gg(x4)
SS1_IN_GG(x1, x2)  =  SS1_IN_GG(x1, x2)
U12_GG(x1, x2, x3, x4)  =  U12_GG(x4)
APP18_IN_AGAG(x1, x2, x3, x4)  =  APP18_IN_AGAG(x2, x4)
U1_AGAG(x1, x2, x3, x4, x5, x6)  =  U1_AGAG(x1, x6)
U13_GG(x1, x2, x3, x4)  =  U13_GG(x2, x3, x4)
U14_GG(x1, x2, x3, x4)  =  U14_GG(x4)
APP28_IN_GGA(x1, x2, x3)  =  APP28_IN_GGA(x1, x2)
U2_GGA(x1, x2, x3, x4, x5)  =  U2_GGA(x1, x5)
U15_GG(x1, x2, x3, x4)  =  U15_GG(x2, x3, x4)
U16_GG(x1, x2, x3, x4)  =  U16_GG(x2, x3, x4)
PERM38_IN_GG(x1, x2)  =  PERM38_IN_GG(x1, x2)
U3_GG(x1, x2, x3, x4)  =  U3_GG(x4)
U4_GG(x1, x2, x3, x4)  =  U4_GG(x3, x4)
U5_GG(x1, x2, x3, x4)  =  U5_GG(x4)
U6_GG(x1, x2, x3, x4)  =  U6_GG(x3, x4)
U7_GG(x1, x2, x3, x4)  =  U7_GG(x4)
U17_GG(x1, x2, x3, x4)  =  U17_GG(x4)
ORDERED39_IN_GG(x1, x2)  =  ORDERED39_IN_GG(x1, x2)
U8_GG(x1, x2, x3, x4)  =  U8_GG(x2, x3, x4)
LESS61_IN_GG(x1, x2)  =  LESS61_IN_GG(x1, x2)
U11_GG(x1, x2, x3)  =  U11_GG(x3)
LESS69_IN_GG(x1, x2)  =  LESS69_IN_GG(x1, x2)
U10_GG(x1, x2, x3)  =  U10_GG(x3)
U9_GG(x1, x2, x3, x4)  =  U9_GG(x4)

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

(6) 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, app18_in_agag(T18, T14, T19, T13))
U13_GG(T13, T14, T15, app18_out_agag(T18, T14, T19, T13)) → U14_GG(T13, T14, T15, app28_in_gga(T18, T19, X25))
U13_GG(T13, T14, T15, app18_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, app18_out_agag(T18, T14, T19, T13)) → U15_GG(T13, T14, T15, app28_in_gga(T18, T19, T37))
U15_GG(T13, T14, T15, app28_out_gga(T18, T19, T37)) → U16_GG(T13, T14, T15, perm38_in_gg(T37, T15))
U15_GG(T13, T14, T15, app28_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, app18_in_agag(T67, T63, T68, T62))
U4_GG(T62, T63, T64, app18_out_agag(T67, T63, T68, T62)) → U5_GG(T62, T63, T64, app28_in_gga(T67, T68, X122))
U4_GG(T62, T63, T64, app18_out_agag(T67, T63, T68, T62)) → APP28_IN_GGA(T67, T68, X122)
U4_GG(T62, T63, T64, app18_out_agag(T67, T63, T68, T62)) → U6_GG(T62, T63, T64, app28_in_gga(T67, T68, T73))
U6_GG(T62, T63, T64, app28_out_gga(T67, T68, T73)) → U7_GG(T62, T63, T64, perm38_in_gg(T73, T64))
U6_GG(T62, T63, T64, app28_out_gga(T67, T68, T73)) → PERM38_IN_GG(T73, T64)
U16_GG(T13, T14, T15, perm38_out_gg(T37, T15)) → U17_GG(T13, T14, T15, ordered39_in_gg(T14, T15))
U16_GG(T13, T14, T15, perm38_out_gg(T37, T15)) → ORDERED39_IN_GG(T14, T15)
ORDERED39_IN_GG(T89, .(T90, T91)) → U8_GG(T89, T90, T91, less61_in_gg(T89, T90))
ORDERED39_IN_GG(T89, .(T90, T91)) → LESS61_IN_GG(T89, T90)
LESS61_IN_GG(s(T105), T106) → U11_GG(T105, T106, less69_in_gg(T105, T106))
LESS61_IN_GG(s(T105), T106) → LESS69_IN_GG(T105, T106)
LESS69_IN_GG(s(T118), s(T119)) → U10_GG(T118, T119, less69_in_gg(T118, T119))
LESS69_IN_GG(s(T118), s(T119)) → LESS69_IN_GG(T118, T119)
U8_GG(T89, T90, T91, less61_out_gg(T89, T90)) → U9_GG(T89, T90, T91, ordered39_in_gg(T90, T91))
U8_GG(T89, T90, T91, less61_out_gg(T89, T90)) → ORDERED39_IN_GG(T90, T91)

The TRS R consists of the following rules:

ss1_in_gg([], []) → ss1_out_gg([], [])
ss1_in_gg(T13, .(T14, T15)) → U12_gg(T13, T14, T15, app18_in_agag(X23, T14, X24, T13))
app18_in_agag([], T26, X46, .(T26, X46)) → app18_out_agag([], T26, X46, .(T26, X46))
app18_in_agag(.(X66, X67), T31, X68, .(X66, T32)) → U1_agag(X66, X67, T31, X68, T32, app18_in_agag(X67, T31, X68, T32))
U1_agag(X66, X67, T31, X68, T32, app18_out_agag(X67, T31, X68, T32)) → app18_out_agag(.(X66, X67), T31, X68, .(X66, T32))
U12_gg(T13, T14, T15, app18_out_agag(X23, T14, X24, T13)) → ss1_out_gg(T13, .(T14, T15))
ss1_in_gg(T13, .(T14, T15)) → U13_gg(T13, T14, T15, app18_in_agag(T18, T14, T19, T13))
U13_gg(T13, T14, T15, app18_out_agag(T18, T14, T19, T13)) → U14_gg(T13, T14, T15, app28_in_gga(T18, T19, X25))
app28_in_gga([], T44, T44) → app28_out_gga([], T44, T44)
app28_in_gga(.(T51, T52), T53, .(T51, X101)) → U2_gga(T51, T52, T53, X101, app28_in_gga(T52, T53, X101))
U2_gga(T51, T52, T53, X101, app28_out_gga(T52, T53, X101)) → app28_out_gga(.(T51, T52), T53, .(T51, X101))
U14_gg(T13, T14, T15, app28_out_gga(T18, T19, X25)) → ss1_out_gg(T13, .(T14, T15))
U13_gg(T13, T14, T15, app18_out_agag(T18, T14, T19, T13)) → U15_gg(T13, T14, T15, app28_in_gga(T18, T19, T37))
U15_gg(T13, T14, T15, app28_out_gga(T18, T19, T37)) → U16_gg(T13, T14, T15, perm38_in_gg(T37, T15))
perm38_in_gg([], []) → perm38_out_gg([], [])
perm38_in_gg(T62, .(T63, T64)) → U3_gg(T62, T63, T64, app18_in_agag(X120, T63, X121, T62))
U3_gg(T62, T63, T64, app18_out_agag(X120, T63, X121, T62)) → perm38_out_gg(T62, .(T63, T64))
perm38_in_gg(T62, .(T63, T64)) → U4_gg(T62, T63, T64, app18_in_agag(T67, T63, T68, T62))
U4_gg(T62, T63, T64, app18_out_agag(T67, T63, T68, T62)) → U5_gg(T62, T63, T64, app28_in_gga(T67, T68, X122))
U5_gg(T62, T63, T64, app28_out_gga(T67, T68, X122)) → perm38_out_gg(T62, .(T63, T64))
U4_gg(T62, T63, T64, app18_out_agag(T67, T63, T68, T62)) → U6_gg(T62, T63, T64, app28_in_gga(T67, T68, T73))
U6_gg(T62, T63, T64, app28_out_gga(T67, T68, T73)) → U7_gg(T62, T63, T64, perm38_in_gg(T73, T64))
U7_gg(T62, T63, T64, perm38_out_gg(T73, T64)) → perm38_out_gg(T62, .(T63, T64))
U16_gg(T13, T14, T15, perm38_out_gg(T37, T15)) → ss1_out_gg(T13, .(T14, T15))
U16_gg(T13, T14, T15, perm38_out_gg(T37, T15)) → U17_gg(T13, T14, T15, ordered39_in_gg(T14, T15))
ordered39_in_gg(T82, []) → ordered39_out_gg(T82, [])
ordered39_in_gg(T89, .(T90, T91)) → U8_gg(T89, T90, T91, less61_in_gg(T89, T90))
less61_in_gg(0, T100) → less61_out_gg(0, T100)
less61_in_gg(s(T105), T106) → U11_gg(T105, T106, less69_in_gg(T105, T106))
less69_in_gg(0, s(T113)) → less69_out_gg(0, s(T113))
less69_in_gg(s(T118), s(T119)) → U10_gg(T118, T119, less69_in_gg(T118, T119))
U10_gg(T118, T119, less69_out_gg(T118, T119)) → less69_out_gg(s(T118), s(T119))
U11_gg(T105, T106, less69_out_gg(T105, T106)) → less61_out_gg(s(T105), T106)
U8_gg(T89, T90, T91, less61_out_gg(T89, T90)) → ordered39_out_gg(T89, .(T90, T91))
U8_gg(T89, T90, T91, less61_out_gg(T89, T90)) → U9_gg(T89, T90, T91, ordered39_in_gg(T90, T91))
U9_gg(T89, T90, T91, ordered39_out_gg(T90, T91)) → ordered39_out_gg(T89, .(T90, T91))
U17_gg(T13, T14, T15, ordered39_out_gg(T14, T15)) → ss1_out_gg(T13, .(T14, T15))

The argument filtering Pi contains the following mapping:
ss1_in_gg(x1, x2)  =  ss1_in_gg(x1, x2)
[]  =  []
ss1_out_gg(x1, x2)  =  ss1_out_gg
.(x1, x2)  =  .(x1, x2)
U12_gg(x1, x2, x3, x4)  =  U12_gg(x4)
app18_in_agag(x1, x2, x3, x4)  =  app18_in_agag(x2, x4)
app18_out_agag(x1, x2, x3, x4)  =  app18_out_agag(x1, x3)
U1_agag(x1, x2, x3, x4, x5, x6)  =  U1_agag(x1, x6)
U13_gg(x1, x2, x3, x4)  =  U13_gg(x2, x3, x4)
U14_gg(x1, x2, x3, x4)  =  U14_gg(x4)
app28_in_gga(x1, x2, x3)  =  app28_in_gga(x1, x2)
app28_out_gga(x1, x2, x3)  =  app28_out_gga(x3)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x5)
U15_gg(x1, x2, x3, x4)  =  U15_gg(x2, x3, x4)
U16_gg(x1, x2, x3, x4)  =  U16_gg(x2, x3, x4)
perm38_in_gg(x1, x2)  =  perm38_in_gg(x1, x2)
perm38_out_gg(x1, x2)  =  perm38_out_gg
U3_gg(x1, x2, x3, x4)  =  U3_gg(x4)
U4_gg(x1, x2, x3, x4)  =  U4_gg(x3, x4)
U5_gg(x1, x2, x3, x4)  =  U5_gg(x4)
U6_gg(x1, x2, x3, x4)  =  U6_gg(x3, x4)
U7_gg(x1, x2, x3, x4)  =  U7_gg(x4)
U17_gg(x1, x2, x3, x4)  =  U17_gg(x4)
ordered39_in_gg(x1, x2)  =  ordered39_in_gg(x1, x2)
ordered39_out_gg(x1, x2)  =  ordered39_out_gg
U8_gg(x1, x2, x3, x4)  =  U8_gg(x2, x3, x4)
less61_in_gg(x1, x2)  =  less61_in_gg(x1, x2)
0  =  0
less61_out_gg(x1, x2)  =  less61_out_gg
s(x1)  =  s(x1)
U11_gg(x1, x2, x3)  =  U11_gg(x3)
less69_in_gg(x1, x2)  =  less69_in_gg(x1, x2)
less69_out_gg(x1, x2)  =  less69_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
U9_gg(x1, x2, x3, x4)  =  U9_gg(x4)
SS1_IN_GG(x1, x2)  =  SS1_IN_GG(x1, x2)
U12_GG(x1, x2, x3, x4)  =  U12_GG(x4)
APP18_IN_AGAG(x1, x2, x3, x4)  =  APP18_IN_AGAG(x2, x4)
U1_AGAG(x1, x2, x3, x4, x5, x6)  =  U1_AGAG(x1, x6)
U13_GG(x1, x2, x3, x4)  =  U13_GG(x2, x3, x4)
U14_GG(x1, x2, x3, x4)  =  U14_GG(x4)
APP28_IN_GGA(x1, x2, x3)  =  APP28_IN_GGA(x1, x2)
U2_GGA(x1, x2, x3, x4, x5)  =  U2_GGA(x1, x5)
U15_GG(x1, x2, x3, x4)  =  U15_GG(x2, x3, x4)
U16_GG(x1, x2, x3, x4)  =  U16_GG(x2, x3, x4)
PERM38_IN_GG(x1, x2)  =  PERM38_IN_GG(x1, x2)
U3_GG(x1, x2, x3, x4)  =  U3_GG(x4)
U4_GG(x1, x2, x3, x4)  =  U4_GG(x3, x4)
U5_GG(x1, x2, x3, x4)  =  U5_GG(x4)
U6_GG(x1, x2, x3, x4)  =  U6_GG(x3, x4)
U7_GG(x1, x2, x3, x4)  =  U7_GG(x4)
U17_GG(x1, x2, x3, x4)  =  U17_GG(x4)
ORDERED39_IN_GG(x1, x2)  =  ORDERED39_IN_GG(x1, x2)
U8_GG(x1, x2, x3, x4)  =  U8_GG(x2, x3, x4)
LESS61_IN_GG(x1, x2)  =  LESS61_IN_GG(x1, x2)
U11_GG(x1, x2, x3)  =  U11_GG(x3)
LESS69_IN_GG(x1, x2)  =  LESS69_IN_GG(x1, x2)
U10_GG(x1, x2, x3)  =  U10_GG(x3)
U9_GG(x1, x2, x3, x4)  =  U9_GG(x4)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

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

(8) Complex Obligation (AND)

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

The TRS R consists of the following rules:

ss1_in_gg([], []) → ss1_out_gg([], [])
ss1_in_gg(T13, .(T14, T15)) → U12_gg(T13, T14, T15, app18_in_agag(X23, T14, X24, T13))
app18_in_agag([], T26, X46, .(T26, X46)) → app18_out_agag([], T26, X46, .(T26, X46))
app18_in_agag(.(X66, X67), T31, X68, .(X66, T32)) → U1_agag(X66, X67, T31, X68, T32, app18_in_agag(X67, T31, X68, T32))
U1_agag(X66, X67, T31, X68, T32, app18_out_agag(X67, T31, X68, T32)) → app18_out_agag(.(X66, X67), T31, X68, .(X66, T32))
U12_gg(T13, T14, T15, app18_out_agag(X23, T14, X24, T13)) → ss1_out_gg(T13, .(T14, T15))
ss1_in_gg(T13, .(T14, T15)) → U13_gg(T13, T14, T15, app18_in_agag(T18, T14, T19, T13))
U13_gg(T13, T14, T15, app18_out_agag(T18, T14, T19, T13)) → U14_gg(T13, T14, T15, app28_in_gga(T18, T19, X25))
app28_in_gga([], T44, T44) → app28_out_gga([], T44, T44)
app28_in_gga(.(T51, T52), T53, .(T51, X101)) → U2_gga(T51, T52, T53, X101, app28_in_gga(T52, T53, X101))
U2_gga(T51, T52, T53, X101, app28_out_gga(T52, T53, X101)) → app28_out_gga(.(T51, T52), T53, .(T51, X101))
U14_gg(T13, T14, T15, app28_out_gga(T18, T19, X25)) → ss1_out_gg(T13, .(T14, T15))
U13_gg(T13, T14, T15, app18_out_agag(T18, T14, T19, T13)) → U15_gg(T13, T14, T15, app28_in_gga(T18, T19, T37))
U15_gg(T13, T14, T15, app28_out_gga(T18, T19, T37)) → U16_gg(T13, T14, T15, perm38_in_gg(T37, T15))
perm38_in_gg([], []) → perm38_out_gg([], [])
perm38_in_gg(T62, .(T63, T64)) → U3_gg(T62, T63, T64, app18_in_agag(X120, T63, X121, T62))
U3_gg(T62, T63, T64, app18_out_agag(X120, T63, X121, T62)) → perm38_out_gg(T62, .(T63, T64))
perm38_in_gg(T62, .(T63, T64)) → U4_gg(T62, T63, T64, app18_in_agag(T67, T63, T68, T62))
U4_gg(T62, T63, T64, app18_out_agag(T67, T63, T68, T62)) → U5_gg(T62, T63, T64, app28_in_gga(T67, T68, X122))
U5_gg(T62, T63, T64, app28_out_gga(T67, T68, X122)) → perm38_out_gg(T62, .(T63, T64))
U4_gg(T62, T63, T64, app18_out_agag(T67, T63, T68, T62)) → U6_gg(T62, T63, T64, app28_in_gga(T67, T68, T73))
U6_gg(T62, T63, T64, app28_out_gga(T67, T68, T73)) → U7_gg(T62, T63, T64, perm38_in_gg(T73, T64))
U7_gg(T62, T63, T64, perm38_out_gg(T73, T64)) → perm38_out_gg(T62, .(T63, T64))
U16_gg(T13, T14, T15, perm38_out_gg(T37, T15)) → ss1_out_gg(T13, .(T14, T15))
U16_gg(T13, T14, T15, perm38_out_gg(T37, T15)) → U17_gg(T13, T14, T15, ordered39_in_gg(T14, T15))
ordered39_in_gg(T82, []) → ordered39_out_gg(T82, [])
ordered39_in_gg(T89, .(T90, T91)) → U8_gg(T89, T90, T91, less61_in_gg(T89, T90))
less61_in_gg(0, T100) → less61_out_gg(0, T100)
less61_in_gg(s(T105), T106) → U11_gg(T105, T106, less69_in_gg(T105, T106))
less69_in_gg(0, s(T113)) → less69_out_gg(0, s(T113))
less69_in_gg(s(T118), s(T119)) → U10_gg(T118, T119, less69_in_gg(T118, T119))
U10_gg(T118, T119, less69_out_gg(T118, T119)) → less69_out_gg(s(T118), s(T119))
U11_gg(T105, T106, less69_out_gg(T105, T106)) → less61_out_gg(s(T105), T106)
U8_gg(T89, T90, T91, less61_out_gg(T89, T90)) → ordered39_out_gg(T89, .(T90, T91))
U8_gg(T89, T90, T91, less61_out_gg(T89, T90)) → U9_gg(T89, T90, T91, ordered39_in_gg(T90, T91))
U9_gg(T89, T90, T91, ordered39_out_gg(T90, T91)) → ordered39_out_gg(T89, .(T90, T91))
U17_gg(T13, T14, T15, ordered39_out_gg(T14, T15)) → ss1_out_gg(T13, .(T14, T15))

The argument filtering Pi contains the following mapping:
ss1_in_gg(x1, x2)  =  ss1_in_gg(x1, x2)
[]  =  []
ss1_out_gg(x1, x2)  =  ss1_out_gg
.(x1, x2)  =  .(x1, x2)
U12_gg(x1, x2, x3, x4)  =  U12_gg(x4)
app18_in_agag(x1, x2, x3, x4)  =  app18_in_agag(x2, x4)
app18_out_agag(x1, x2, x3, x4)  =  app18_out_agag(x1, x3)
U1_agag(x1, x2, x3, x4, x5, x6)  =  U1_agag(x1, x6)
U13_gg(x1, x2, x3, x4)  =  U13_gg(x2, x3, x4)
U14_gg(x1, x2, x3, x4)  =  U14_gg(x4)
app28_in_gga(x1, x2, x3)  =  app28_in_gga(x1, x2)
app28_out_gga(x1, x2, x3)  =  app28_out_gga(x3)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x5)
U15_gg(x1, x2, x3, x4)  =  U15_gg(x2, x3, x4)
U16_gg(x1, x2, x3, x4)  =  U16_gg(x2, x3, x4)
perm38_in_gg(x1, x2)  =  perm38_in_gg(x1, x2)
perm38_out_gg(x1, x2)  =  perm38_out_gg
U3_gg(x1, x2, x3, x4)  =  U3_gg(x4)
U4_gg(x1, x2, x3, x4)  =  U4_gg(x3, x4)
U5_gg(x1, x2, x3, x4)  =  U5_gg(x4)
U6_gg(x1, x2, x3, x4)  =  U6_gg(x3, x4)
U7_gg(x1, x2, x3, x4)  =  U7_gg(x4)
U17_gg(x1, x2, x3, x4)  =  U17_gg(x4)
ordered39_in_gg(x1, x2)  =  ordered39_in_gg(x1, x2)
ordered39_out_gg(x1, x2)  =  ordered39_out_gg
U8_gg(x1, x2, x3, x4)  =  U8_gg(x2, x3, x4)
less61_in_gg(x1, x2)  =  less61_in_gg(x1, x2)
0  =  0
less61_out_gg(x1, x2)  =  less61_out_gg
s(x1)  =  s(x1)
U11_gg(x1, x2, x3)  =  U11_gg(x3)
less69_in_gg(x1, x2)  =  less69_in_gg(x1, x2)
less69_out_gg(x1, x2)  =  less69_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
U9_gg(x1, x2, x3, x4)  =  U9_gg(x4)
LESS69_IN_GG(x1, x2)  =  LESS69_IN_GG(x1, x2)

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

(10) UsableRulesProof (EQUIVALENT transformation)

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

(11) 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

(12) PiDPToQDPProof (EQUIVALENT transformation)

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

(13) 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.

(14) 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

(15) YES

(16) Obligation:

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

U8_GG(T89, T90, T91, less61_out_gg(T89, T90)) → ORDERED39_IN_GG(T90, T91)
ORDERED39_IN_GG(T89, .(T90, T91)) → U8_GG(T89, T90, T91, less61_in_gg(T89, T90))

The TRS R consists of the following rules:

ss1_in_gg([], []) → ss1_out_gg([], [])
ss1_in_gg(T13, .(T14, T15)) → U12_gg(T13, T14, T15, app18_in_agag(X23, T14, X24, T13))
app18_in_agag([], T26, X46, .(T26, X46)) → app18_out_agag([], T26, X46, .(T26, X46))
app18_in_agag(.(X66, X67), T31, X68, .(X66, T32)) → U1_agag(X66, X67, T31, X68, T32, app18_in_agag(X67, T31, X68, T32))
U1_agag(X66, X67, T31, X68, T32, app18_out_agag(X67, T31, X68, T32)) → app18_out_agag(.(X66, X67), T31, X68, .(X66, T32))
U12_gg(T13, T14, T15, app18_out_agag(X23, T14, X24, T13)) → ss1_out_gg(T13, .(T14, T15))
ss1_in_gg(T13, .(T14, T15)) → U13_gg(T13, T14, T15, app18_in_agag(T18, T14, T19, T13))
U13_gg(T13, T14, T15, app18_out_agag(T18, T14, T19, T13)) → U14_gg(T13, T14, T15, app28_in_gga(T18, T19, X25))
app28_in_gga([], T44, T44) → app28_out_gga([], T44, T44)
app28_in_gga(.(T51, T52), T53, .(T51, X101)) → U2_gga(T51, T52, T53, X101, app28_in_gga(T52, T53, X101))
U2_gga(T51, T52, T53, X101, app28_out_gga(T52, T53, X101)) → app28_out_gga(.(T51, T52), T53, .(T51, X101))
U14_gg(T13, T14, T15, app28_out_gga(T18, T19, X25)) → ss1_out_gg(T13, .(T14, T15))
U13_gg(T13, T14, T15, app18_out_agag(T18, T14, T19, T13)) → U15_gg(T13, T14, T15, app28_in_gga(T18, T19, T37))
U15_gg(T13, T14, T15, app28_out_gga(T18, T19, T37)) → U16_gg(T13, T14, T15, perm38_in_gg(T37, T15))
perm38_in_gg([], []) → perm38_out_gg([], [])
perm38_in_gg(T62, .(T63, T64)) → U3_gg(T62, T63, T64, app18_in_agag(X120, T63, X121, T62))
U3_gg(T62, T63, T64, app18_out_agag(X120, T63, X121, T62)) → perm38_out_gg(T62, .(T63, T64))
perm38_in_gg(T62, .(T63, T64)) → U4_gg(T62, T63, T64, app18_in_agag(T67, T63, T68, T62))
U4_gg(T62, T63, T64, app18_out_agag(T67, T63, T68, T62)) → U5_gg(T62, T63, T64, app28_in_gga(T67, T68, X122))
U5_gg(T62, T63, T64, app28_out_gga(T67, T68, X122)) → perm38_out_gg(T62, .(T63, T64))
U4_gg(T62, T63, T64, app18_out_agag(T67, T63, T68, T62)) → U6_gg(T62, T63, T64, app28_in_gga(T67, T68, T73))
U6_gg(T62, T63, T64, app28_out_gga(T67, T68, T73)) → U7_gg(T62, T63, T64, perm38_in_gg(T73, T64))
U7_gg(T62, T63, T64, perm38_out_gg(T73, T64)) → perm38_out_gg(T62, .(T63, T64))
U16_gg(T13, T14, T15, perm38_out_gg(T37, T15)) → ss1_out_gg(T13, .(T14, T15))
U16_gg(T13, T14, T15, perm38_out_gg(T37, T15)) → U17_gg(T13, T14, T15, ordered39_in_gg(T14, T15))
ordered39_in_gg(T82, []) → ordered39_out_gg(T82, [])
ordered39_in_gg(T89, .(T90, T91)) → U8_gg(T89, T90, T91, less61_in_gg(T89, T90))
less61_in_gg(0, T100) → less61_out_gg(0, T100)
less61_in_gg(s(T105), T106) → U11_gg(T105, T106, less69_in_gg(T105, T106))
less69_in_gg(0, s(T113)) → less69_out_gg(0, s(T113))
less69_in_gg(s(T118), s(T119)) → U10_gg(T118, T119, less69_in_gg(T118, T119))
U10_gg(T118, T119, less69_out_gg(T118, T119)) → less69_out_gg(s(T118), s(T119))
U11_gg(T105, T106, less69_out_gg(T105, T106)) → less61_out_gg(s(T105), T106)
U8_gg(T89, T90, T91, less61_out_gg(T89, T90)) → ordered39_out_gg(T89, .(T90, T91))
U8_gg(T89, T90, T91, less61_out_gg(T89, T90)) → U9_gg(T89, T90, T91, ordered39_in_gg(T90, T91))
U9_gg(T89, T90, T91, ordered39_out_gg(T90, T91)) → ordered39_out_gg(T89, .(T90, T91))
U17_gg(T13, T14, T15, ordered39_out_gg(T14, T15)) → ss1_out_gg(T13, .(T14, T15))

The argument filtering Pi contains the following mapping:
ss1_in_gg(x1, x2)  =  ss1_in_gg(x1, x2)
[]  =  []
ss1_out_gg(x1, x2)  =  ss1_out_gg
.(x1, x2)  =  .(x1, x2)
U12_gg(x1, x2, x3, x4)  =  U12_gg(x4)
app18_in_agag(x1, x2, x3, x4)  =  app18_in_agag(x2, x4)
app18_out_agag(x1, x2, x3, x4)  =  app18_out_agag(x1, x3)
U1_agag(x1, x2, x3, x4, x5, x6)  =  U1_agag(x1, x6)
U13_gg(x1, x2, x3, x4)  =  U13_gg(x2, x3, x4)
U14_gg(x1, x2, x3, x4)  =  U14_gg(x4)
app28_in_gga(x1, x2, x3)  =  app28_in_gga(x1, x2)
app28_out_gga(x1, x2, x3)  =  app28_out_gga(x3)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x5)
U15_gg(x1, x2, x3, x4)  =  U15_gg(x2, x3, x4)
U16_gg(x1, x2, x3, x4)  =  U16_gg(x2, x3, x4)
perm38_in_gg(x1, x2)  =  perm38_in_gg(x1, x2)
perm38_out_gg(x1, x2)  =  perm38_out_gg
U3_gg(x1, x2, x3, x4)  =  U3_gg(x4)
U4_gg(x1, x2, x3, x4)  =  U4_gg(x3, x4)
U5_gg(x1, x2, x3, x4)  =  U5_gg(x4)
U6_gg(x1, x2, x3, x4)  =  U6_gg(x3, x4)
U7_gg(x1, x2, x3, x4)  =  U7_gg(x4)
U17_gg(x1, x2, x3, x4)  =  U17_gg(x4)
ordered39_in_gg(x1, x2)  =  ordered39_in_gg(x1, x2)
ordered39_out_gg(x1, x2)  =  ordered39_out_gg
U8_gg(x1, x2, x3, x4)  =  U8_gg(x2, x3, x4)
less61_in_gg(x1, x2)  =  less61_in_gg(x1, x2)
0  =  0
less61_out_gg(x1, x2)  =  less61_out_gg
s(x1)  =  s(x1)
U11_gg(x1, x2, x3)  =  U11_gg(x3)
less69_in_gg(x1, x2)  =  less69_in_gg(x1, x2)
less69_out_gg(x1, x2)  =  less69_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
U9_gg(x1, x2, x3, x4)  =  U9_gg(x4)
ORDERED39_IN_GG(x1, x2)  =  ORDERED39_IN_GG(x1, x2)
U8_GG(x1, x2, x3, x4)  =  U8_GG(x2, x3, x4)

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

(17) UsableRulesProof (EQUIVALENT transformation)

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

(18) Obligation:

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

U8_GG(T89, T90, T91, less61_out_gg(T89, T90)) → ORDERED39_IN_GG(T90, T91)
ORDERED39_IN_GG(T89, .(T90, T91)) → U8_GG(T89, T90, T91, less61_in_gg(T89, T90))

The TRS R consists of the following rules:

less61_in_gg(0, T100) → less61_out_gg(0, T100)
less61_in_gg(s(T105), T106) → U11_gg(T105, T106, less69_in_gg(T105, T106))
U11_gg(T105, T106, less69_out_gg(T105, T106)) → less61_out_gg(s(T105), T106)
less69_in_gg(0, s(T113)) → less69_out_gg(0, s(T113))
less69_in_gg(s(T118), s(T119)) → U10_gg(T118, T119, less69_in_gg(T118, T119))
U10_gg(T118, T119, less69_out_gg(T118, T119)) → less69_out_gg(s(T118), s(T119))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
less61_in_gg(x1, x2)  =  less61_in_gg(x1, x2)
0  =  0
less61_out_gg(x1, x2)  =  less61_out_gg
s(x1)  =  s(x1)
U11_gg(x1, x2, x3)  =  U11_gg(x3)
less69_in_gg(x1, x2)  =  less69_in_gg(x1, x2)
less69_out_gg(x1, x2)  =  less69_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
ORDERED39_IN_GG(x1, x2)  =  ORDERED39_IN_GG(x1, x2)
U8_GG(x1, x2, x3, x4)  =  U8_GG(x2, x3, x4)

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

(19) PiDPToQDPProof (SOUND transformation)

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

(20) Obligation:

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

U8_GG(T90, T91, less61_out_gg) → ORDERED39_IN_GG(T90, T91)
ORDERED39_IN_GG(T89, .(T90, T91)) → U8_GG(T90, T91, less61_in_gg(T89, T90))

The TRS R consists of the following rules:

less61_in_gg(0, T100) → less61_out_gg
less61_in_gg(s(T105), T106) → U11_gg(less69_in_gg(T105, T106))
U11_gg(less69_out_gg) → less61_out_gg
less69_in_gg(0, s(T113)) → less69_out_gg
less69_in_gg(s(T118), s(T119)) → U10_gg(less69_in_gg(T118, T119))
U10_gg(less69_out_gg) → less69_out_gg

The set Q consists of the following terms:

less61_in_gg(x0, x1)
U11_gg(x0)
less69_in_gg(x0, x1)
U10_gg(x0)

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

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

  • ORDERED39_IN_GG(T89, .(T90, T91)) → U8_GG(T90, T91, less61_in_gg(T89, T90))
    The graph contains the following edges 2 > 1, 2 > 2

  • U8_GG(T90, T91, less61_out_gg) → ORDERED39_IN_GG(T90, T91)
    The graph contains the following edges 1 >= 1, 2 >= 2

(22) YES

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

The TRS R consists of the following rules:

ss1_in_gg([], []) → ss1_out_gg([], [])
ss1_in_gg(T13, .(T14, T15)) → U12_gg(T13, T14, T15, app18_in_agag(X23, T14, X24, T13))
app18_in_agag([], T26, X46, .(T26, X46)) → app18_out_agag([], T26, X46, .(T26, X46))
app18_in_agag(.(X66, X67), T31, X68, .(X66, T32)) → U1_agag(X66, X67, T31, X68, T32, app18_in_agag(X67, T31, X68, T32))
U1_agag(X66, X67, T31, X68, T32, app18_out_agag(X67, T31, X68, T32)) → app18_out_agag(.(X66, X67), T31, X68, .(X66, T32))
U12_gg(T13, T14, T15, app18_out_agag(X23, T14, X24, T13)) → ss1_out_gg(T13, .(T14, T15))
ss1_in_gg(T13, .(T14, T15)) → U13_gg(T13, T14, T15, app18_in_agag(T18, T14, T19, T13))
U13_gg(T13, T14, T15, app18_out_agag(T18, T14, T19, T13)) → U14_gg(T13, T14, T15, app28_in_gga(T18, T19, X25))
app28_in_gga([], T44, T44) → app28_out_gga([], T44, T44)
app28_in_gga(.(T51, T52), T53, .(T51, X101)) → U2_gga(T51, T52, T53, X101, app28_in_gga(T52, T53, X101))
U2_gga(T51, T52, T53, X101, app28_out_gga(T52, T53, X101)) → app28_out_gga(.(T51, T52), T53, .(T51, X101))
U14_gg(T13, T14, T15, app28_out_gga(T18, T19, X25)) → ss1_out_gg(T13, .(T14, T15))
U13_gg(T13, T14, T15, app18_out_agag(T18, T14, T19, T13)) → U15_gg(T13, T14, T15, app28_in_gga(T18, T19, T37))
U15_gg(T13, T14, T15, app28_out_gga(T18, T19, T37)) → U16_gg(T13, T14, T15, perm38_in_gg(T37, T15))
perm38_in_gg([], []) → perm38_out_gg([], [])
perm38_in_gg(T62, .(T63, T64)) → U3_gg(T62, T63, T64, app18_in_agag(X120, T63, X121, T62))
U3_gg(T62, T63, T64, app18_out_agag(X120, T63, X121, T62)) → perm38_out_gg(T62, .(T63, T64))
perm38_in_gg(T62, .(T63, T64)) → U4_gg(T62, T63, T64, app18_in_agag(T67, T63, T68, T62))
U4_gg(T62, T63, T64, app18_out_agag(T67, T63, T68, T62)) → U5_gg(T62, T63, T64, app28_in_gga(T67, T68, X122))
U5_gg(T62, T63, T64, app28_out_gga(T67, T68, X122)) → perm38_out_gg(T62, .(T63, T64))
U4_gg(T62, T63, T64, app18_out_agag(T67, T63, T68, T62)) → U6_gg(T62, T63, T64, app28_in_gga(T67, T68, T73))
U6_gg(T62, T63, T64, app28_out_gga(T67, T68, T73)) → U7_gg(T62, T63, T64, perm38_in_gg(T73, T64))
U7_gg(T62, T63, T64, perm38_out_gg(T73, T64)) → perm38_out_gg(T62, .(T63, T64))
U16_gg(T13, T14, T15, perm38_out_gg(T37, T15)) → ss1_out_gg(T13, .(T14, T15))
U16_gg(T13, T14, T15, perm38_out_gg(T37, T15)) → U17_gg(T13, T14, T15, ordered39_in_gg(T14, T15))
ordered39_in_gg(T82, []) → ordered39_out_gg(T82, [])
ordered39_in_gg(T89, .(T90, T91)) → U8_gg(T89, T90, T91, less61_in_gg(T89, T90))
less61_in_gg(0, T100) → less61_out_gg(0, T100)
less61_in_gg(s(T105), T106) → U11_gg(T105, T106, less69_in_gg(T105, T106))
less69_in_gg(0, s(T113)) → less69_out_gg(0, s(T113))
less69_in_gg(s(T118), s(T119)) → U10_gg(T118, T119, less69_in_gg(T118, T119))
U10_gg(T118, T119, less69_out_gg(T118, T119)) → less69_out_gg(s(T118), s(T119))
U11_gg(T105, T106, less69_out_gg(T105, T106)) → less61_out_gg(s(T105), T106)
U8_gg(T89, T90, T91, less61_out_gg(T89, T90)) → ordered39_out_gg(T89, .(T90, T91))
U8_gg(T89, T90, T91, less61_out_gg(T89, T90)) → U9_gg(T89, T90, T91, ordered39_in_gg(T90, T91))
U9_gg(T89, T90, T91, ordered39_out_gg(T90, T91)) → ordered39_out_gg(T89, .(T90, T91))
U17_gg(T13, T14, T15, ordered39_out_gg(T14, T15)) → ss1_out_gg(T13, .(T14, T15))

The argument filtering Pi contains the following mapping:
ss1_in_gg(x1, x2)  =  ss1_in_gg(x1, x2)
[]  =  []
ss1_out_gg(x1, x2)  =  ss1_out_gg
.(x1, x2)  =  .(x1, x2)
U12_gg(x1, x2, x3, x4)  =  U12_gg(x4)
app18_in_agag(x1, x2, x3, x4)  =  app18_in_agag(x2, x4)
app18_out_agag(x1, x2, x3, x4)  =  app18_out_agag(x1, x3)
U1_agag(x1, x2, x3, x4, x5, x6)  =  U1_agag(x1, x6)
U13_gg(x1, x2, x3, x4)  =  U13_gg(x2, x3, x4)
U14_gg(x1, x2, x3, x4)  =  U14_gg(x4)
app28_in_gga(x1, x2, x3)  =  app28_in_gga(x1, x2)
app28_out_gga(x1, x2, x3)  =  app28_out_gga(x3)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x5)
U15_gg(x1, x2, x3, x4)  =  U15_gg(x2, x3, x4)
U16_gg(x1, x2, x3, x4)  =  U16_gg(x2, x3, x4)
perm38_in_gg(x1, x2)  =  perm38_in_gg(x1, x2)
perm38_out_gg(x1, x2)  =  perm38_out_gg
U3_gg(x1, x2, x3, x4)  =  U3_gg(x4)
U4_gg(x1, x2, x3, x4)  =  U4_gg(x3, x4)
U5_gg(x1, x2, x3, x4)  =  U5_gg(x4)
U6_gg(x1, x2, x3, x4)  =  U6_gg(x3, x4)
U7_gg(x1, x2, x3, x4)  =  U7_gg(x4)
U17_gg(x1, x2, x3, x4)  =  U17_gg(x4)
ordered39_in_gg(x1, x2)  =  ordered39_in_gg(x1, x2)
ordered39_out_gg(x1, x2)  =  ordered39_out_gg
U8_gg(x1, x2, x3, x4)  =  U8_gg(x2, x3, x4)
less61_in_gg(x1, x2)  =  less61_in_gg(x1, x2)
0  =  0
less61_out_gg(x1, x2)  =  less61_out_gg
s(x1)  =  s(x1)
U11_gg(x1, x2, x3)  =  U11_gg(x3)
less69_in_gg(x1, x2)  =  less69_in_gg(x1, x2)
less69_out_gg(x1, x2)  =  less69_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
U9_gg(x1, x2, x3, x4)  =  U9_gg(x4)
APP28_IN_GGA(x1, x2, x3)  =  APP28_IN_GGA(x1, x2)

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

(24) UsableRulesProof (EQUIVALENT transformation)

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

(25) 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

(26) PiDPToQDPProof (SOUND transformation)

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

(27) 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.

(28) 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

(29) YES

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

The TRS R consists of the following rules:

ss1_in_gg([], []) → ss1_out_gg([], [])
ss1_in_gg(T13, .(T14, T15)) → U12_gg(T13, T14, T15, app18_in_agag(X23, T14, X24, T13))
app18_in_agag([], T26, X46, .(T26, X46)) → app18_out_agag([], T26, X46, .(T26, X46))
app18_in_agag(.(X66, X67), T31, X68, .(X66, T32)) → U1_agag(X66, X67, T31, X68, T32, app18_in_agag(X67, T31, X68, T32))
U1_agag(X66, X67, T31, X68, T32, app18_out_agag(X67, T31, X68, T32)) → app18_out_agag(.(X66, X67), T31, X68, .(X66, T32))
U12_gg(T13, T14, T15, app18_out_agag(X23, T14, X24, T13)) → ss1_out_gg(T13, .(T14, T15))
ss1_in_gg(T13, .(T14, T15)) → U13_gg(T13, T14, T15, app18_in_agag(T18, T14, T19, T13))
U13_gg(T13, T14, T15, app18_out_agag(T18, T14, T19, T13)) → U14_gg(T13, T14, T15, app28_in_gga(T18, T19, X25))
app28_in_gga([], T44, T44) → app28_out_gga([], T44, T44)
app28_in_gga(.(T51, T52), T53, .(T51, X101)) → U2_gga(T51, T52, T53, X101, app28_in_gga(T52, T53, X101))
U2_gga(T51, T52, T53, X101, app28_out_gga(T52, T53, X101)) → app28_out_gga(.(T51, T52), T53, .(T51, X101))
U14_gg(T13, T14, T15, app28_out_gga(T18, T19, X25)) → ss1_out_gg(T13, .(T14, T15))
U13_gg(T13, T14, T15, app18_out_agag(T18, T14, T19, T13)) → U15_gg(T13, T14, T15, app28_in_gga(T18, T19, T37))
U15_gg(T13, T14, T15, app28_out_gga(T18, T19, T37)) → U16_gg(T13, T14, T15, perm38_in_gg(T37, T15))
perm38_in_gg([], []) → perm38_out_gg([], [])
perm38_in_gg(T62, .(T63, T64)) → U3_gg(T62, T63, T64, app18_in_agag(X120, T63, X121, T62))
U3_gg(T62, T63, T64, app18_out_agag(X120, T63, X121, T62)) → perm38_out_gg(T62, .(T63, T64))
perm38_in_gg(T62, .(T63, T64)) → U4_gg(T62, T63, T64, app18_in_agag(T67, T63, T68, T62))
U4_gg(T62, T63, T64, app18_out_agag(T67, T63, T68, T62)) → U5_gg(T62, T63, T64, app28_in_gga(T67, T68, X122))
U5_gg(T62, T63, T64, app28_out_gga(T67, T68, X122)) → perm38_out_gg(T62, .(T63, T64))
U4_gg(T62, T63, T64, app18_out_agag(T67, T63, T68, T62)) → U6_gg(T62, T63, T64, app28_in_gga(T67, T68, T73))
U6_gg(T62, T63, T64, app28_out_gga(T67, T68, T73)) → U7_gg(T62, T63, T64, perm38_in_gg(T73, T64))
U7_gg(T62, T63, T64, perm38_out_gg(T73, T64)) → perm38_out_gg(T62, .(T63, T64))
U16_gg(T13, T14, T15, perm38_out_gg(T37, T15)) → ss1_out_gg(T13, .(T14, T15))
U16_gg(T13, T14, T15, perm38_out_gg(T37, T15)) → U17_gg(T13, T14, T15, ordered39_in_gg(T14, T15))
ordered39_in_gg(T82, []) → ordered39_out_gg(T82, [])
ordered39_in_gg(T89, .(T90, T91)) → U8_gg(T89, T90, T91, less61_in_gg(T89, T90))
less61_in_gg(0, T100) → less61_out_gg(0, T100)
less61_in_gg(s(T105), T106) → U11_gg(T105, T106, less69_in_gg(T105, T106))
less69_in_gg(0, s(T113)) → less69_out_gg(0, s(T113))
less69_in_gg(s(T118), s(T119)) → U10_gg(T118, T119, less69_in_gg(T118, T119))
U10_gg(T118, T119, less69_out_gg(T118, T119)) → less69_out_gg(s(T118), s(T119))
U11_gg(T105, T106, less69_out_gg(T105, T106)) → less61_out_gg(s(T105), T106)
U8_gg(T89, T90, T91, less61_out_gg(T89, T90)) → ordered39_out_gg(T89, .(T90, T91))
U8_gg(T89, T90, T91, less61_out_gg(T89, T90)) → U9_gg(T89, T90, T91, ordered39_in_gg(T90, T91))
U9_gg(T89, T90, T91, ordered39_out_gg(T90, T91)) → ordered39_out_gg(T89, .(T90, T91))
U17_gg(T13, T14, T15, ordered39_out_gg(T14, T15)) → ss1_out_gg(T13, .(T14, T15))

The argument filtering Pi contains the following mapping:
ss1_in_gg(x1, x2)  =  ss1_in_gg(x1, x2)
[]  =  []
ss1_out_gg(x1, x2)  =  ss1_out_gg
.(x1, x2)  =  .(x1, x2)
U12_gg(x1, x2, x3, x4)  =  U12_gg(x4)
app18_in_agag(x1, x2, x3, x4)  =  app18_in_agag(x2, x4)
app18_out_agag(x1, x2, x3, x4)  =  app18_out_agag(x1, x3)
U1_agag(x1, x2, x3, x4, x5, x6)  =  U1_agag(x1, x6)
U13_gg(x1, x2, x3, x4)  =  U13_gg(x2, x3, x4)
U14_gg(x1, x2, x3, x4)  =  U14_gg(x4)
app28_in_gga(x1, x2, x3)  =  app28_in_gga(x1, x2)
app28_out_gga(x1, x2, x3)  =  app28_out_gga(x3)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x5)
U15_gg(x1, x2, x3, x4)  =  U15_gg(x2, x3, x4)
U16_gg(x1, x2, x3, x4)  =  U16_gg(x2, x3, x4)
perm38_in_gg(x1, x2)  =  perm38_in_gg(x1, x2)
perm38_out_gg(x1, x2)  =  perm38_out_gg
U3_gg(x1, x2, x3, x4)  =  U3_gg(x4)
U4_gg(x1, x2, x3, x4)  =  U4_gg(x3, x4)
U5_gg(x1, x2, x3, x4)  =  U5_gg(x4)
U6_gg(x1, x2, x3, x4)  =  U6_gg(x3, x4)
U7_gg(x1, x2, x3, x4)  =  U7_gg(x4)
U17_gg(x1, x2, x3, x4)  =  U17_gg(x4)
ordered39_in_gg(x1, x2)  =  ordered39_in_gg(x1, x2)
ordered39_out_gg(x1, x2)  =  ordered39_out_gg
U8_gg(x1, x2, x3, x4)  =  U8_gg(x2, x3, x4)
less61_in_gg(x1, x2)  =  less61_in_gg(x1, x2)
0  =  0
less61_out_gg(x1, x2)  =  less61_out_gg
s(x1)  =  s(x1)
U11_gg(x1, x2, x3)  =  U11_gg(x3)
less69_in_gg(x1, x2)  =  less69_in_gg(x1, x2)
less69_out_gg(x1, x2)  =  less69_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
U9_gg(x1, x2, x3, x4)  =  U9_gg(x4)
APP18_IN_AGAG(x1, x2, x3, x4)  =  APP18_IN_AGAG(x2, x4)

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

(31) UsableRulesProof (EQUIVALENT transformation)

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

(32) 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

(33) PiDPToQDPProof (SOUND transformation)

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

(34) 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.

(35) 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

(36) YES

(37) Obligation:

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

PERM38_IN_GG(T62, .(T63, T64)) → U4_GG(T62, T63, T64, app18_in_agag(T67, T63, T68, T62))
U4_GG(T62, T63, T64, app18_out_agag(T67, T63, T68, T62)) → U6_GG(T62, T63, T64, app28_in_gga(T67, T68, T73))
U6_GG(T62, T63, T64, app28_out_gga(T67, T68, T73)) → PERM38_IN_GG(T73, T64)

The TRS R consists of the following rules:

ss1_in_gg([], []) → ss1_out_gg([], [])
ss1_in_gg(T13, .(T14, T15)) → U12_gg(T13, T14, T15, app18_in_agag(X23, T14, X24, T13))
app18_in_agag([], T26, X46, .(T26, X46)) → app18_out_agag([], T26, X46, .(T26, X46))
app18_in_agag(.(X66, X67), T31, X68, .(X66, T32)) → U1_agag(X66, X67, T31, X68, T32, app18_in_agag(X67, T31, X68, T32))
U1_agag(X66, X67, T31, X68, T32, app18_out_agag(X67, T31, X68, T32)) → app18_out_agag(.(X66, X67), T31, X68, .(X66, T32))
U12_gg(T13, T14, T15, app18_out_agag(X23, T14, X24, T13)) → ss1_out_gg(T13, .(T14, T15))
ss1_in_gg(T13, .(T14, T15)) → U13_gg(T13, T14, T15, app18_in_agag(T18, T14, T19, T13))
U13_gg(T13, T14, T15, app18_out_agag(T18, T14, T19, T13)) → U14_gg(T13, T14, T15, app28_in_gga(T18, T19, X25))
app28_in_gga([], T44, T44) → app28_out_gga([], T44, T44)
app28_in_gga(.(T51, T52), T53, .(T51, X101)) → U2_gga(T51, T52, T53, X101, app28_in_gga(T52, T53, X101))
U2_gga(T51, T52, T53, X101, app28_out_gga(T52, T53, X101)) → app28_out_gga(.(T51, T52), T53, .(T51, X101))
U14_gg(T13, T14, T15, app28_out_gga(T18, T19, X25)) → ss1_out_gg(T13, .(T14, T15))
U13_gg(T13, T14, T15, app18_out_agag(T18, T14, T19, T13)) → U15_gg(T13, T14, T15, app28_in_gga(T18, T19, T37))
U15_gg(T13, T14, T15, app28_out_gga(T18, T19, T37)) → U16_gg(T13, T14, T15, perm38_in_gg(T37, T15))
perm38_in_gg([], []) → perm38_out_gg([], [])
perm38_in_gg(T62, .(T63, T64)) → U3_gg(T62, T63, T64, app18_in_agag(X120, T63, X121, T62))
U3_gg(T62, T63, T64, app18_out_agag(X120, T63, X121, T62)) → perm38_out_gg(T62, .(T63, T64))
perm38_in_gg(T62, .(T63, T64)) → U4_gg(T62, T63, T64, app18_in_agag(T67, T63, T68, T62))
U4_gg(T62, T63, T64, app18_out_agag(T67, T63, T68, T62)) → U5_gg(T62, T63, T64, app28_in_gga(T67, T68, X122))
U5_gg(T62, T63, T64, app28_out_gga(T67, T68, X122)) → perm38_out_gg(T62, .(T63, T64))
U4_gg(T62, T63, T64, app18_out_agag(T67, T63, T68, T62)) → U6_gg(T62, T63, T64, app28_in_gga(T67, T68, T73))
U6_gg(T62, T63, T64, app28_out_gga(T67, T68, T73)) → U7_gg(T62, T63, T64, perm38_in_gg(T73, T64))
U7_gg(T62, T63, T64, perm38_out_gg(T73, T64)) → perm38_out_gg(T62, .(T63, T64))
U16_gg(T13, T14, T15, perm38_out_gg(T37, T15)) → ss1_out_gg(T13, .(T14, T15))
U16_gg(T13, T14, T15, perm38_out_gg(T37, T15)) → U17_gg(T13, T14, T15, ordered39_in_gg(T14, T15))
ordered39_in_gg(T82, []) → ordered39_out_gg(T82, [])
ordered39_in_gg(T89, .(T90, T91)) → U8_gg(T89, T90, T91, less61_in_gg(T89, T90))
less61_in_gg(0, T100) → less61_out_gg(0, T100)
less61_in_gg(s(T105), T106) → U11_gg(T105, T106, less69_in_gg(T105, T106))
less69_in_gg(0, s(T113)) → less69_out_gg(0, s(T113))
less69_in_gg(s(T118), s(T119)) → U10_gg(T118, T119, less69_in_gg(T118, T119))
U10_gg(T118, T119, less69_out_gg(T118, T119)) → less69_out_gg(s(T118), s(T119))
U11_gg(T105, T106, less69_out_gg(T105, T106)) → less61_out_gg(s(T105), T106)
U8_gg(T89, T90, T91, less61_out_gg(T89, T90)) → ordered39_out_gg(T89, .(T90, T91))
U8_gg(T89, T90, T91, less61_out_gg(T89, T90)) → U9_gg(T89, T90, T91, ordered39_in_gg(T90, T91))
U9_gg(T89, T90, T91, ordered39_out_gg(T90, T91)) → ordered39_out_gg(T89, .(T90, T91))
U17_gg(T13, T14, T15, ordered39_out_gg(T14, T15)) → ss1_out_gg(T13, .(T14, T15))

The argument filtering Pi contains the following mapping:
ss1_in_gg(x1, x2)  =  ss1_in_gg(x1, x2)
[]  =  []
ss1_out_gg(x1, x2)  =  ss1_out_gg
.(x1, x2)  =  .(x1, x2)
U12_gg(x1, x2, x3, x4)  =  U12_gg(x4)
app18_in_agag(x1, x2, x3, x4)  =  app18_in_agag(x2, x4)
app18_out_agag(x1, x2, x3, x4)  =  app18_out_agag(x1, x3)
U1_agag(x1, x2, x3, x4, x5, x6)  =  U1_agag(x1, x6)
U13_gg(x1, x2, x3, x4)  =  U13_gg(x2, x3, x4)
U14_gg(x1, x2, x3, x4)  =  U14_gg(x4)
app28_in_gga(x1, x2, x3)  =  app28_in_gga(x1, x2)
app28_out_gga(x1, x2, x3)  =  app28_out_gga(x3)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x5)
U15_gg(x1, x2, x3, x4)  =  U15_gg(x2, x3, x4)
U16_gg(x1, x2, x3, x4)  =  U16_gg(x2, x3, x4)
perm38_in_gg(x1, x2)  =  perm38_in_gg(x1, x2)
perm38_out_gg(x1, x2)  =  perm38_out_gg
U3_gg(x1, x2, x3, x4)  =  U3_gg(x4)
U4_gg(x1, x2, x3, x4)  =  U4_gg(x3, x4)
U5_gg(x1, x2, x3, x4)  =  U5_gg(x4)
U6_gg(x1, x2, x3, x4)  =  U6_gg(x3, x4)
U7_gg(x1, x2, x3, x4)  =  U7_gg(x4)
U17_gg(x1, x2, x3, x4)  =  U17_gg(x4)
ordered39_in_gg(x1, x2)  =  ordered39_in_gg(x1, x2)
ordered39_out_gg(x1, x2)  =  ordered39_out_gg
U8_gg(x1, x2, x3, x4)  =  U8_gg(x2, x3, x4)
less61_in_gg(x1, x2)  =  less61_in_gg(x1, x2)
0  =  0
less61_out_gg(x1, x2)  =  less61_out_gg
s(x1)  =  s(x1)
U11_gg(x1, x2, x3)  =  U11_gg(x3)
less69_in_gg(x1, x2)  =  less69_in_gg(x1, x2)
less69_out_gg(x1, x2)  =  less69_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
U9_gg(x1, x2, x3, x4)  =  U9_gg(x4)
PERM38_IN_GG(x1, x2)  =  PERM38_IN_GG(x1, x2)
U4_GG(x1, x2, x3, x4)  =  U4_GG(x3, x4)
U6_GG(x1, x2, x3, x4)  =  U6_GG(x3, x4)

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

(38) UsableRulesProof (EQUIVALENT transformation)

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

(39) Obligation:

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

PERM38_IN_GG(T62, .(T63, T64)) → U4_GG(T62, T63, T64, app18_in_agag(T67, T63, T68, T62))
U4_GG(T62, T63, T64, app18_out_agag(T67, T63, T68, T62)) → U6_GG(T62, T63, T64, app28_in_gga(T67, T68, T73))
U6_GG(T62, T63, T64, app28_out_gga(T67, T68, T73)) → PERM38_IN_GG(T73, T64)

The TRS R consists of the following rules:

app18_in_agag([], T26, X46, .(T26, X46)) → app18_out_agag([], T26, X46, .(T26, X46))
app18_in_agag(.(X66, X67), T31, X68, .(X66, T32)) → U1_agag(X66, X67, T31, X68, T32, app18_in_agag(X67, T31, X68, T32))
app28_in_gga([], T44, T44) → app28_out_gga([], T44, T44)
app28_in_gga(.(T51, T52), T53, .(T51, X101)) → U2_gga(T51, T52, T53, X101, app28_in_gga(T52, T53, X101))
U1_agag(X66, X67, T31, X68, T32, app18_out_agag(X67, T31, X68, T32)) → app18_out_agag(.(X66, X67), T31, X68, .(X66, T32))
U2_gga(T51, T52, T53, X101, app28_out_gga(T52, T53, X101)) → app28_out_gga(.(T51, T52), T53, .(T51, X101))

The argument filtering Pi contains the following mapping:
[]  =  []
.(x1, x2)  =  .(x1, x2)
app18_in_agag(x1, x2, x3, x4)  =  app18_in_agag(x2, x4)
app18_out_agag(x1, x2, x3, x4)  =  app18_out_agag(x1, x3)
U1_agag(x1, x2, x3, x4, x5, x6)  =  U1_agag(x1, x6)
app28_in_gga(x1, x2, x3)  =  app28_in_gga(x1, x2)
app28_out_gga(x1, x2, x3)  =  app28_out_gga(x3)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x5)
PERM38_IN_GG(x1, x2)  =  PERM38_IN_GG(x1, x2)
U4_GG(x1, x2, x3, x4)  =  U4_GG(x3, x4)
U6_GG(x1, x2, x3, x4)  =  U6_GG(x3, x4)

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

(40) PiDPToQDPProof (SOUND transformation)

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

(41) Obligation:

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

PERM38_IN_GG(T62, .(T63, T64)) → U4_GG(T64, app18_in_agag(T63, T62))
U4_GG(T64, app18_out_agag(T67, T68)) → U6_GG(T64, app28_in_gga(T67, T68))
U6_GG(T64, app28_out_gga(T73)) → PERM38_IN_GG(T73, T64)

The TRS R consists of the following rules:

app18_in_agag(T26, .(T26, X46)) → app18_out_agag([], X46)
app18_in_agag(T31, .(X66, T32)) → U1_agag(X66, app18_in_agag(T31, T32))
app28_in_gga([], T44) → app28_out_gga(T44)
app28_in_gga(.(T51, T52), T53) → U2_gga(T51, app28_in_gga(T52, T53))
U1_agag(X66, app18_out_agag(X67, X68)) → app18_out_agag(.(X66, X67), X68)
U2_gga(T51, app28_out_gga(X101)) → app28_out_gga(.(T51, X101))

The set Q consists of the following terms:

app18_in_agag(x0, x1)
app28_in_gga(x0, x1)
U1_agag(x0, x1)
U2_gga(x0, x1)

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

(42) 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(T64, app18_out_agag(T67, T68)) → U6_GG(T64, app28_in_gga(T67, T68))
    The graph contains the following edges 1 >= 1

  • U6_GG(T64, app28_out_gga(T73)) → PERM38_IN_GG(T73, T64)
    The graph contains the following edges 2 > 1, 1 >= 2

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

(43) YES