(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(a,g).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

delete26(T76, .(T77, T79), X96) :- delete26(T76, T79, X96).
delete18(T52, T53, T55, X65) :- delete26(T52, T55, X65).
perm35(.(T96, .(T97, [])), .(T94, .(T95, []))) :- delete18(T94, T96, T97, X118).
perm35(.(T96, .(T97, [])), .(T94, .(T95, []))) :- ','(deletec18(T94, T96, T97, T102), perm35(T102, T95)).
le51(s(T132), s(T133)) :- le51(T132, T133).
slowsort1(.(T20, .(T21, [])), .(T18, .(T19, []))) :- delete18(T18, T20, T21, X22).
slowsort1(.(T20, .(T21, [])), .(T18, .(T19, []))) :- ','(deletec18(T18, T20, T21, T26), perm35(T26, T19)).
slowsort1(.(T20, .(T21, [])), .(T118, .(T119, []))) :- ','(deletec18(T118, T20, T21, T26), ','(permc35(T26, T119), le51(T118, T119))).

Clauses:

deletec26(T68, .(T68, T69), T69).
deletec26(T76, .(T77, T79), X96) :- deletec26(T76, T79, X96).
deletec18(T39, T39, T40, T40).
deletec18(T52, T53, T55, X65) :- deletec26(T52, T55, X65).
permc35([], []).
permc35(.(T96, .(T97, [])), .(T94, .(T95, []))) :- ','(deletec18(T94, T96, T97, T102), permc35(T102, T95)).
lec51(s(T132), s(T133)) :- lec51(T132, T133).
lec51(0, s(T140)).
lec51(0, 0).

Afs:

slowsort1(x1, x2)  =  slowsort1(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:
slowsort1_in: (f,b)
delete18_in: (b,f,f,f)
delete26_in: (b,f,f)
deletec18_in: (b,f,f,f)
deletec26_in: (b,f,f)
perm35_in: (f,b)
permc35_in: (f,b)
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_AG(.(T20, .(T21, [])), .(T18, .(T19, []))) → U7_AG(T20, T21, T18, T19, delete18_in_gaaa(T18, T20, T21, X22))
SLOWSORT1_IN_AG(.(T20, .(T21, [])), .(T18, .(T19, []))) → DELETE18_IN_GAAA(T18, T20, T21, X22)
DELETE18_IN_GAAA(T52, T53, T55, X65) → U2_GAAA(T52, T53, T55, X65, delete26_in_gaa(T52, T55, X65))
DELETE18_IN_GAAA(T52, T53, T55, X65) → DELETE26_IN_GAA(T52, T55, X65)
DELETE26_IN_GAA(T76, .(T77, T79), X96) → U1_GAA(T76, T77, T79, X96, delete26_in_gaa(T76, T79, X96))
DELETE26_IN_GAA(T76, .(T77, T79), X96) → DELETE26_IN_GAA(T76, T79, X96)
SLOWSORT1_IN_AG(.(T20, .(T21, [])), .(T18, .(T19, []))) → U8_AG(T20, T21, T18, T19, deletec18_in_gaaa(T18, T20, T21, T26))
U8_AG(T20, T21, T18, T19, deletec18_out_gaaa(T18, T20, T21, T26)) → U9_AG(T20, T21, T18, T19, perm35_in_ag(T26, T19))
U8_AG(T20, T21, T18, T19, deletec18_out_gaaa(T18, T20, T21, T26)) → PERM35_IN_AG(T26, T19)
PERM35_IN_AG(.(T96, .(T97, [])), .(T94, .(T95, []))) → U3_AG(T96, T97, T94, T95, delete18_in_gaaa(T94, T96, T97, X118))
PERM35_IN_AG(.(T96, .(T97, [])), .(T94, .(T95, []))) → DELETE18_IN_GAAA(T94, T96, T97, X118)
PERM35_IN_AG(.(T96, .(T97, [])), .(T94, .(T95, []))) → U4_AG(T96, T97, T94, T95, deletec18_in_gaaa(T94, T96, T97, T102))
U4_AG(T96, T97, T94, T95, deletec18_out_gaaa(T94, T96, T97, T102)) → U5_AG(T96, T97, T94, T95, perm35_in_ag(T102, T95))
U4_AG(T96, T97, T94, T95, deletec18_out_gaaa(T94, T96, T97, T102)) → PERM35_IN_AG(T102, T95)
SLOWSORT1_IN_AG(.(T20, .(T21, [])), .(T118, .(T119, []))) → U10_AG(T20, T21, T118, T119, deletec18_in_gaaa(T118, T20, T21, T26))
U10_AG(T20, T21, T118, T119, deletec18_out_gaaa(T118, T20, T21, T26)) → U11_AG(T20, T21, T118, T119, permc35_in_ag(T26, T119))
U11_AG(T20, T21, T118, T119, permc35_out_ag(T26, T119)) → U12_AG(T20, T21, T118, T119, le51_in_gg(T118, T119))
U11_AG(T20, T21, T118, T119, permc35_out_ag(T26, T119)) → LE51_IN_GG(T118, T119)
LE51_IN_GG(s(T132), s(T133)) → U6_GG(T132, T133, le51_in_gg(T132, T133))
LE51_IN_GG(s(T132), s(T133)) → LE51_IN_GG(T132, T133)

The TRS R consists of the following rules:

deletec18_in_gaaa(T39, T39, T40, T40) → deletec18_out_gaaa(T39, T39, T40, T40)
deletec18_in_gaaa(T52, T53, T55, X65) → U15_gaaa(T52, T53, T55, X65, deletec26_in_gaa(T52, T55, X65))
deletec26_in_gaa(T68, .(T68, T69), T69) → deletec26_out_gaa(T68, .(T68, T69), T69)
deletec26_in_gaa(T76, .(T77, T79), X96) → U14_gaa(T76, T77, T79, X96, deletec26_in_gaa(T76, T79, X96))
U14_gaa(T76, T77, T79, X96, deletec26_out_gaa(T76, T79, X96)) → deletec26_out_gaa(T76, .(T77, T79), X96)
U15_gaaa(T52, T53, T55, X65, deletec26_out_gaa(T52, T55, X65)) → deletec18_out_gaaa(T52, T53, T55, X65)
permc35_in_ag([], []) → permc35_out_ag([], [])
permc35_in_ag(.(T96, .(T97, [])), .(T94, .(T95, []))) → U16_ag(T96, T97, T94, T95, deletec18_in_gaaa(T94, T96, T97, T102))
U16_ag(T96, T97, T94, T95, deletec18_out_gaaa(T94, T96, T97, T102)) → U17_ag(T96, T97, T94, T95, permc35_in_ag(T102, T95))
U17_ag(T96, T97, T94, T95, permc35_out_ag(T102, T95)) → permc35_out_ag(.(T96, .(T97, [])), .(T94, .(T95, [])))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
[]  =  []
delete18_in_gaaa(x1, x2, x3, x4)  =  delete18_in_gaaa(x1)
delete26_in_gaa(x1, x2, x3)  =  delete26_in_gaa(x1)
deletec18_in_gaaa(x1, x2, x3, x4)  =  deletec18_in_gaaa(x1)
deletec18_out_gaaa(x1, x2, x3, x4)  =  deletec18_out_gaaa(x1)
U15_gaaa(x1, x2, x3, x4, x5)  =  U15_gaaa(x1, x5)
deletec26_in_gaa(x1, x2, x3)  =  deletec26_in_gaa(x1)
deletec26_out_gaa(x1, x2, x3)  =  deletec26_out_gaa(x1)
U14_gaa(x1, x2, x3, x4, x5)  =  U14_gaa(x1, x5)
perm35_in_ag(x1, x2)  =  perm35_in_ag(x2)
permc35_in_ag(x1, x2)  =  permc35_in_ag(x2)
permc35_out_ag(x1, x2)  =  permc35_out_ag(x2)
U16_ag(x1, x2, x3, x4, x5)  =  U16_ag(x3, x4, x5)
U17_ag(x1, x2, x3, x4, x5)  =  U17_ag(x3, x4, x5)
le51_in_gg(x1, x2)  =  le51_in_gg(x1, x2)
s(x1)  =  s(x1)
SLOWSORT1_IN_AG(x1, x2)  =  SLOWSORT1_IN_AG(x2)
U7_AG(x1, x2, x3, x4, x5)  =  U7_AG(x3, x4, x5)
DELETE18_IN_GAAA(x1, x2, x3, x4)  =  DELETE18_IN_GAAA(x1)
U2_GAAA(x1, x2, x3, x4, x5)  =  U2_GAAA(x1, x5)
DELETE26_IN_GAA(x1, x2, x3)  =  DELETE26_IN_GAA(x1)
U1_GAA(x1, x2, x3, x4, x5)  =  U1_GAA(x1, x5)
U8_AG(x1, x2, x3, x4, x5)  =  U8_AG(x3, x4, x5)
U9_AG(x1, x2, x3, x4, x5)  =  U9_AG(x3, x4, x5)
PERM35_IN_AG(x1, x2)  =  PERM35_IN_AG(x2)
U3_AG(x1, x2, x3, x4, x5)  =  U3_AG(x3, x4, x5)
U4_AG(x1, x2, x3, x4, x5)  =  U4_AG(x3, x4, x5)
U5_AG(x1, x2, x3, x4, x5)  =  U5_AG(x3, x4, x5)
U10_AG(x1, x2, x3, x4, x5)  =  U10_AG(x3, x4, x5)
U11_AG(x1, x2, x3, x4, x5)  =  U11_AG(x3, x4, x5)
U12_AG(x1, x2, x3, x4, x5)  =  U12_AG(x3, x4, 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_AG(.(T20, .(T21, [])), .(T18, .(T19, []))) → U7_AG(T20, T21, T18, T19, delete18_in_gaaa(T18, T20, T21, X22))
SLOWSORT1_IN_AG(.(T20, .(T21, [])), .(T18, .(T19, []))) → DELETE18_IN_GAAA(T18, T20, T21, X22)
DELETE18_IN_GAAA(T52, T53, T55, X65) → U2_GAAA(T52, T53, T55, X65, delete26_in_gaa(T52, T55, X65))
DELETE18_IN_GAAA(T52, T53, T55, X65) → DELETE26_IN_GAA(T52, T55, X65)
DELETE26_IN_GAA(T76, .(T77, T79), X96) → U1_GAA(T76, T77, T79, X96, delete26_in_gaa(T76, T79, X96))
DELETE26_IN_GAA(T76, .(T77, T79), X96) → DELETE26_IN_GAA(T76, T79, X96)
SLOWSORT1_IN_AG(.(T20, .(T21, [])), .(T18, .(T19, []))) → U8_AG(T20, T21, T18, T19, deletec18_in_gaaa(T18, T20, T21, T26))
U8_AG(T20, T21, T18, T19, deletec18_out_gaaa(T18, T20, T21, T26)) → U9_AG(T20, T21, T18, T19, perm35_in_ag(T26, T19))
U8_AG(T20, T21, T18, T19, deletec18_out_gaaa(T18, T20, T21, T26)) → PERM35_IN_AG(T26, T19)
PERM35_IN_AG(.(T96, .(T97, [])), .(T94, .(T95, []))) → U3_AG(T96, T97, T94, T95, delete18_in_gaaa(T94, T96, T97, X118))
PERM35_IN_AG(.(T96, .(T97, [])), .(T94, .(T95, []))) → DELETE18_IN_GAAA(T94, T96, T97, X118)
PERM35_IN_AG(.(T96, .(T97, [])), .(T94, .(T95, []))) → U4_AG(T96, T97, T94, T95, deletec18_in_gaaa(T94, T96, T97, T102))
U4_AG(T96, T97, T94, T95, deletec18_out_gaaa(T94, T96, T97, T102)) → U5_AG(T96, T97, T94, T95, perm35_in_ag(T102, T95))
U4_AG(T96, T97, T94, T95, deletec18_out_gaaa(T94, T96, T97, T102)) → PERM35_IN_AG(T102, T95)
SLOWSORT1_IN_AG(.(T20, .(T21, [])), .(T118, .(T119, []))) → U10_AG(T20, T21, T118, T119, deletec18_in_gaaa(T118, T20, T21, T26))
U10_AG(T20, T21, T118, T119, deletec18_out_gaaa(T118, T20, T21, T26)) → U11_AG(T20, T21, T118, T119, permc35_in_ag(T26, T119))
U11_AG(T20, T21, T118, T119, permc35_out_ag(T26, T119)) → U12_AG(T20, T21, T118, T119, le51_in_gg(T118, T119))
U11_AG(T20, T21, T118, T119, permc35_out_ag(T26, T119)) → LE51_IN_GG(T118, T119)
LE51_IN_GG(s(T132), s(T133)) → U6_GG(T132, T133, le51_in_gg(T132, T133))
LE51_IN_GG(s(T132), s(T133)) → LE51_IN_GG(T132, T133)

The TRS R consists of the following rules:

deletec18_in_gaaa(T39, T39, T40, T40) → deletec18_out_gaaa(T39, T39, T40, T40)
deletec18_in_gaaa(T52, T53, T55, X65) → U15_gaaa(T52, T53, T55, X65, deletec26_in_gaa(T52, T55, X65))
deletec26_in_gaa(T68, .(T68, T69), T69) → deletec26_out_gaa(T68, .(T68, T69), T69)
deletec26_in_gaa(T76, .(T77, T79), X96) → U14_gaa(T76, T77, T79, X96, deletec26_in_gaa(T76, T79, X96))
U14_gaa(T76, T77, T79, X96, deletec26_out_gaa(T76, T79, X96)) → deletec26_out_gaa(T76, .(T77, T79), X96)
U15_gaaa(T52, T53, T55, X65, deletec26_out_gaa(T52, T55, X65)) → deletec18_out_gaaa(T52, T53, T55, X65)
permc35_in_ag([], []) → permc35_out_ag([], [])
permc35_in_ag(.(T96, .(T97, [])), .(T94, .(T95, []))) → U16_ag(T96, T97, T94, T95, deletec18_in_gaaa(T94, T96, T97, T102))
U16_ag(T96, T97, T94, T95, deletec18_out_gaaa(T94, T96, T97, T102)) → U17_ag(T96, T97, T94, T95, permc35_in_ag(T102, T95))
U17_ag(T96, T97, T94, T95, permc35_out_ag(T102, T95)) → permc35_out_ag(.(T96, .(T97, [])), .(T94, .(T95, [])))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
[]  =  []
delete18_in_gaaa(x1, x2, x3, x4)  =  delete18_in_gaaa(x1)
delete26_in_gaa(x1, x2, x3)  =  delete26_in_gaa(x1)
deletec18_in_gaaa(x1, x2, x3, x4)  =  deletec18_in_gaaa(x1)
deletec18_out_gaaa(x1, x2, x3, x4)  =  deletec18_out_gaaa(x1)
U15_gaaa(x1, x2, x3, x4, x5)  =  U15_gaaa(x1, x5)
deletec26_in_gaa(x1, x2, x3)  =  deletec26_in_gaa(x1)
deletec26_out_gaa(x1, x2, x3)  =  deletec26_out_gaa(x1)
U14_gaa(x1, x2, x3, x4, x5)  =  U14_gaa(x1, x5)
perm35_in_ag(x1, x2)  =  perm35_in_ag(x2)
permc35_in_ag(x1, x2)  =  permc35_in_ag(x2)
permc35_out_ag(x1, x2)  =  permc35_out_ag(x2)
U16_ag(x1, x2, x3, x4, x5)  =  U16_ag(x3, x4, x5)
U17_ag(x1, x2, x3, x4, x5)  =  U17_ag(x3, x4, x5)
le51_in_gg(x1, x2)  =  le51_in_gg(x1, x2)
s(x1)  =  s(x1)
SLOWSORT1_IN_AG(x1, x2)  =  SLOWSORT1_IN_AG(x2)
U7_AG(x1, x2, x3, x4, x5)  =  U7_AG(x3, x4, x5)
DELETE18_IN_GAAA(x1, x2, x3, x4)  =  DELETE18_IN_GAAA(x1)
U2_GAAA(x1, x2, x3, x4, x5)  =  U2_GAAA(x1, x5)
DELETE26_IN_GAA(x1, x2, x3)  =  DELETE26_IN_GAA(x1)
U1_GAA(x1, x2, x3, x4, x5)  =  U1_GAA(x1, x5)
U8_AG(x1, x2, x3, x4, x5)  =  U8_AG(x3, x4, x5)
U9_AG(x1, x2, x3, x4, x5)  =  U9_AG(x3, x4, x5)
PERM35_IN_AG(x1, x2)  =  PERM35_IN_AG(x2)
U3_AG(x1, x2, x3, x4, x5)  =  U3_AG(x3, x4, x5)
U4_AG(x1, x2, x3, x4, x5)  =  U4_AG(x3, x4, x5)
U5_AG(x1, x2, x3, x4, x5)  =  U5_AG(x3, x4, x5)
U10_AG(x1, x2, x3, x4, x5)  =  U10_AG(x3, x4, x5)
U11_AG(x1, x2, x3, x4, x5)  =  U11_AG(x3, x4, x5)
U12_AG(x1, x2, x3, x4, x5)  =  U12_AG(x3, x4, 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(T132), s(T133)) → LE51_IN_GG(T132, T133)

The TRS R consists of the following rules:

deletec18_in_gaaa(T39, T39, T40, T40) → deletec18_out_gaaa(T39, T39, T40, T40)
deletec18_in_gaaa(T52, T53, T55, X65) → U15_gaaa(T52, T53, T55, X65, deletec26_in_gaa(T52, T55, X65))
deletec26_in_gaa(T68, .(T68, T69), T69) → deletec26_out_gaa(T68, .(T68, T69), T69)
deletec26_in_gaa(T76, .(T77, T79), X96) → U14_gaa(T76, T77, T79, X96, deletec26_in_gaa(T76, T79, X96))
U14_gaa(T76, T77, T79, X96, deletec26_out_gaa(T76, T79, X96)) → deletec26_out_gaa(T76, .(T77, T79), X96)
U15_gaaa(T52, T53, T55, X65, deletec26_out_gaa(T52, T55, X65)) → deletec18_out_gaaa(T52, T53, T55, X65)
permc35_in_ag([], []) → permc35_out_ag([], [])
permc35_in_ag(.(T96, .(T97, [])), .(T94, .(T95, []))) → U16_ag(T96, T97, T94, T95, deletec18_in_gaaa(T94, T96, T97, T102))
U16_ag(T96, T97, T94, T95, deletec18_out_gaaa(T94, T96, T97, T102)) → U17_ag(T96, T97, T94, T95, permc35_in_ag(T102, T95))
U17_ag(T96, T97, T94, T95, permc35_out_ag(T102, T95)) → permc35_out_ag(.(T96, .(T97, [])), .(T94, .(T95, [])))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
[]  =  []
deletec18_in_gaaa(x1, x2, x3, x4)  =  deletec18_in_gaaa(x1)
deletec18_out_gaaa(x1, x2, x3, x4)  =  deletec18_out_gaaa(x1)
U15_gaaa(x1, x2, x3, x4, x5)  =  U15_gaaa(x1, x5)
deletec26_in_gaa(x1, x2, x3)  =  deletec26_in_gaa(x1)
deletec26_out_gaa(x1, x2, x3)  =  deletec26_out_gaa(x1)
U14_gaa(x1, x2, x3, x4, x5)  =  U14_gaa(x1, x5)
permc35_in_ag(x1, x2)  =  permc35_in_ag(x2)
permc35_out_ag(x1, x2)  =  permc35_out_ag(x2)
U16_ag(x1, x2, x3, x4, x5)  =  U16_ag(x3, x4, x5)
U17_ag(x1, x2, x3, x4, x5)  =  U17_ag(x3, x4, 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(T132), s(T133)) → LE51_IN_GG(T132, T133)

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(T132), s(T133)) → LE51_IN_GG(T132, T133)

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(T132), s(T133)) → LE51_IN_GG(T132, T133)
    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_GAA(T76, .(T77, T79), X96) → DELETE26_IN_GAA(T76, T79, X96)

The TRS R consists of the following rules:

deletec18_in_gaaa(T39, T39, T40, T40) → deletec18_out_gaaa(T39, T39, T40, T40)
deletec18_in_gaaa(T52, T53, T55, X65) → U15_gaaa(T52, T53, T55, X65, deletec26_in_gaa(T52, T55, X65))
deletec26_in_gaa(T68, .(T68, T69), T69) → deletec26_out_gaa(T68, .(T68, T69), T69)
deletec26_in_gaa(T76, .(T77, T79), X96) → U14_gaa(T76, T77, T79, X96, deletec26_in_gaa(T76, T79, X96))
U14_gaa(T76, T77, T79, X96, deletec26_out_gaa(T76, T79, X96)) → deletec26_out_gaa(T76, .(T77, T79), X96)
U15_gaaa(T52, T53, T55, X65, deletec26_out_gaa(T52, T55, X65)) → deletec18_out_gaaa(T52, T53, T55, X65)
permc35_in_ag([], []) → permc35_out_ag([], [])
permc35_in_ag(.(T96, .(T97, [])), .(T94, .(T95, []))) → U16_ag(T96, T97, T94, T95, deletec18_in_gaaa(T94, T96, T97, T102))
U16_ag(T96, T97, T94, T95, deletec18_out_gaaa(T94, T96, T97, T102)) → U17_ag(T96, T97, T94, T95, permc35_in_ag(T102, T95))
U17_ag(T96, T97, T94, T95, permc35_out_ag(T102, T95)) → permc35_out_ag(.(T96, .(T97, [])), .(T94, .(T95, [])))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
[]  =  []
deletec18_in_gaaa(x1, x2, x3, x4)  =  deletec18_in_gaaa(x1)
deletec18_out_gaaa(x1, x2, x3, x4)  =  deletec18_out_gaaa(x1)
U15_gaaa(x1, x2, x3, x4, x5)  =  U15_gaaa(x1, x5)
deletec26_in_gaa(x1, x2, x3)  =  deletec26_in_gaa(x1)
deletec26_out_gaa(x1, x2, x3)  =  deletec26_out_gaa(x1)
U14_gaa(x1, x2, x3, x4, x5)  =  U14_gaa(x1, x5)
permc35_in_ag(x1, x2)  =  permc35_in_ag(x2)
permc35_out_ag(x1, x2)  =  permc35_out_ag(x2)
U16_ag(x1, x2, x3, x4, x5)  =  U16_ag(x3, x4, x5)
U17_ag(x1, x2, x3, x4, x5)  =  U17_ag(x3, x4, x5)
DELETE26_IN_GAA(x1, x2, x3)  =  DELETE26_IN_GAA(x1)

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_GAA(T76, .(T77, T79), X96) → DELETE26_IN_GAA(T76, T79, X96)

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

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_GAA(T76) → DELETE26_IN_GAA(T76)

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

(19) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

s = DELETE26_IN_GAA(T76) evaluates to t =DELETE26_IN_GAA(T76)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Matcher: [ ]
  • Semiunifier: [ ]




Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from DELETE26_IN_GAA(T76) to DELETE26_IN_GAA(T76).



(20) NO

(21) Obligation:

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

PERM35_IN_AG(.(T96, .(T97, [])), .(T94, .(T95, []))) → U4_AG(T96, T97, T94, T95, deletec18_in_gaaa(T94, T96, T97, T102))
U4_AG(T96, T97, T94, T95, deletec18_out_gaaa(T94, T96, T97, T102)) → PERM35_IN_AG(T102, T95)

The TRS R consists of the following rules:

deletec18_in_gaaa(T39, T39, T40, T40) → deletec18_out_gaaa(T39, T39, T40, T40)
deletec18_in_gaaa(T52, T53, T55, X65) → U15_gaaa(T52, T53, T55, X65, deletec26_in_gaa(T52, T55, X65))
deletec26_in_gaa(T68, .(T68, T69), T69) → deletec26_out_gaa(T68, .(T68, T69), T69)
deletec26_in_gaa(T76, .(T77, T79), X96) → U14_gaa(T76, T77, T79, X96, deletec26_in_gaa(T76, T79, X96))
U14_gaa(T76, T77, T79, X96, deletec26_out_gaa(T76, T79, X96)) → deletec26_out_gaa(T76, .(T77, T79), X96)
U15_gaaa(T52, T53, T55, X65, deletec26_out_gaa(T52, T55, X65)) → deletec18_out_gaaa(T52, T53, T55, X65)
permc35_in_ag([], []) → permc35_out_ag([], [])
permc35_in_ag(.(T96, .(T97, [])), .(T94, .(T95, []))) → U16_ag(T96, T97, T94, T95, deletec18_in_gaaa(T94, T96, T97, T102))
U16_ag(T96, T97, T94, T95, deletec18_out_gaaa(T94, T96, T97, T102)) → U17_ag(T96, T97, T94, T95, permc35_in_ag(T102, T95))
U17_ag(T96, T97, T94, T95, permc35_out_ag(T102, T95)) → permc35_out_ag(.(T96, .(T97, [])), .(T94, .(T95, [])))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
[]  =  []
deletec18_in_gaaa(x1, x2, x3, x4)  =  deletec18_in_gaaa(x1)
deletec18_out_gaaa(x1, x2, x3, x4)  =  deletec18_out_gaaa(x1)
U15_gaaa(x1, x2, x3, x4, x5)  =  U15_gaaa(x1, x5)
deletec26_in_gaa(x1, x2, x3)  =  deletec26_in_gaa(x1)
deletec26_out_gaa(x1, x2, x3)  =  deletec26_out_gaa(x1)
U14_gaa(x1, x2, x3, x4, x5)  =  U14_gaa(x1, x5)
permc35_in_ag(x1, x2)  =  permc35_in_ag(x2)
permc35_out_ag(x1, x2)  =  permc35_out_ag(x2)
U16_ag(x1, x2, x3, x4, x5)  =  U16_ag(x3, x4, x5)
U17_ag(x1, x2, x3, x4, x5)  =  U17_ag(x3, x4, x5)
PERM35_IN_AG(x1, x2)  =  PERM35_IN_AG(x2)
U4_AG(x1, x2, x3, x4, x5)  =  U4_AG(x3, x4, 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_AG(.(T96, .(T97, [])), .(T94, .(T95, []))) → U4_AG(T96, T97, T94, T95, deletec18_in_gaaa(T94, T96, T97, T102))
U4_AG(T96, T97, T94, T95, deletec18_out_gaaa(T94, T96, T97, T102)) → PERM35_IN_AG(T102, T95)

The TRS R consists of the following rules:

deletec18_in_gaaa(T39, T39, T40, T40) → deletec18_out_gaaa(T39, T39, T40, T40)
deletec18_in_gaaa(T52, T53, T55, X65) → U15_gaaa(T52, T53, T55, X65, deletec26_in_gaa(T52, T55, X65))
U15_gaaa(T52, T53, T55, X65, deletec26_out_gaa(T52, T55, X65)) → deletec18_out_gaaa(T52, T53, T55, X65)
deletec26_in_gaa(T68, .(T68, T69), T69) → deletec26_out_gaa(T68, .(T68, T69), T69)
deletec26_in_gaa(T76, .(T77, T79), X96) → U14_gaa(T76, T77, T79, X96, deletec26_in_gaa(T76, T79, X96))
U14_gaa(T76, T77, T79, X96, deletec26_out_gaa(T76, T79, X96)) → deletec26_out_gaa(T76, .(T77, T79), X96)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
[]  =  []
deletec18_in_gaaa(x1, x2, x3, x4)  =  deletec18_in_gaaa(x1)
deletec18_out_gaaa(x1, x2, x3, x4)  =  deletec18_out_gaaa(x1)
U15_gaaa(x1, x2, x3, x4, x5)  =  U15_gaaa(x1, x5)
deletec26_in_gaa(x1, x2, x3)  =  deletec26_in_gaa(x1)
deletec26_out_gaa(x1, x2, x3)  =  deletec26_out_gaa(x1)
U14_gaa(x1, x2, x3, x4, x5)  =  U14_gaa(x1, x5)
PERM35_IN_AG(x1, x2)  =  PERM35_IN_AG(x2)
U4_AG(x1, x2, x3, x4, x5)  =  U4_AG(x3, x4, 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_AG(.(T94, .(T95, []))) → U4_AG(T94, T95, deletec18_in_gaaa(T94))
U4_AG(T94, T95, deletec18_out_gaaa(T94)) → PERM35_IN_AG(T95)

The TRS R consists of the following rules:

deletec18_in_gaaa(T39) → deletec18_out_gaaa(T39)
deletec18_in_gaaa(T52) → U15_gaaa(T52, deletec26_in_gaa(T52))
U15_gaaa(T52, deletec26_out_gaa(T52)) → deletec18_out_gaaa(T52)
deletec26_in_gaa(T68) → deletec26_out_gaa(T68)
deletec26_in_gaa(T76) → U14_gaa(T76, deletec26_in_gaa(T76))
U14_gaa(T76, deletec26_out_gaa(T76)) → deletec26_out_gaa(T76)

The set Q consists of the following terms:

deletec18_in_gaaa(x0)
U15_gaaa(x0, x1)
deletec26_in_gaa(x0)
U14_gaa(x0, x1)

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:

  • U4_AG(T94, T95, deletec18_out_gaaa(T94)) → PERM35_IN_AG(T95)
    The graph contains the following edges 2 >= 1

  • PERM35_IN_AG(.(T94, .(T95, []))) → U4_AG(T94, T95, deletec18_in_gaaa(T94))
    The graph contains the following edges 1 > 1, 1 > 2

(27) YES