(0) Obligation:

Clauses:

slowsort(X, Y) :- ','(perm(X, Y), sorted(Y)).
sorted([]).
sorted(.(X, [])).
sorted(.(X, .(Y, Z))) :- ','(le(X, Y), sorted(.(Y, Z))).
perm([], []).
perm(.(X, .(Y, [])), .(U, .(V, []))) :- ','(delete(U, .(X, Y), Z), perm(Z, V)).
delete(X, .(X, Y), Y).
delete(X, .(Y, Z), W) :- delete(X, Z, W).
le(s(X), s(Y)) :- le(X, Y).
le(0, s(X)).
le(0, 0).

Queries:

slowsort(g,a).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

delete26(T81, .(T79, T80), X96) :- delete26(T81, T80, X96).
delete18(T57, T55, T56, X65) :- delete26(T57, T56, X65).
perm35(.(T95, .(T96, [])), .(T99, .(T100, []))) :- delete18(T99, T95, T96, X118).
perm35(.(T95, .(T96, [])), .(T99, .(T106, []))) :- ','(deletec18(T99, T95, T96, T105), perm35(T105, T106)).
le51(s(T136), s(T137)) :- le51(T136, T137).
slowsort1(.(T16, .(T17, [])), .(T20, .(T21, []))) :- delete18(T20, T16, T17, X22).
slowsort1(.(T16, .(T17, [])), .(T28, .(T27, []))) :- ','(deletec18(T28, T16, T17, T26), perm35(T26, T27)).
slowsort1(.(T16, .(T17, [])), .(T122, .(T123, []))) :- ','(deletec18(T122, T16, T17, T26), ','(permc35(T26, T123), le51(T122, T123))).

Clauses:

deletec26(T70, .(T70, T71), T71).
deletec26(T81, .(T79, T80), X96) :- deletec26(T81, T80, X96).
deletec18(T41, T41, T42, T42).
deletec18(T57, T55, T56, X65) :- deletec26(T57, T56, X65).
permc35([], []).
permc35(.(T95, .(T96, [])), .(T99, .(T106, []))) :- ','(deletec18(T99, T95, T96, T105), permc35(T105, T106)).
lec51(s(T136), s(T137)) :- lec51(T136, T137).
lec51(0, s(T144)).
lec51(0, 0).

Afs:

slowsort1(x1, x2)  =  slowsort1(x1)

(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:
slowsort1_in: (b,f)
delete18_in: (f,b,b,f)
delete26_in: (f,b,f)
deletec18_in: (f,b,b,f)
deletec26_in: (f,b,f)
perm35_in: (b,f)
permc35_in: (b,f)
le51_in: (b,b)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

SLOWSORT1_IN_GA(.(T16, .(T17, [])), .(T20, .(T21, []))) → U7_GA(T16, T17, T20, T21, delete18_in_agga(T20, T16, T17, X22))
SLOWSORT1_IN_GA(.(T16, .(T17, [])), .(T20, .(T21, []))) → DELETE18_IN_AGGA(T20, T16, T17, X22)
DELETE18_IN_AGGA(T57, T55, T56, X65) → U2_AGGA(T57, T55, T56, X65, delete26_in_aga(T57, T56, X65))
DELETE18_IN_AGGA(T57, T55, T56, X65) → DELETE26_IN_AGA(T57, T56, X65)
DELETE26_IN_AGA(T81, .(T79, T80), X96) → U1_AGA(T81, T79, T80, X96, delete26_in_aga(T81, T80, X96))
DELETE26_IN_AGA(T81, .(T79, T80), X96) → DELETE26_IN_AGA(T81, T80, X96)
SLOWSORT1_IN_GA(.(T16, .(T17, [])), .(T28, .(T27, []))) → U8_GA(T16, T17, T28, T27, deletec18_in_agga(T28, T16, T17, T26))
U8_GA(T16, T17, T28, T27, deletec18_out_agga(T28, T16, T17, T26)) → U9_GA(T16, T17, T28, T27, perm35_in_ga(T26, T27))
U8_GA(T16, T17, T28, T27, deletec18_out_agga(T28, T16, T17, T26)) → PERM35_IN_GA(T26, T27)
PERM35_IN_GA(.(T95, .(T96, [])), .(T99, .(T100, []))) → U3_GA(T95, T96, T99, T100, delete18_in_agga(T99, T95, T96, X118))
PERM35_IN_GA(.(T95, .(T96, [])), .(T99, .(T100, []))) → DELETE18_IN_AGGA(T99, T95, T96, X118)
PERM35_IN_GA(.(T95, .(T96, [])), .(T99, .(T106, []))) → U4_GA(T95, T96, T99, T106, deletec18_in_agga(T99, T95, T96, T105))
U4_GA(T95, T96, T99, T106, deletec18_out_agga(T99, T95, T96, T105)) → U5_GA(T95, T96, T99, T106, perm35_in_ga(T105, T106))
U4_GA(T95, T96, T99, T106, deletec18_out_agga(T99, T95, T96, T105)) → PERM35_IN_GA(T105, T106)
SLOWSORT1_IN_GA(.(T16, .(T17, [])), .(T122, .(T123, []))) → U10_GA(T16, T17, T122, T123, deletec18_in_agga(T122, T16, T17, T26))
U10_GA(T16, T17, T122, T123, deletec18_out_agga(T122, T16, T17, T26)) → U11_GA(T16, T17, T122, T123, permc35_in_ga(T26, T123))
U11_GA(T16, T17, T122, T123, permc35_out_ga(T26, T123)) → U12_GA(T16, T17, T122, T123, le51_in_gg(T122, T123))
U11_GA(T16, T17, T122, T123, permc35_out_ga(T26, T123)) → LE51_IN_GG(T122, T123)
LE51_IN_GG(s(T136), s(T137)) → U6_GG(T136, T137, le51_in_gg(T136, T137))
LE51_IN_GG(s(T136), s(T137)) → LE51_IN_GG(T136, T137)

The TRS R consists of the following rules:

deletec18_in_agga(T41, T41, T42, T42) → deletec18_out_agga(T41, T41, T42, T42)
deletec18_in_agga(T57, T55, T56, X65) → U15_agga(T57, T55, T56, X65, deletec26_in_aga(T57, T56, X65))
deletec26_in_aga(T70, .(T70, T71), T71) → deletec26_out_aga(T70, .(T70, T71), T71)
deletec26_in_aga(T81, .(T79, T80), X96) → U14_aga(T81, T79, T80, X96, deletec26_in_aga(T81, T80, X96))
U14_aga(T81, T79, T80, X96, deletec26_out_aga(T81, T80, X96)) → deletec26_out_aga(T81, .(T79, T80), X96)
U15_agga(T57, T55, T56, X65, deletec26_out_aga(T57, T56, X65)) → deletec18_out_agga(T57, T55, T56, X65)
permc35_in_ga([], []) → permc35_out_ga([], [])
permc35_in_ga(.(T95, .(T96, [])), .(T99, .(T106, []))) → U16_ga(T95, T96, T99, T106, deletec18_in_agga(T99, T95, T96, T105))
U16_ga(T95, T96, T99, T106, deletec18_out_agga(T99, T95, T96, T105)) → U17_ga(T95, T96, T99, T106, permc35_in_ga(T105, T106))
U17_ga(T95, T96, T99, T106, permc35_out_ga(T105, T106)) → permc35_out_ga(.(T95, .(T96, [])), .(T99, .(T106, [])))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
[]  =  []
delete18_in_agga(x1, x2, x3, x4)  =  delete18_in_agga(x2, x3)
delete26_in_aga(x1, x2, x3)  =  delete26_in_aga(x2)
deletec18_in_agga(x1, x2, x3, x4)  =  deletec18_in_agga(x2, x3)
deletec18_out_agga(x1, x2, x3, x4)  =  deletec18_out_agga(x1, x2, x3, x4)
U15_agga(x1, x2, x3, x4, x5)  =  U15_agga(x2, x3, x5)
deletec26_in_aga(x1, x2, x3)  =  deletec26_in_aga(x2)
deletec26_out_aga(x1, x2, x3)  =  deletec26_out_aga(x1, x2, x3)
U14_aga(x1, x2, x3, x4, x5)  =  U14_aga(x2, x3, x5)
perm35_in_ga(x1, x2)  =  perm35_in_ga(x1)
permc35_in_ga(x1, x2)  =  permc35_in_ga(x1)
permc35_out_ga(x1, x2)  =  permc35_out_ga(x1, x2)
U16_ga(x1, x2, x3, x4, x5)  =  U16_ga(x1, x2, x5)
U17_ga(x1, x2, x3, x4, x5)  =  U17_ga(x1, x2, x3, x5)
le51_in_gg(x1, x2)  =  le51_in_gg(x1, x2)
s(x1)  =  s(x1)
SLOWSORT1_IN_GA(x1, x2)  =  SLOWSORT1_IN_GA(x1)
U7_GA(x1, x2, x3, x4, x5)  =  U7_GA(x1, x2, x5)
DELETE18_IN_AGGA(x1, x2, x3, x4)  =  DELETE18_IN_AGGA(x2, x3)
U2_AGGA(x1, x2, x3, x4, x5)  =  U2_AGGA(x2, x3, x5)
DELETE26_IN_AGA(x1, x2, x3)  =  DELETE26_IN_AGA(x2)
U1_AGA(x1, x2, x3, x4, x5)  =  U1_AGA(x2, x3, x5)
U8_GA(x1, x2, x3, x4, x5)  =  U8_GA(x1, x2, x5)
U9_GA(x1, x2, x3, x4, x5)  =  U9_GA(x1, x2, x5)
PERM35_IN_GA(x1, x2)  =  PERM35_IN_GA(x1)
U3_GA(x1, x2, x3, x4, x5)  =  U3_GA(x1, x2, x5)
U4_GA(x1, x2, x3, x4, x5)  =  U4_GA(x1, x2, x5)
U5_GA(x1, x2, x3, x4, x5)  =  U5_GA(x1, x2, x5)
U10_GA(x1, x2, x3, x4, x5)  =  U10_GA(x1, x2, x5)
U11_GA(x1, x2, x3, x4, x5)  =  U11_GA(x1, x2, x3, x5)
U12_GA(x1, x2, x3, x4, x5)  =  U12_GA(x1, x2, x5)
LE51_IN_GG(x1, x2)  =  LE51_IN_GG(x1, x2)
U6_GG(x1, x2, x3)  =  U6_GG(x1, x2, x3)

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:

SLOWSORT1_IN_GA(.(T16, .(T17, [])), .(T20, .(T21, []))) → U7_GA(T16, T17, T20, T21, delete18_in_agga(T20, T16, T17, X22))
SLOWSORT1_IN_GA(.(T16, .(T17, [])), .(T20, .(T21, []))) → DELETE18_IN_AGGA(T20, T16, T17, X22)
DELETE18_IN_AGGA(T57, T55, T56, X65) → U2_AGGA(T57, T55, T56, X65, delete26_in_aga(T57, T56, X65))
DELETE18_IN_AGGA(T57, T55, T56, X65) → DELETE26_IN_AGA(T57, T56, X65)
DELETE26_IN_AGA(T81, .(T79, T80), X96) → U1_AGA(T81, T79, T80, X96, delete26_in_aga(T81, T80, X96))
DELETE26_IN_AGA(T81, .(T79, T80), X96) → DELETE26_IN_AGA(T81, T80, X96)
SLOWSORT1_IN_GA(.(T16, .(T17, [])), .(T28, .(T27, []))) → U8_GA(T16, T17, T28, T27, deletec18_in_agga(T28, T16, T17, T26))
U8_GA(T16, T17, T28, T27, deletec18_out_agga(T28, T16, T17, T26)) → U9_GA(T16, T17, T28, T27, perm35_in_ga(T26, T27))
U8_GA(T16, T17, T28, T27, deletec18_out_agga(T28, T16, T17, T26)) → PERM35_IN_GA(T26, T27)
PERM35_IN_GA(.(T95, .(T96, [])), .(T99, .(T100, []))) → U3_GA(T95, T96, T99, T100, delete18_in_agga(T99, T95, T96, X118))
PERM35_IN_GA(.(T95, .(T96, [])), .(T99, .(T100, []))) → DELETE18_IN_AGGA(T99, T95, T96, X118)
PERM35_IN_GA(.(T95, .(T96, [])), .(T99, .(T106, []))) → U4_GA(T95, T96, T99, T106, deletec18_in_agga(T99, T95, T96, T105))
U4_GA(T95, T96, T99, T106, deletec18_out_agga(T99, T95, T96, T105)) → U5_GA(T95, T96, T99, T106, perm35_in_ga(T105, T106))
U4_GA(T95, T96, T99, T106, deletec18_out_agga(T99, T95, T96, T105)) → PERM35_IN_GA(T105, T106)
SLOWSORT1_IN_GA(.(T16, .(T17, [])), .(T122, .(T123, []))) → U10_GA(T16, T17, T122, T123, deletec18_in_agga(T122, T16, T17, T26))
U10_GA(T16, T17, T122, T123, deletec18_out_agga(T122, T16, T17, T26)) → U11_GA(T16, T17, T122, T123, permc35_in_ga(T26, T123))
U11_GA(T16, T17, T122, T123, permc35_out_ga(T26, T123)) → U12_GA(T16, T17, T122, T123, le51_in_gg(T122, T123))
U11_GA(T16, T17, T122, T123, permc35_out_ga(T26, T123)) → LE51_IN_GG(T122, T123)
LE51_IN_GG(s(T136), s(T137)) → U6_GG(T136, T137, le51_in_gg(T136, T137))
LE51_IN_GG(s(T136), s(T137)) → LE51_IN_GG(T136, T137)

The TRS R consists of the following rules:

deletec18_in_agga(T41, T41, T42, T42) → deletec18_out_agga(T41, T41, T42, T42)
deletec18_in_agga(T57, T55, T56, X65) → U15_agga(T57, T55, T56, X65, deletec26_in_aga(T57, T56, X65))
deletec26_in_aga(T70, .(T70, T71), T71) → deletec26_out_aga(T70, .(T70, T71), T71)
deletec26_in_aga(T81, .(T79, T80), X96) → U14_aga(T81, T79, T80, X96, deletec26_in_aga(T81, T80, X96))
U14_aga(T81, T79, T80, X96, deletec26_out_aga(T81, T80, X96)) → deletec26_out_aga(T81, .(T79, T80), X96)
U15_agga(T57, T55, T56, X65, deletec26_out_aga(T57, T56, X65)) → deletec18_out_agga(T57, T55, T56, X65)
permc35_in_ga([], []) → permc35_out_ga([], [])
permc35_in_ga(.(T95, .(T96, [])), .(T99, .(T106, []))) → U16_ga(T95, T96, T99, T106, deletec18_in_agga(T99, T95, T96, T105))
U16_ga(T95, T96, T99, T106, deletec18_out_agga(T99, T95, T96, T105)) → U17_ga(T95, T96, T99, T106, permc35_in_ga(T105, T106))
U17_ga(T95, T96, T99, T106, permc35_out_ga(T105, T106)) → permc35_out_ga(.(T95, .(T96, [])), .(T99, .(T106, [])))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
[]  =  []
delete18_in_agga(x1, x2, x3, x4)  =  delete18_in_agga(x2, x3)
delete26_in_aga(x1, x2, x3)  =  delete26_in_aga(x2)
deletec18_in_agga(x1, x2, x3, x4)  =  deletec18_in_agga(x2, x3)
deletec18_out_agga(x1, x2, x3, x4)  =  deletec18_out_agga(x1, x2, x3, x4)
U15_agga(x1, x2, x3, x4, x5)  =  U15_agga(x2, x3, x5)
deletec26_in_aga(x1, x2, x3)  =  deletec26_in_aga(x2)
deletec26_out_aga(x1, x2, x3)  =  deletec26_out_aga(x1, x2, x3)
U14_aga(x1, x2, x3, x4, x5)  =  U14_aga(x2, x3, x5)
perm35_in_ga(x1, x2)  =  perm35_in_ga(x1)
permc35_in_ga(x1, x2)  =  permc35_in_ga(x1)
permc35_out_ga(x1, x2)  =  permc35_out_ga(x1, x2)
U16_ga(x1, x2, x3, x4, x5)  =  U16_ga(x1, x2, x5)
U17_ga(x1, x2, x3, x4, x5)  =  U17_ga(x1, x2, x3, x5)
le51_in_gg(x1, x2)  =  le51_in_gg(x1, x2)
s(x1)  =  s(x1)
SLOWSORT1_IN_GA(x1, x2)  =  SLOWSORT1_IN_GA(x1)
U7_GA(x1, x2, x3, x4, x5)  =  U7_GA(x1, x2, x5)
DELETE18_IN_AGGA(x1, x2, x3, x4)  =  DELETE18_IN_AGGA(x2, x3)
U2_AGGA(x1, x2, x3, x4, x5)  =  U2_AGGA(x2, x3, x5)
DELETE26_IN_AGA(x1, x2, x3)  =  DELETE26_IN_AGA(x2)
U1_AGA(x1, x2, x3, x4, x5)  =  U1_AGA(x2, x3, x5)
U8_GA(x1, x2, x3, x4, x5)  =  U8_GA(x1, x2, x5)
U9_GA(x1, x2, x3, x4, x5)  =  U9_GA(x1, x2, x5)
PERM35_IN_GA(x1, x2)  =  PERM35_IN_GA(x1)
U3_GA(x1, x2, x3, x4, x5)  =  U3_GA(x1, x2, x5)
U4_GA(x1, x2, x3, x4, x5)  =  U4_GA(x1, x2, x5)
U5_GA(x1, x2, x3, x4, x5)  =  U5_GA(x1, x2, x5)
U10_GA(x1, x2, x3, x4, x5)  =  U10_GA(x1, x2, x5)
U11_GA(x1, x2, x3, x4, x5)  =  U11_GA(x1, x2, x3, x5)
U12_GA(x1, x2, x3, x4, x5)  =  U12_GA(x1, x2, x5)
LE51_IN_GG(x1, x2)  =  LE51_IN_GG(x1, x2)
U6_GG(x1, x2, x3)  =  U6_GG(x1, x2, x3)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 16 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

LE51_IN_GG(s(T136), s(T137)) → LE51_IN_GG(T136, T137)

The TRS R consists of the following rules:

deletec18_in_agga(T41, T41, T42, T42) → deletec18_out_agga(T41, T41, T42, T42)
deletec18_in_agga(T57, T55, T56, X65) → U15_agga(T57, T55, T56, X65, deletec26_in_aga(T57, T56, X65))
deletec26_in_aga(T70, .(T70, T71), T71) → deletec26_out_aga(T70, .(T70, T71), T71)
deletec26_in_aga(T81, .(T79, T80), X96) → U14_aga(T81, T79, T80, X96, deletec26_in_aga(T81, T80, X96))
U14_aga(T81, T79, T80, X96, deletec26_out_aga(T81, T80, X96)) → deletec26_out_aga(T81, .(T79, T80), X96)
U15_agga(T57, T55, T56, X65, deletec26_out_aga(T57, T56, X65)) → deletec18_out_agga(T57, T55, T56, X65)
permc35_in_ga([], []) → permc35_out_ga([], [])
permc35_in_ga(.(T95, .(T96, [])), .(T99, .(T106, []))) → U16_ga(T95, T96, T99, T106, deletec18_in_agga(T99, T95, T96, T105))
U16_ga(T95, T96, T99, T106, deletec18_out_agga(T99, T95, T96, T105)) → U17_ga(T95, T96, T99, T106, permc35_in_ga(T105, T106))
U17_ga(T95, T96, T99, T106, permc35_out_ga(T105, T106)) → permc35_out_ga(.(T95, .(T96, [])), .(T99, .(T106, [])))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
[]  =  []
deletec18_in_agga(x1, x2, x3, x4)  =  deletec18_in_agga(x2, x3)
deletec18_out_agga(x1, x2, x3, x4)  =  deletec18_out_agga(x1, x2, x3, x4)
U15_agga(x1, x2, x3, x4, x5)  =  U15_agga(x2, x3, x5)
deletec26_in_aga(x1, x2, x3)  =  deletec26_in_aga(x2)
deletec26_out_aga(x1, x2, x3)  =  deletec26_out_aga(x1, x2, x3)
U14_aga(x1, x2, x3, x4, x5)  =  U14_aga(x2, x3, x5)
permc35_in_ga(x1, x2)  =  permc35_in_ga(x1)
permc35_out_ga(x1, x2)  =  permc35_out_ga(x1, x2)
U16_ga(x1, x2, x3, x4, x5)  =  U16_ga(x1, x2, x5)
U17_ga(x1, x2, x3, x4, x5)  =  U17_ga(x1, x2, x3, x5)
s(x1)  =  s(x1)
LE51_IN_GG(x1, x2)  =  LE51_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:

LE51_IN_GG(s(T136), s(T137)) → LE51_IN_GG(T136, T137)

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:

LE51_IN_GG(s(T136), s(T137)) → LE51_IN_GG(T136, T137)

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:

  • LE51_IN_GG(s(T136), s(T137)) → LE51_IN_GG(T136, T137)
    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:

DELETE26_IN_AGA(T81, .(T79, T80), X96) → DELETE26_IN_AGA(T81, T80, X96)

The TRS R consists of the following rules:

deletec18_in_agga(T41, T41, T42, T42) → deletec18_out_agga(T41, T41, T42, T42)
deletec18_in_agga(T57, T55, T56, X65) → U15_agga(T57, T55, T56, X65, deletec26_in_aga(T57, T56, X65))
deletec26_in_aga(T70, .(T70, T71), T71) → deletec26_out_aga(T70, .(T70, T71), T71)
deletec26_in_aga(T81, .(T79, T80), X96) → U14_aga(T81, T79, T80, X96, deletec26_in_aga(T81, T80, X96))
U14_aga(T81, T79, T80, X96, deletec26_out_aga(T81, T80, X96)) → deletec26_out_aga(T81, .(T79, T80), X96)
U15_agga(T57, T55, T56, X65, deletec26_out_aga(T57, T56, X65)) → deletec18_out_agga(T57, T55, T56, X65)
permc35_in_ga([], []) → permc35_out_ga([], [])
permc35_in_ga(.(T95, .(T96, [])), .(T99, .(T106, []))) → U16_ga(T95, T96, T99, T106, deletec18_in_agga(T99, T95, T96, T105))
U16_ga(T95, T96, T99, T106, deletec18_out_agga(T99, T95, T96, T105)) → U17_ga(T95, T96, T99, T106, permc35_in_ga(T105, T106))
U17_ga(T95, T96, T99, T106, permc35_out_ga(T105, T106)) → permc35_out_ga(.(T95, .(T96, [])), .(T99, .(T106, [])))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
[]  =  []
deletec18_in_agga(x1, x2, x3, x4)  =  deletec18_in_agga(x2, x3)
deletec18_out_agga(x1, x2, x3, x4)  =  deletec18_out_agga(x1, x2, x3, x4)
U15_agga(x1, x2, x3, x4, x5)  =  U15_agga(x2, x3, x5)
deletec26_in_aga(x1, x2, x3)  =  deletec26_in_aga(x2)
deletec26_out_aga(x1, x2, x3)  =  deletec26_out_aga(x1, x2, x3)
U14_aga(x1, x2, x3, x4, x5)  =  U14_aga(x2, x3, x5)
permc35_in_ga(x1, x2)  =  permc35_in_ga(x1)
permc35_out_ga(x1, x2)  =  permc35_out_ga(x1, x2)
U16_ga(x1, x2, x3, x4, x5)  =  U16_ga(x1, x2, x5)
U17_ga(x1, x2, x3, x4, x5)  =  U17_ga(x1, x2, x3, x5)
DELETE26_IN_AGA(x1, x2, x3)  =  DELETE26_IN_AGA(x2)

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

(15) UsableRulesProof (EQUIVALENT transformation)

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

(16) Obligation:

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

DELETE26_IN_AGA(T81, .(T79, T80), X96) → DELETE26_IN_AGA(T81, T80, X96)

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

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

(17) PiDPToQDPProof (SOUND transformation)

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

(18) Obligation:

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

DELETE26_IN_AGA(.(T79, T80)) → DELETE26_IN_AGA(T80)

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

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • DELETE26_IN_AGA(.(T79, T80)) → DELETE26_IN_AGA(T80)
    The graph contains the following edges 1 > 1

(20) YES

(21) Obligation:

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

PERM35_IN_GA(.(T95, .(T96, [])), .(T99, .(T106, []))) → U4_GA(T95, T96, T99, T106, deletec18_in_agga(T99, T95, T96, T105))
U4_GA(T95, T96, T99, T106, deletec18_out_agga(T99, T95, T96, T105)) → PERM35_IN_GA(T105, T106)

The TRS R consists of the following rules:

deletec18_in_agga(T41, T41, T42, T42) → deletec18_out_agga(T41, T41, T42, T42)
deletec18_in_agga(T57, T55, T56, X65) → U15_agga(T57, T55, T56, X65, deletec26_in_aga(T57, T56, X65))
deletec26_in_aga(T70, .(T70, T71), T71) → deletec26_out_aga(T70, .(T70, T71), T71)
deletec26_in_aga(T81, .(T79, T80), X96) → U14_aga(T81, T79, T80, X96, deletec26_in_aga(T81, T80, X96))
U14_aga(T81, T79, T80, X96, deletec26_out_aga(T81, T80, X96)) → deletec26_out_aga(T81, .(T79, T80), X96)
U15_agga(T57, T55, T56, X65, deletec26_out_aga(T57, T56, X65)) → deletec18_out_agga(T57, T55, T56, X65)
permc35_in_ga([], []) → permc35_out_ga([], [])
permc35_in_ga(.(T95, .(T96, [])), .(T99, .(T106, []))) → U16_ga(T95, T96, T99, T106, deletec18_in_agga(T99, T95, T96, T105))
U16_ga(T95, T96, T99, T106, deletec18_out_agga(T99, T95, T96, T105)) → U17_ga(T95, T96, T99, T106, permc35_in_ga(T105, T106))
U17_ga(T95, T96, T99, T106, permc35_out_ga(T105, T106)) → permc35_out_ga(.(T95, .(T96, [])), .(T99, .(T106, [])))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
[]  =  []
deletec18_in_agga(x1, x2, x3, x4)  =  deletec18_in_agga(x2, x3)
deletec18_out_agga(x1, x2, x3, x4)  =  deletec18_out_agga(x1, x2, x3, x4)
U15_agga(x1, x2, x3, x4, x5)  =  U15_agga(x2, x3, x5)
deletec26_in_aga(x1, x2, x3)  =  deletec26_in_aga(x2)
deletec26_out_aga(x1, x2, x3)  =  deletec26_out_aga(x1, x2, x3)
U14_aga(x1, x2, x3, x4, x5)  =  U14_aga(x2, x3, x5)
permc35_in_ga(x1, x2)  =  permc35_in_ga(x1)
permc35_out_ga(x1, x2)  =  permc35_out_ga(x1, x2)
U16_ga(x1, x2, x3, x4, x5)  =  U16_ga(x1, x2, x5)
U17_ga(x1, x2, x3, x4, x5)  =  U17_ga(x1, x2, x3, x5)
PERM35_IN_GA(x1, x2)  =  PERM35_IN_GA(x1)
U4_GA(x1, x2, x3, x4, x5)  =  U4_GA(x1, x2, x5)

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:

PERM35_IN_GA(.(T95, .(T96, [])), .(T99, .(T106, []))) → U4_GA(T95, T96, T99, T106, deletec18_in_agga(T99, T95, T96, T105))
U4_GA(T95, T96, T99, T106, deletec18_out_agga(T99, T95, T96, T105)) → PERM35_IN_GA(T105, T106)

The TRS R consists of the following rules:

deletec18_in_agga(T41, T41, T42, T42) → deletec18_out_agga(T41, T41, T42, T42)
deletec18_in_agga(T57, T55, T56, X65) → U15_agga(T57, T55, T56, X65, deletec26_in_aga(T57, T56, X65))
U15_agga(T57, T55, T56, X65, deletec26_out_aga(T57, T56, X65)) → deletec18_out_agga(T57, T55, T56, X65)
deletec26_in_aga(T70, .(T70, T71), T71) → deletec26_out_aga(T70, .(T70, T71), T71)
deletec26_in_aga(T81, .(T79, T80), X96) → U14_aga(T81, T79, T80, X96, deletec26_in_aga(T81, T80, X96))
U14_aga(T81, T79, T80, X96, deletec26_out_aga(T81, T80, X96)) → deletec26_out_aga(T81, .(T79, T80), X96)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
[]  =  []
deletec18_in_agga(x1, x2, x3, x4)  =  deletec18_in_agga(x2, x3)
deletec18_out_agga(x1, x2, x3, x4)  =  deletec18_out_agga(x1, x2, x3, x4)
U15_agga(x1, x2, x3, x4, x5)  =  U15_agga(x2, x3, x5)
deletec26_in_aga(x1, x2, x3)  =  deletec26_in_aga(x2)
deletec26_out_aga(x1, x2, x3)  =  deletec26_out_aga(x1, x2, x3)
U14_aga(x1, x2, x3, x4, x5)  =  U14_aga(x2, x3, x5)
PERM35_IN_GA(x1, x2)  =  PERM35_IN_GA(x1)
U4_GA(x1, x2, x3, x4, x5)  =  U4_GA(x1, x2, x5)

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:

PERM35_IN_GA(.(T95, .(T96, []))) → U4_GA(T95, T96, deletec18_in_agga(T95, T96))
U4_GA(T95, T96, deletec18_out_agga(T99, T95, T96, T105)) → PERM35_IN_GA(T105)

The TRS R consists of the following rules:

deletec18_in_agga(T41, T42) → deletec18_out_agga(T41, T41, T42, T42)
deletec18_in_agga(T55, T56) → U15_agga(T55, T56, deletec26_in_aga(T56))
U15_agga(T55, T56, deletec26_out_aga(T57, T56, X65)) → deletec18_out_agga(T57, T55, T56, X65)
deletec26_in_aga(.(T70, T71)) → deletec26_out_aga(T70, .(T70, T71), T71)
deletec26_in_aga(.(T79, T80)) → U14_aga(T79, T80, deletec26_in_aga(T80))
U14_aga(T79, T80, deletec26_out_aga(T81, T80, X96)) → deletec26_out_aga(T81, .(T79, T80), X96)

The set Q consists of the following terms:

deletec18_in_agga(x0, x1)
U15_agga(x0, x1, x2)
deletec26_in_aga(x0)
U14_aga(x0, x1, x2)

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

(26) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


PERM35_IN_GA(.(T95, .(T96, []))) → U4_GA(T95, T96, deletec18_in_agga(T95, T96))
U4_GA(T95, T96, deletec18_out_agga(T99, T95, T96, T105)) → PERM35_IN_GA(T105)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(.(x1, x2)) = 1 + x1 + x2   
POL(PERM35_IN_GA(x1)) = x1   
POL(U14_aga(x1, x2, x3)) = 1 + x1 + x3   
POL(U15_agga(x1, x2, x3)) = x3   
POL(U4_GA(x1, x2, x3)) = x3   
POL([]) = 1   
POL(deletec18_in_agga(x1, x2)) = 1 + x1 + x2   
POL(deletec18_out_agga(x1, x2, x3, x4)) = 1 + x4   
POL(deletec26_in_aga(x1)) = 1 + x1   
POL(deletec26_out_aga(x1, x2, x3)) = 1 + x1 + x3   

The following usable rules [FROCOS05] were oriented:

deletec18_in_agga(T41, T42) → deletec18_out_agga(T41, T41, T42, T42)
deletec18_in_agga(T55, T56) → U15_agga(T55, T56, deletec26_in_aga(T56))
deletec26_in_aga(.(T70, T71)) → deletec26_out_aga(T70, .(T70, T71), T71)
deletec26_in_aga(.(T79, T80)) → U14_aga(T79, T80, deletec26_in_aga(T80))
U15_agga(T55, T56, deletec26_out_aga(T57, T56, X65)) → deletec18_out_agga(T57, T55, T56, X65)
U14_aga(T79, T80, deletec26_out_aga(T81, T80, X96)) → deletec26_out_aga(T81, .(T79, T80), X96)

(27) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

deletec18_in_agga(T41, T42) → deletec18_out_agga(T41, T41, T42, T42)
deletec18_in_agga(T55, T56) → U15_agga(T55, T56, deletec26_in_aga(T56))
U15_agga(T55, T56, deletec26_out_aga(T57, T56, X65)) → deletec18_out_agga(T57, T55, T56, X65)
deletec26_in_aga(.(T70, T71)) → deletec26_out_aga(T70, .(T70, T71), T71)
deletec26_in_aga(.(T79, T80)) → U14_aga(T79, T80, deletec26_in_aga(T80))
U14_aga(T79, T80, deletec26_out_aga(T81, T80, X96)) → deletec26_out_aga(T81, .(T79, T80), X96)

The set Q consists of the following terms:

deletec18_in_agga(x0, x1)
U15_agga(x0, x1, x2)
deletec26_in_aga(x0)
U14_aga(x0, x1, x2)

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

(28) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(29) YES