Left Termination proof of /tmp/tmpSsN4d9/slowsort-oi.pl

Left Termination of the query pattern sort(f,b) w.r.t. the given Prolog program could not be shown:

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

sort₂(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₀).

With regard to the inferred argument filtering the predicates were used in the following modes:
sort₂: (f,b)
perm₂: (f,b) (f,f)
delete₃: (f,b,f) (f,f,f)
sorted₁: (b)
le₂: (f,f)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

sort_2_in_ag₂(X, Y) -> if_sort_2_in_1_ag₃(X, Y, perm_2_in_ag₂(X, Y))
perm_2_in_ag₂([]_0, []_0) -> perm_2_out_ag₂([]_0, []_0)
perm_2_in_ag₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> if_perm_2_in_1_ag₅(X, Y, U, V, delete_3_in_aga₃(U, ._2₂(X, Y), Z))
delete_3_in_aga₃(X, ._2₂(X, Y), Y) -> delete_3_out_aga₃(X, ._2₂(X, Y), Y)
delete_3_in_aga₃(X, ._2₂(Y, Z), W) -> if_delete_3_in_1_aga₅(X, Y, Z, W, delete_3_in_aaa₃(X, Z, W))
delete_3_in_aaa₃(X, ._2₂(X, Y), Y) -> delete_3_out_aaa₃(X, ._2₂(X, Y), Y)
delete_3_in_aaa₃(X, ._2₂(Y, Z), W) -> if_delete_3_in_1_aaa₅(X, Y, Z, W, delete_3_in_aaa₃(X, Z, W))
if_delete_3_in_1_aaa₅(X, Y, Z, W, delete_3_out_aaa₃(X, Z, W)) -> delete_3_out_aaa₃(X, ._2₂(Y, Z), W)
if_delete_3_in_1_aga₅(X, Y, Z, W, delete_3_out_aaa₃(X, Z, W)) -> delete_3_out_aga₃(X, ._2₂(Y, Z), W)
if_perm_2_in_1_ag₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> if_perm_2_in_2_ag₆(X, Y, U, V, Z, perm_2_in_aa₂(Z, V))
perm_2_in_aa₂([]_0, []_0) -> perm_2_out_aa₂([]_0, []_0)
perm_2_in_aa₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> if_perm_2_in_1_aa₅(X, Y, U, V, delete_3_in_aga₃(U, ._2₂(X, Y), Z))
if_perm_2_in_1_aa₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> if_perm_2_in_2_aa₆(X, Y, U, V, Z, perm_2_in_aa₂(Z, V))
if_perm_2_in_2_aa₆(X, Y, U, V, Z, perm_2_out_aa₂(Z, V)) -> perm_2_out_aa₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0)))
if_perm_2_in_2_ag₆(X, Y, U, V, Z, perm_2_out_aa₂(Z, V)) -> perm_2_out_ag₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0)))
if_sort_2_in_1_ag₃(X, Y, perm_2_out_ag₂(X, Y)) -> if_sort_2_in_2_ag₃(X, Y, sorted_1_in_g₁(Y))
sorted_1_in_g₁([]_0) -> sorted_1_out_g₁([]_0)
sorted_1_in_g₁(._2₂(X, []_0)) -> sorted_1_out_g₁(._2₂(X, []_0))
sorted_1_in_g₁(._2₂(X, ._2₂(Y, Z))) -> if_sorted_1_in_1_g₄(X, Y, Z, le_2_in_aa₂(X, Y))
le_2_in_aa₂(s_1₁(X), s_1₁(Y)) -> if_le_2_in_1_aa₃(X, Y, le_2_in_aa₂(X, Y))
le_2_in_aa₂(0_0, s_1₁(X)) -> le_2_out_aa₂(0_0, s_1₁(X))
le_2_in_aa₂(0_0, 0_0) -> le_2_out_aa₂(0_0, 0_0)
if_le_2_in_1_aa₃(X, Y, le_2_out_aa₂(X, Y)) -> le_2_out_aa₂(s_1₁(X), s_1₁(Y))
if_sorted_1_in_1_g₄(X, Y, Z, le_2_out_aa₂(X, Y)) -> if_sorted_1_in_2_g₄(X, Y, Z, sorted_1_in_g₁(._2₂(Y, Z)))
if_sorted_1_in_2_g₄(X, Y, Z, sorted_1_out_g₁(._2₂(Y, Z))) -> sorted_1_out_g₁(._2₂(X, ._2₂(Y, Z)))
if_sort_2_in_2_ag₃(X, Y, sorted_1_out_g₁(Y)) -> sort_2_out_ag₂(X, Y)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

  ↳ PrologToPiTRSProof

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

sort_2_in_ag₂(X, Y) -> if_sort_2_in_1_ag₃(X, Y, perm_2_in_ag₂(X, Y))
perm_2_in_ag₂([]_0, []_0) -> perm_2_out_ag₂([]_0, []_0)
perm_2_in_ag₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> if_perm_2_in_1_ag₅(X, Y, U, V, delete_3_in_aga₃(U, ._2₂(X, Y), Z))
delete_3_in_aga₃(X, ._2₂(X, Y), Y) -> delete_3_out_aga₃(X, ._2₂(X, Y), Y)
delete_3_in_aga₃(X, ._2₂(Y, Z), W) -> if_delete_3_in_1_aga₅(X, Y, Z, W, delete_3_in_aaa₃(X, Z, W))
delete_3_in_aaa₃(X, ._2₂(X, Y), Y) -> delete_3_out_aaa₃(X, ._2₂(X, Y), Y)
delete_3_in_aaa₃(X, ._2₂(Y, Z), W) -> if_delete_3_in_1_aaa₅(X, Y, Z, W, delete_3_in_aaa₃(X, Z, W))
if_delete_3_in_1_aaa₅(X, Y, Z, W, delete_3_out_aaa₃(X, Z, W)) -> delete_3_out_aaa₃(X, ._2₂(Y, Z), W)
if_delete_3_in_1_aga₅(X, Y, Z, W, delete_3_out_aaa₃(X, Z, W)) -> delete_3_out_aga₃(X, ._2₂(Y, Z), W)
if_perm_2_in_1_ag₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> if_perm_2_in_2_ag₆(X, Y, U, V, Z, perm_2_in_aa₂(Z, V))
perm_2_in_aa₂([]_0, []_0) -> perm_2_out_aa₂([]_0, []_0)
perm_2_in_aa₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> if_perm_2_in_1_aa₅(X, Y, U, V, delete_3_in_aga₃(U, ._2₂(X, Y), Z))
if_perm_2_in_1_aa₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> if_perm_2_in_2_aa₆(X, Y, U, V, Z, perm_2_in_aa₂(Z, V))
if_perm_2_in_2_aa₆(X, Y, U, V, Z, perm_2_out_aa₂(Z, V)) -> perm_2_out_aa₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0)))
if_perm_2_in_2_ag₆(X, Y, U, V, Z, perm_2_out_aa₂(Z, V)) -> perm_2_out_ag₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0)))
if_sort_2_in_1_ag₃(X, Y, perm_2_out_ag₂(X, Y)) -> if_sort_2_in_2_ag₃(X, Y, sorted_1_in_g₁(Y))
sorted_1_in_g₁([]_0) -> sorted_1_out_g₁([]_0)
sorted_1_in_g₁(._2₂(X, []_0)) -> sorted_1_out_g₁(._2₂(X, []_0))
sorted_1_in_g₁(._2₂(X, ._2₂(Y, Z))) -> if_sorted_1_in_1_g₄(X, Y, Z, le_2_in_aa₂(X, Y))
le_2_in_aa₂(s_1₁(X), s_1₁(Y)) -> if_le_2_in_1_aa₃(X, Y, le_2_in_aa₂(X, Y))
le_2_in_aa₂(0_0, s_1₁(X)) -> le_2_out_aa₂(0_0, s_1₁(X))
le_2_in_aa₂(0_0, 0_0) -> le_2_out_aa₂(0_0, 0_0)
if_le_2_in_1_aa₃(X, Y, le_2_out_aa₂(X, Y)) -> le_2_out_aa₂(s_1₁(X), s_1₁(Y))
if_sorted_1_in_1_g₄(X, Y, Z, le_2_out_aa₂(X, Y)) -> if_sorted_1_in_2_g₄(X, Y, Z, sorted_1_in_g₁(._2₂(Y, Z)))
if_sorted_1_in_2_g₄(X, Y, Z, sorted_1_out_g₁(._2₂(Y, Z))) -> sorted_1_out_g₁(._2₂(X, ._2₂(Y, Z)))
if_sort_2_in_2_ag₃(X, Y, sorted_1_out_g₁(Y)) -> sort_2_out_ag₂(X, Y)

SORT_2_IN_AG₂(X, Y) -> IF_SORT_2_IN_1_AG₃(X, Y, perm_2_in_ag₂(X, Y))
SORT_2_IN_AG₂(X, Y) -> PERM_2_IN_AG₂(X, Y)
PERM_2_IN_AG₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> IF_PERM_2_IN_1_AG₅(X, Y, U, V, delete_3_in_aga₃(U, ._2₂(X, Y), Z))
PERM_2_IN_AG₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> DELETE_3_IN_AGA₃(U, ._2₂(X, Y), Z)
DELETE_3_IN_AGA₃(X, ._2₂(Y, Z), W) -> IF_DELETE_3_IN_1_AGA₅(X, Y, Z, W, delete_3_in_aaa₃(X, Z, W))
DELETE_3_IN_AGA₃(X, ._2₂(Y, Z), W) -> DELETE_3_IN_AAA₃(X, Z, W)
DELETE_3_IN_AAA₃(X, ._2₂(Y, Z), W) -> IF_DELETE_3_IN_1_AAA₅(X, Y, Z, W, delete_3_in_aaa₃(X, Z, W))
DELETE_3_IN_AAA₃(X, ._2₂(Y, Z), W) -> DELETE_3_IN_AAA₃(X, Z, W)
IF_PERM_2_IN_1_AG₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> IF_PERM_2_IN_2_AG₆(X, Y, U, V, Z, perm_2_in_aa₂(Z, V))
IF_PERM_2_IN_1_AG₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> PERM_2_IN_AA₂(Z, V)
PERM_2_IN_AA₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> IF_PERM_2_IN_1_AA₅(X, Y, U, V, delete_3_in_aga₃(U, ._2₂(X, Y), Z))
PERM_2_IN_AA₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> DELETE_3_IN_AGA₃(U, ._2₂(X, Y), Z)
IF_PERM_2_IN_1_AA₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> IF_PERM_2_IN_2_AA₆(X, Y, U, V, Z, perm_2_in_aa₂(Z, V))
IF_PERM_2_IN_1_AA₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> PERM_2_IN_AA₂(Z, V)
IF_SORT_2_IN_1_AG₃(X, Y, perm_2_out_ag₂(X, Y)) -> IF_SORT_2_IN_2_AG₃(X, Y, sorted_1_in_g₁(Y))
IF_SORT_2_IN_1_AG₃(X, Y, perm_2_out_ag₂(X, Y)) -> SORTED_1_IN_G₁(Y)
SORTED_1_IN_G₁(._2₂(X, ._2₂(Y, Z))) -> IF_SORTED_1_IN_1_G₄(X, Y, Z, le_2_in_aa₂(X, Y))
SORTED_1_IN_G₁(._2₂(X, ._2₂(Y, Z))) -> LE_2_IN_AA₂(X, Y)
LE_2_IN_AA₂(s_1₁(X), s_1₁(Y)) -> IF_LE_2_IN_1_AA₃(X, Y, le_2_in_aa₂(X, Y))
LE_2_IN_AA₂(s_1₁(X), s_1₁(Y)) -> LE_2_IN_AA₂(X, Y)
IF_SORTED_1_IN_1_G₄(X, Y, Z, le_2_out_aa₂(X, Y)) -> IF_SORTED_1_IN_2_G₄(X, Y, Z, sorted_1_in_g₁(._2₂(Y, Z)))
IF_SORTED_1_IN_1_G₄(X, Y, Z, le_2_out_aa₂(X, Y)) -> SORTED_1_IN_G₁(._2₂(Y, Z))

The TRS R consists of the following rules:

sort_2_in_ag₂(X, Y) -> if_sort_2_in_1_ag₃(X, Y, perm_2_in_ag₂(X, Y))
perm_2_in_ag₂([]_0, []_0) -> perm_2_out_ag₂([]_0, []_0)
perm_2_in_ag₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> if_perm_2_in_1_ag₅(X, Y, U, V, delete_3_in_aga₃(U, ._2₂(X, Y), Z))
delete_3_in_aga₃(X, ._2₂(X, Y), Y) -> delete_3_out_aga₃(X, ._2₂(X, Y), Y)
delete_3_in_aga₃(X, ._2₂(Y, Z), W) -> if_delete_3_in_1_aga₅(X, Y, Z, W, delete_3_in_aaa₃(X, Z, W))
delete_3_in_aaa₃(X, ._2₂(X, Y), Y) -> delete_3_out_aaa₃(X, ._2₂(X, Y), Y)
delete_3_in_aaa₃(X, ._2₂(Y, Z), W) -> if_delete_3_in_1_aaa₅(X, Y, Z, W, delete_3_in_aaa₃(X, Z, W))
if_delete_3_in_1_aaa₅(X, Y, Z, W, delete_3_out_aaa₃(X, Z, W)) -> delete_3_out_aaa₃(X, ._2₂(Y, Z), W)
if_delete_3_in_1_aga₅(X, Y, Z, W, delete_3_out_aaa₃(X, Z, W)) -> delete_3_out_aga₃(X, ._2₂(Y, Z), W)
if_perm_2_in_1_ag₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> if_perm_2_in_2_ag₆(X, Y, U, V, Z, perm_2_in_aa₂(Z, V))
perm_2_in_aa₂([]_0, []_0) -> perm_2_out_aa₂([]_0, []_0)
perm_2_in_aa₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> if_perm_2_in_1_aa₅(X, Y, U, V, delete_3_in_aga₃(U, ._2₂(X, Y), Z))
if_perm_2_in_1_aa₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> if_perm_2_in_2_aa₆(X, Y, U, V, Z, perm_2_in_aa₂(Z, V))
if_perm_2_in_2_aa₆(X, Y, U, V, Z, perm_2_out_aa₂(Z, V)) -> perm_2_out_aa₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0)))
if_perm_2_in_2_ag₆(X, Y, U, V, Z, perm_2_out_aa₂(Z, V)) -> perm_2_out_ag₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0)))
if_sort_2_in_1_ag₃(X, Y, perm_2_out_ag₂(X, Y)) -> if_sort_2_in_2_ag₃(X, Y, sorted_1_in_g₁(Y))
sorted_1_in_g₁([]_0) -> sorted_1_out_g₁([]_0)
sorted_1_in_g₁(._2₂(X, []_0)) -> sorted_1_out_g₁(._2₂(X, []_0))
sorted_1_in_g₁(._2₂(X, ._2₂(Y, Z))) -> if_sorted_1_in_1_g₄(X, Y, Z, le_2_in_aa₂(X, Y))
le_2_in_aa₂(s_1₁(X), s_1₁(Y)) -> if_le_2_in_1_aa₃(X, Y, le_2_in_aa₂(X, Y))
le_2_in_aa₂(0_0, s_1₁(X)) -> le_2_out_aa₂(0_0, s_1₁(X))
le_2_in_aa₂(0_0, 0_0) -> le_2_out_aa₂(0_0, 0_0)
if_le_2_in_1_aa₃(X, Y, le_2_out_aa₂(X, Y)) -> le_2_out_aa₂(s_1₁(X), s_1₁(Y))
if_sorted_1_in_1_g₄(X, Y, Z, le_2_out_aa₂(X, Y)) -> if_sorted_1_in_2_g₄(X, Y, Z, sorted_1_in_g₁(._2₂(Y, Z)))
if_sorted_1_in_2_g₄(X, Y, Z, sorted_1_out_g₁(._2₂(Y, Z))) -> sorted_1_out_g₁(._2₂(X, ._2₂(Y, Z)))
if_sort_2_in_2_ag₃(X, Y, sorted_1_out_g₁(Y)) -> sort_2_out_ag₂(X, Y)

The argument filtering Pi contains the following mapping:
sort_2_in_ag₂(x1, x2) = sort_2_in_ag₁(x2)
[]_0 = []_0
._2₂(x1, x2) = ._2
s_1₁(x1) = s_1
0_0 = 0_0
if_sort_2_in_1_ag₃(x1, x2, x3) = if_sort_2_in_1_ag₂(x2, x3)
perm_2_in_ag₂(x1, x2) = perm_2_in_ag₁(x2)
perm_2_out_ag₂(x1, x2) = perm_2_out_ag₁(x1)
if_perm_2_in_1_ag₅(x1, x2, x3, x4, x5) = if_perm_2_in_1_ag₁(x5)
delete_3_in_aga₃(x1, x2, x3) = delete_3_in_aga₁(x2)
delete_3_out_aga₃(x1, x2, x3) = delete_3_out_aga
if_delete_3_in_1_aga₅(x1, x2, x3, x4, x5) = if_delete_3_in_1_aga₁(x5)
delete_3_in_aaa₃(x1, x2, x3) = delete_3_in_aaa
delete_3_out_aaa₃(x1, x2, x3) = delete_3_out_aaa₁(x2)
if_delete_3_in_1_aaa₅(x1, x2, x3, x4, x5) = if_delete_3_in_1_aaa₁(x5)
if_perm_2_in_2_ag₆(x1, x2, x3, x4, x5, x6) = if_perm_2_in_2_ag₁(x6)
perm_2_in_aa₂(x1, x2) = perm_2_in_aa
perm_2_out_aa₂(x1, x2) = perm_2_out_aa₂(x1, x2)
if_perm_2_in_1_aa₅(x1, x2, x3, x4, x5) = if_perm_2_in_1_aa₁(x5)
if_perm_2_in_2_aa₆(x1, x2, x3, x4, x5, x6) = if_perm_2_in_2_aa₁(x6)
if_sort_2_in_2_ag₃(x1, x2, x3) = if_sort_2_in_2_ag₂(x1, x3)
sorted_1_in_g₁(x1) = sorted_1_in_g₁(x1)
sorted_1_out_g₁(x1) = sorted_1_out_g
if_sorted_1_in_1_g₄(x1, x2, x3, x4) = if_sorted_1_in_1_g₁(x4)
le_2_in_aa₂(x1, x2) = le_2_in_aa
if_le_2_in_1_aa₃(x1, x2, x3) = if_le_2_in_1_aa₁(x3)
le_2_out_aa₂(x1, x2) = le_2_out_aa₂(x1, x2)
if_sorted_1_in_2_g₄(x1, x2, x3, x4) = if_sorted_1_in_2_g₁(x4)
sort_2_out_ag₂(x1, x2) = sort_2_out_ag₁(x1)
IF_DELETE_3_IN_1_AAA₅(x1, x2, x3, x4, x5) = IF_DELETE_3_IN_1_AAA₁(x5)
IF_SORTED_1_IN_2_G₄(x1, x2, x3, x4) = IF_SORTED_1_IN_2_G₁(x4)
IF_SORT_2_IN_2_AG₃(x1, x2, x3) = IF_SORT_2_IN_2_AG₂(x1, x3)
IF_SORT_2_IN_1_AG₃(x1, x2, x3) = IF_SORT_2_IN_1_AG₂(x2, x3)
PERM_2_IN_AG₂(x1, x2) = PERM_2_IN_AG₁(x2)
IF_DELETE_3_IN_1_AGA₅(x1, x2, x3, x4, x5) = IF_DELETE_3_IN_1_AGA₁(x5)
IF_PERM_2_IN_2_AA₆(x1, x2, x3, x4, x5, x6) = IF_PERM_2_IN_2_AA₁(x6)
PERM_2_IN_AA₂(x1, x2) = PERM_2_IN_AA
SORTED_1_IN_G₁(x1) = SORTED_1_IN_G₁(x1)
SORT_2_IN_AG₂(x1, x2) = SORT_2_IN_AG₁(x2)
LE_2_IN_AA₂(x1, x2) = LE_2_IN_AA
IF_LE_2_IN_1_AA₃(x1, x2, x3) = IF_LE_2_IN_1_AA₁(x3)
DELETE_3_IN_AGA₃(x1, x2, x3) = DELETE_3_IN_AGA₁(x2)
IF_PERM_2_IN_1_AG₅(x1, x2, x3, x4, x5) = IF_PERM_2_IN_1_AG₁(x5)
IF_PERM_2_IN_2_AG₆(x1, x2, x3, x4, x5, x6) = IF_PERM_2_IN_2_AG₁(x6)
IF_SORTED_1_IN_1_G₄(x1, x2, x3, x4) = IF_SORTED_1_IN_1_G₁(x4)
DELETE_3_IN_AAA₃(x1, x2, x3) = DELETE_3_IN_AAA
IF_PERM_2_IN_1_AA₅(x1, x2, x3, x4, x5) = IF_PERM_2_IN_1_AA₁(x5)

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

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

  ↳ PrologToPiTRSProof

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

SORT_2_IN_AG₂(X, Y) -> IF_SORT_2_IN_1_AG₃(X, Y, perm_2_in_ag₂(X, Y))
SORT_2_IN_AG₂(X, Y) -> PERM_2_IN_AG₂(X, Y)
PERM_2_IN_AG₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> IF_PERM_2_IN_1_AG₅(X, Y, U, V, delete_3_in_aga₃(U, ._2₂(X, Y), Z))
PERM_2_IN_AG₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> DELETE_3_IN_AGA₃(U, ._2₂(X, Y), Z)
DELETE_3_IN_AGA₃(X, ._2₂(Y, Z), W) -> IF_DELETE_3_IN_1_AGA₅(X, Y, Z, W, delete_3_in_aaa₃(X, Z, W))
DELETE_3_IN_AGA₃(X, ._2₂(Y, Z), W) -> DELETE_3_IN_AAA₃(X, Z, W)
DELETE_3_IN_AAA₃(X, ._2₂(Y, Z), W) -> IF_DELETE_3_IN_1_AAA₅(X, Y, Z, W, delete_3_in_aaa₃(X, Z, W))
DELETE_3_IN_AAA₃(X, ._2₂(Y, Z), W) -> DELETE_3_IN_AAA₃(X, Z, W)
IF_PERM_2_IN_1_AG₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> IF_PERM_2_IN_2_AG₆(X, Y, U, V, Z, perm_2_in_aa₂(Z, V))
IF_PERM_2_IN_1_AG₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> PERM_2_IN_AA₂(Z, V)
PERM_2_IN_AA₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> IF_PERM_2_IN_1_AA₅(X, Y, U, V, delete_3_in_aga₃(U, ._2₂(X, Y), Z))
PERM_2_IN_AA₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> DELETE_3_IN_AGA₃(U, ._2₂(X, Y), Z)
IF_PERM_2_IN_1_AA₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> IF_PERM_2_IN_2_AA₆(X, Y, U, V, Z, perm_2_in_aa₂(Z, V))
IF_PERM_2_IN_1_AA₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> PERM_2_IN_AA₂(Z, V)
IF_SORT_2_IN_1_AG₃(X, Y, perm_2_out_ag₂(X, Y)) -> IF_SORT_2_IN_2_AG₃(X, Y, sorted_1_in_g₁(Y))
IF_SORT_2_IN_1_AG₃(X, Y, perm_2_out_ag₂(X, Y)) -> SORTED_1_IN_G₁(Y)
SORTED_1_IN_G₁(._2₂(X, ._2₂(Y, Z))) -> IF_SORTED_1_IN_1_G₄(X, Y, Z, le_2_in_aa₂(X, Y))
SORTED_1_IN_G₁(._2₂(X, ._2₂(Y, Z))) -> LE_2_IN_AA₂(X, Y)
LE_2_IN_AA₂(s_1₁(X), s_1₁(Y)) -> IF_LE_2_IN_1_AA₃(X, Y, le_2_in_aa₂(X, Y))
LE_2_IN_AA₂(s_1₁(X), s_1₁(Y)) -> LE_2_IN_AA₂(X, Y)
IF_SORTED_1_IN_1_G₄(X, Y, Z, le_2_out_aa₂(X, Y)) -> IF_SORTED_1_IN_2_G₄(X, Y, Z, sorted_1_in_g₁(._2₂(Y, Z)))
IF_SORTED_1_IN_1_G₄(X, Y, Z, le_2_out_aa₂(X, Y)) -> SORTED_1_IN_G₁(._2₂(Y, Z))

The TRS R consists of the following rules:

sort_2_in_ag₂(X, Y) -> if_sort_2_in_1_ag₃(X, Y, perm_2_in_ag₂(X, Y))
perm_2_in_ag₂([]_0, []_0) -> perm_2_out_ag₂([]_0, []_0)
perm_2_in_ag₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> if_perm_2_in_1_ag₅(X, Y, U, V, delete_3_in_aga₃(U, ._2₂(X, Y), Z))
delete_3_in_aga₃(X, ._2₂(X, Y), Y) -> delete_3_out_aga₃(X, ._2₂(X, Y), Y)
delete_3_in_aga₃(X, ._2₂(Y, Z), W) -> if_delete_3_in_1_aga₅(X, Y, Z, W, delete_3_in_aaa₃(X, Z, W))
delete_3_in_aaa₃(X, ._2₂(X, Y), Y) -> delete_3_out_aaa₃(X, ._2₂(X, Y), Y)
delete_3_in_aaa₃(X, ._2₂(Y, Z), W) -> if_delete_3_in_1_aaa₅(X, Y, Z, W, delete_3_in_aaa₃(X, Z, W))
if_delete_3_in_1_aaa₅(X, Y, Z, W, delete_3_out_aaa₃(X, Z, W)) -> delete_3_out_aaa₃(X, ._2₂(Y, Z), W)
if_delete_3_in_1_aga₅(X, Y, Z, W, delete_3_out_aaa₃(X, Z, W)) -> delete_3_out_aga₃(X, ._2₂(Y, Z), W)
if_perm_2_in_1_ag₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> if_perm_2_in_2_ag₆(X, Y, U, V, Z, perm_2_in_aa₂(Z, V))
perm_2_in_aa₂([]_0, []_0) -> perm_2_out_aa₂([]_0, []_0)
perm_2_in_aa₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> if_perm_2_in_1_aa₅(X, Y, U, V, delete_3_in_aga₃(U, ._2₂(X, Y), Z))
if_perm_2_in_1_aa₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> if_perm_2_in_2_aa₆(X, Y, U, V, Z, perm_2_in_aa₂(Z, V))
if_perm_2_in_2_aa₆(X, Y, U, V, Z, perm_2_out_aa₂(Z, V)) -> perm_2_out_aa₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0)))
if_perm_2_in_2_ag₆(X, Y, U, V, Z, perm_2_out_aa₂(Z, V)) -> perm_2_out_ag₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0)))
if_sort_2_in_1_ag₃(X, Y, perm_2_out_ag₂(X, Y)) -> if_sort_2_in_2_ag₃(X, Y, sorted_1_in_g₁(Y))
sorted_1_in_g₁([]_0) -> sorted_1_out_g₁([]_0)
sorted_1_in_g₁(._2₂(X, []_0)) -> sorted_1_out_g₁(._2₂(X, []_0))
sorted_1_in_g₁(._2₂(X, ._2₂(Y, Z))) -> if_sorted_1_in_1_g₄(X, Y, Z, le_2_in_aa₂(X, Y))
le_2_in_aa₂(s_1₁(X), s_1₁(Y)) -> if_le_2_in_1_aa₃(X, Y, le_2_in_aa₂(X, Y))
le_2_in_aa₂(0_0, s_1₁(X)) -> le_2_out_aa₂(0_0, s_1₁(X))
le_2_in_aa₂(0_0, 0_0) -> le_2_out_aa₂(0_0, 0_0)
if_le_2_in_1_aa₃(X, Y, le_2_out_aa₂(X, Y)) -> le_2_out_aa₂(s_1₁(X), s_1₁(Y))
if_sorted_1_in_1_g₄(X, Y, Z, le_2_out_aa₂(X, Y)) -> if_sorted_1_in_2_g₄(X, Y, Z, sorted_1_in_g₁(._2₂(Y, Z)))
if_sorted_1_in_2_g₄(X, Y, Z, sorted_1_out_g₁(._2₂(Y, Z))) -> sorted_1_out_g₁(._2₂(X, ._2₂(Y, Z)))
if_sort_2_in_2_ag₃(X, Y, sorted_1_out_g₁(Y)) -> sort_2_out_ag₂(X, Y)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

LE_2_IN_AA₂(s_1₁(X), s_1₁(Y)) -> LE_2_IN_AA₂(X, Y)

The TRS R consists of the following rules:

sort_2_in_ag₂(X, Y) -> if_sort_2_in_1_ag₃(X, Y, perm_2_in_ag₂(X, Y))
perm_2_in_ag₂([]_0, []_0) -> perm_2_out_ag₂([]_0, []_0)
perm_2_in_ag₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> if_perm_2_in_1_ag₅(X, Y, U, V, delete_3_in_aga₃(U, ._2₂(X, Y), Z))
delete_3_in_aga₃(X, ._2₂(X, Y), Y) -> delete_3_out_aga₃(X, ._2₂(X, Y), Y)
delete_3_in_aga₃(X, ._2₂(Y, Z), W) -> if_delete_3_in_1_aga₅(X, Y, Z, W, delete_3_in_aaa₃(X, Z, W))
delete_3_in_aaa₃(X, ._2₂(X, Y), Y) -> delete_3_out_aaa₃(X, ._2₂(X, Y), Y)
delete_3_in_aaa₃(X, ._2₂(Y, Z), W) -> if_delete_3_in_1_aaa₅(X, Y, Z, W, delete_3_in_aaa₃(X, Z, W))
if_delete_3_in_1_aaa₅(X, Y, Z, W, delete_3_out_aaa₃(X, Z, W)) -> delete_3_out_aaa₃(X, ._2₂(Y, Z), W)
if_delete_3_in_1_aga₅(X, Y, Z, W, delete_3_out_aaa₃(X, Z, W)) -> delete_3_out_aga₃(X, ._2₂(Y, Z), W)
if_perm_2_in_1_ag₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> if_perm_2_in_2_ag₆(X, Y, U, V, Z, perm_2_in_aa₂(Z, V))
perm_2_in_aa₂([]_0, []_0) -> perm_2_out_aa₂([]_0, []_0)
perm_2_in_aa₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> if_perm_2_in_1_aa₅(X, Y, U, V, delete_3_in_aga₃(U, ._2₂(X, Y), Z))
if_perm_2_in_1_aa₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> if_perm_2_in_2_aa₆(X, Y, U, V, Z, perm_2_in_aa₂(Z, V))
if_perm_2_in_2_aa₆(X, Y, U, V, Z, perm_2_out_aa₂(Z, V)) -> perm_2_out_aa₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0)))
if_perm_2_in_2_ag₆(X, Y, U, V, Z, perm_2_out_aa₂(Z, V)) -> perm_2_out_ag₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0)))
if_sort_2_in_1_ag₃(X, Y, perm_2_out_ag₂(X, Y)) -> if_sort_2_in_2_ag₃(X, Y, sorted_1_in_g₁(Y))
sorted_1_in_g₁([]_0) -> sorted_1_out_g₁([]_0)
sorted_1_in_g₁(._2₂(X, []_0)) -> sorted_1_out_g₁(._2₂(X, []_0))
sorted_1_in_g₁(._2₂(X, ._2₂(Y, Z))) -> if_sorted_1_in_1_g₄(X, Y, Z, le_2_in_aa₂(X, Y))
le_2_in_aa₂(s_1₁(X), s_1₁(Y)) -> if_le_2_in_1_aa₃(X, Y, le_2_in_aa₂(X, Y))
le_2_in_aa₂(0_0, s_1₁(X)) -> le_2_out_aa₂(0_0, s_1₁(X))
le_2_in_aa₂(0_0, 0_0) -> le_2_out_aa₂(0_0, 0_0)
if_le_2_in_1_aa₃(X, Y, le_2_out_aa₂(X, Y)) -> le_2_out_aa₂(s_1₁(X), s_1₁(Y))
if_sorted_1_in_1_g₄(X, Y, Z, le_2_out_aa₂(X, Y)) -> if_sorted_1_in_2_g₄(X, Y, Z, sorted_1_in_g₁(._2₂(Y, Z)))
if_sorted_1_in_2_g₄(X, Y, Z, sorted_1_out_g₁(._2₂(Y, Z))) -> sorted_1_out_g₁(._2₂(X, ._2₂(Y, Z)))
if_sort_2_in_2_ag₃(X, Y, sorted_1_out_g₁(Y)) -> sort_2_out_ag₂(X, Y)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

LE_2_IN_AA₂(s_1₁(X), s_1₁(Y)) -> LE_2_IN_AA₂(X, Y)

R is empty.
The argument filtering Pi contains the following mapping:
s_1₁(x1) = s_1
LE_2_IN_AA₂(x1, x2) = LE_2_IN_AA

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

LE_2_IN_AA -> LE_2_IN_AA

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {LE_2_IN_AA}.

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

IF_SORTED_1_IN_1_G₄(X, Y, Z, le_2_out_aa₂(X, Y)) -> SORTED_1_IN_G₁(._2₂(Y, Z))
SORTED_1_IN_G₁(._2₂(X, ._2₂(Y, Z))) -> IF_SORTED_1_IN_1_G₄(X, Y, Z, le_2_in_aa₂(X, Y))

The TRS R consists of the following rules:

sort_2_in_ag₂(X, Y) -> if_sort_2_in_1_ag₃(X, Y, perm_2_in_ag₂(X, Y))
perm_2_in_ag₂([]_0, []_0) -> perm_2_out_ag₂([]_0, []_0)
perm_2_in_ag₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> if_perm_2_in_1_ag₅(X, Y, U, V, delete_3_in_aga₃(U, ._2₂(X, Y), Z))
delete_3_in_aga₃(X, ._2₂(X, Y), Y) -> delete_3_out_aga₃(X, ._2₂(X, Y), Y)
delete_3_in_aga₃(X, ._2₂(Y, Z), W) -> if_delete_3_in_1_aga₅(X, Y, Z, W, delete_3_in_aaa₃(X, Z, W))
delete_3_in_aaa₃(X, ._2₂(X, Y), Y) -> delete_3_out_aaa₃(X, ._2₂(X, Y), Y)
delete_3_in_aaa₃(X, ._2₂(Y, Z), W) -> if_delete_3_in_1_aaa₅(X, Y, Z, W, delete_3_in_aaa₃(X, Z, W))
if_delete_3_in_1_aaa₅(X, Y, Z, W, delete_3_out_aaa₃(X, Z, W)) -> delete_3_out_aaa₃(X, ._2₂(Y, Z), W)
if_delete_3_in_1_aga₅(X, Y, Z, W, delete_3_out_aaa₃(X, Z, W)) -> delete_3_out_aga₃(X, ._2₂(Y, Z), W)
if_perm_2_in_1_ag₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> if_perm_2_in_2_ag₆(X, Y, U, V, Z, perm_2_in_aa₂(Z, V))
perm_2_in_aa₂([]_0, []_0) -> perm_2_out_aa₂([]_0, []_0)
perm_2_in_aa₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> if_perm_2_in_1_aa₅(X, Y, U, V, delete_3_in_aga₃(U, ._2₂(X, Y), Z))
if_perm_2_in_1_aa₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> if_perm_2_in_2_aa₆(X, Y, U, V, Z, perm_2_in_aa₂(Z, V))
if_perm_2_in_2_aa₆(X, Y, U, V, Z, perm_2_out_aa₂(Z, V)) -> perm_2_out_aa₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0)))
if_perm_2_in_2_ag₆(X, Y, U, V, Z, perm_2_out_aa₂(Z, V)) -> perm_2_out_ag₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0)))
if_sort_2_in_1_ag₃(X, Y, perm_2_out_ag₂(X, Y)) -> if_sort_2_in_2_ag₃(X, Y, sorted_1_in_g₁(Y))
sorted_1_in_g₁([]_0) -> sorted_1_out_g₁([]_0)
sorted_1_in_g₁(._2₂(X, []_0)) -> sorted_1_out_g₁(._2₂(X, []_0))
sorted_1_in_g₁(._2₂(X, ._2₂(Y, Z))) -> if_sorted_1_in_1_g₄(X, Y, Z, le_2_in_aa₂(X, Y))
le_2_in_aa₂(s_1₁(X), s_1₁(Y)) -> if_le_2_in_1_aa₃(X, Y, le_2_in_aa₂(X, Y))
le_2_in_aa₂(0_0, s_1₁(X)) -> le_2_out_aa₂(0_0, s_1₁(X))
le_2_in_aa₂(0_0, 0_0) -> le_2_out_aa₂(0_0, 0_0)
if_le_2_in_1_aa₃(X, Y, le_2_out_aa₂(X, Y)) -> le_2_out_aa₂(s_1₁(X), s_1₁(Y))
if_sorted_1_in_1_g₄(X, Y, Z, le_2_out_aa₂(X, Y)) -> if_sorted_1_in_2_g₄(X, Y, Z, sorted_1_in_g₁(._2₂(Y, Z)))
if_sorted_1_in_2_g₄(X, Y, Z, sorted_1_out_g₁(._2₂(Y, Z))) -> sorted_1_out_g₁(._2₂(X, ._2₂(Y, Z)))
if_sort_2_in_2_ag₃(X, Y, sorted_1_out_g₁(Y)) -> sort_2_out_ag₂(X, Y)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

IF_SORTED_1_IN_1_G₄(X, Y, Z, le_2_out_aa₂(X, Y)) -> SORTED_1_IN_G₁(._2₂(Y, Z))
SORTED_1_IN_G₁(._2₂(X, ._2₂(Y, Z))) -> IF_SORTED_1_IN_1_G₄(X, Y, Z, le_2_in_aa₂(X, Y))

The TRS R consists of the following rules:

le_2_in_aa₂(s_1₁(X), s_1₁(Y)) -> if_le_2_in_1_aa₃(X, Y, le_2_in_aa₂(X, Y))
le_2_in_aa₂(0_0, s_1₁(X)) -> le_2_out_aa₂(0_0, s_1₁(X))
le_2_in_aa₂(0_0, 0_0) -> le_2_out_aa₂(0_0, 0_0)
if_le_2_in_1_aa₃(X, Y, le_2_out_aa₂(X, Y)) -> le_2_out_aa₂(s_1₁(X), s_1₁(Y))

The argument filtering Pi contains the following mapping:
._2₂(x1, x2) = ._2
s_1₁(x1) = s_1
0_0 = 0_0
le_2_in_aa₂(x1, x2) = le_2_in_aa
if_le_2_in_1_aa₃(x1, x2, x3) = if_le_2_in_1_aa₁(x3)
le_2_out_aa₂(x1, x2) = le_2_out_aa₂(x1, x2)
SORTED_1_IN_G₁(x1) = SORTED_1_IN_G₁(x1)
IF_SORTED_1_IN_1_G₄(x1, x2, x3, x4) = IF_SORTED_1_IN_1_G₁(x4)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

IF_SORTED_1_IN_1_G₁(le_2_out_aa₂(X, Y)) -> SORTED_1_IN_G₁(._2)
SORTED_1_IN_G₁(._2) -> IF_SORTED_1_IN_1_G₁(le_2_in_aa)

The TRS R consists of the following rules:

le_2_in_aa -> if_le_2_in_1_aa₁(le_2_in_aa)
le_2_in_aa -> le_2_out_aa₂(0_0, s_1)
le_2_in_aa -> le_2_out_aa₂(0_0, 0_0)
if_le_2_in_1_aa₁(le_2_out_aa₂(X, Y)) -> le_2_out_aa₂(s_1, s_1)

The set Q consists of the following terms:

le_2_in_aa
if_le_2_in_1_aa₁(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {SORTED_1_IN_G₁, IF_SORTED_1_IN_1_G₁}.

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

DELETE_3_IN_AAA₃(X, ._2₂(Y, Z), W) -> DELETE_3_IN_AAA₃(X, Z, W)

The TRS R consists of the following rules:

sort_2_in_ag₂(X, Y) -> if_sort_2_in_1_ag₃(X, Y, perm_2_in_ag₂(X, Y))
perm_2_in_ag₂([]_0, []_0) -> perm_2_out_ag₂([]_0, []_0)
perm_2_in_ag₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> if_perm_2_in_1_ag₅(X, Y, U, V, delete_3_in_aga₃(U, ._2₂(X, Y), Z))
delete_3_in_aga₃(X, ._2₂(X, Y), Y) -> delete_3_out_aga₃(X, ._2₂(X, Y), Y)
delete_3_in_aga₃(X, ._2₂(Y, Z), W) -> if_delete_3_in_1_aga₅(X, Y, Z, W, delete_3_in_aaa₃(X, Z, W))
delete_3_in_aaa₃(X, ._2₂(X, Y), Y) -> delete_3_out_aaa₃(X, ._2₂(X, Y), Y)
delete_3_in_aaa₃(X, ._2₂(Y, Z), W) -> if_delete_3_in_1_aaa₅(X, Y, Z, W, delete_3_in_aaa₃(X, Z, W))
if_delete_3_in_1_aaa₅(X, Y, Z, W, delete_3_out_aaa₃(X, Z, W)) -> delete_3_out_aaa₃(X, ._2₂(Y, Z), W)
if_delete_3_in_1_aga₅(X, Y, Z, W, delete_3_out_aaa₃(X, Z, W)) -> delete_3_out_aga₃(X, ._2₂(Y, Z), W)
if_perm_2_in_1_ag₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> if_perm_2_in_2_ag₆(X, Y, U, V, Z, perm_2_in_aa₂(Z, V))
perm_2_in_aa₂([]_0, []_0) -> perm_2_out_aa₂([]_0, []_0)
perm_2_in_aa₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> if_perm_2_in_1_aa₅(X, Y, U, V, delete_3_in_aga₃(U, ._2₂(X, Y), Z))
if_perm_2_in_1_aa₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> if_perm_2_in_2_aa₆(X, Y, U, V, Z, perm_2_in_aa₂(Z, V))
if_perm_2_in_2_aa₆(X, Y, U, V, Z, perm_2_out_aa₂(Z, V)) -> perm_2_out_aa₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0)))
if_perm_2_in_2_ag₆(X, Y, U, V, Z, perm_2_out_aa₂(Z, V)) -> perm_2_out_ag₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0)))
if_sort_2_in_1_ag₃(X, Y, perm_2_out_ag₂(X, Y)) -> if_sort_2_in_2_ag₃(X, Y, sorted_1_in_g₁(Y))
sorted_1_in_g₁([]_0) -> sorted_1_out_g₁([]_0)
sorted_1_in_g₁(._2₂(X, []_0)) -> sorted_1_out_g₁(._2₂(X, []_0))
sorted_1_in_g₁(._2₂(X, ._2₂(Y, Z))) -> if_sorted_1_in_1_g₄(X, Y, Z, le_2_in_aa₂(X, Y))
le_2_in_aa₂(s_1₁(X), s_1₁(Y)) -> if_le_2_in_1_aa₃(X, Y, le_2_in_aa₂(X, Y))
le_2_in_aa₂(0_0, s_1₁(X)) -> le_2_out_aa₂(0_0, s_1₁(X))
le_2_in_aa₂(0_0, 0_0) -> le_2_out_aa₂(0_0, 0_0)
if_le_2_in_1_aa₃(X, Y, le_2_out_aa₂(X, Y)) -> le_2_out_aa₂(s_1₁(X), s_1₁(Y))
if_sorted_1_in_1_g₄(X, Y, Z, le_2_out_aa₂(X, Y)) -> if_sorted_1_in_2_g₄(X, Y, Z, sorted_1_in_g₁(._2₂(Y, Z)))
if_sorted_1_in_2_g₄(X, Y, Z, sorted_1_out_g₁(._2₂(Y, Z))) -> sorted_1_out_g₁(._2₂(X, ._2₂(Y, Z)))
if_sort_2_in_2_ag₃(X, Y, sorted_1_out_g₁(Y)) -> sort_2_out_ag₂(X, Y)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

DELETE_3_IN_AAA₃(X, ._2₂(Y, Z), W) -> DELETE_3_IN_AAA₃(X, Z, W)

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

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

DELETE_3_IN_AAA -> DELETE_3_IN_AAA

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {DELETE_3_IN_AAA}.

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

  ↳ PrologToPiTRSProof

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

IF_PERM_2_IN_1_AA₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> PERM_2_IN_AA₂(Z, V)
PERM_2_IN_AA₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> IF_PERM_2_IN_1_AA₅(X, Y, U, V, delete_3_in_aga₃(U, ._2₂(X, Y), Z))

The TRS R consists of the following rules:

sort_2_in_ag₂(X, Y) -> if_sort_2_in_1_ag₃(X, Y, perm_2_in_ag₂(X, Y))
perm_2_in_ag₂([]_0, []_0) -> perm_2_out_ag₂([]_0, []_0)
perm_2_in_ag₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> if_perm_2_in_1_ag₅(X, Y, U, V, delete_3_in_aga₃(U, ._2₂(X, Y), Z))
delete_3_in_aga₃(X, ._2₂(X, Y), Y) -> delete_3_out_aga₃(X, ._2₂(X, Y), Y)
delete_3_in_aga₃(X, ._2₂(Y, Z), W) -> if_delete_3_in_1_aga₅(X, Y, Z, W, delete_3_in_aaa₃(X, Z, W))
delete_3_in_aaa₃(X, ._2₂(X, Y), Y) -> delete_3_out_aaa₃(X, ._2₂(X, Y), Y)
delete_3_in_aaa₃(X, ._2₂(Y, Z), W) -> if_delete_3_in_1_aaa₅(X, Y, Z, W, delete_3_in_aaa₃(X, Z, W))
if_delete_3_in_1_aaa₅(X, Y, Z, W, delete_3_out_aaa₃(X, Z, W)) -> delete_3_out_aaa₃(X, ._2₂(Y, Z), W)
if_delete_3_in_1_aga₅(X, Y, Z, W, delete_3_out_aaa₃(X, Z, W)) -> delete_3_out_aga₃(X, ._2₂(Y, Z), W)
if_perm_2_in_1_ag₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> if_perm_2_in_2_ag₆(X, Y, U, V, Z, perm_2_in_aa₂(Z, V))
perm_2_in_aa₂([]_0, []_0) -> perm_2_out_aa₂([]_0, []_0)
perm_2_in_aa₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> if_perm_2_in_1_aa₅(X, Y, U, V, delete_3_in_aga₃(U, ._2₂(X, Y), Z))
if_perm_2_in_1_aa₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> if_perm_2_in_2_aa₆(X, Y, U, V, Z, perm_2_in_aa₂(Z, V))
if_perm_2_in_2_aa₆(X, Y, U, V, Z, perm_2_out_aa₂(Z, V)) -> perm_2_out_aa₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0)))
if_perm_2_in_2_ag₆(X, Y, U, V, Z, perm_2_out_aa₂(Z, V)) -> perm_2_out_ag₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0)))
if_sort_2_in_1_ag₃(X, Y, perm_2_out_ag₂(X, Y)) -> if_sort_2_in_2_ag₃(X, Y, sorted_1_in_g₁(Y))
sorted_1_in_g₁([]_0) -> sorted_1_out_g₁([]_0)
sorted_1_in_g₁(._2₂(X, []_0)) -> sorted_1_out_g₁(._2₂(X, []_0))
sorted_1_in_g₁(._2₂(X, ._2₂(Y, Z))) -> if_sorted_1_in_1_g₄(X, Y, Z, le_2_in_aa₂(X, Y))
le_2_in_aa₂(s_1₁(X), s_1₁(Y)) -> if_le_2_in_1_aa₃(X, Y, le_2_in_aa₂(X, Y))
le_2_in_aa₂(0_0, s_1₁(X)) -> le_2_out_aa₂(0_0, s_1₁(X))
le_2_in_aa₂(0_0, 0_0) -> le_2_out_aa₂(0_0, 0_0)
if_le_2_in_1_aa₃(X, Y, le_2_out_aa₂(X, Y)) -> le_2_out_aa₂(s_1₁(X), s_1₁(Y))
if_sorted_1_in_1_g₄(X, Y, Z, le_2_out_aa₂(X, Y)) -> if_sorted_1_in_2_g₄(X, Y, Z, sorted_1_in_g₁(._2₂(Y, Z)))
if_sorted_1_in_2_g₄(X, Y, Z, sorted_1_out_g₁(._2₂(Y, Z))) -> sorted_1_out_g₁(._2₂(X, ._2₂(Y, Z)))
if_sort_2_in_2_ag₃(X, Y, sorted_1_out_g₁(Y)) -> sort_2_out_ag₂(X, Y)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

  ↳ PrologToPiTRSProof

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

IF_PERM_2_IN_1_AA₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> PERM_2_IN_AA₂(Z, V)
PERM_2_IN_AA₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> IF_PERM_2_IN_1_AA₅(X, Y, U, V, delete_3_in_aga₃(U, ._2₂(X, Y), Z))

The TRS R consists of the following rules:

delete_3_in_aga₃(X, ._2₂(X, Y), Y) -> delete_3_out_aga₃(X, ._2₂(X, Y), Y)
delete_3_in_aga₃(X, ._2₂(Y, Z), W) -> if_delete_3_in_1_aga₅(X, Y, Z, W, delete_3_in_aaa₃(X, Z, W))
if_delete_3_in_1_aga₅(X, Y, Z, W, delete_3_out_aaa₃(X, Z, W)) -> delete_3_out_aga₃(X, ._2₂(Y, Z), W)
delete_3_in_aaa₃(X, ._2₂(X, Y), Y) -> delete_3_out_aaa₃(X, ._2₂(X, Y), Y)
delete_3_in_aaa₃(X, ._2₂(Y, Z), W) -> if_delete_3_in_1_aaa₅(X, Y, Z, W, delete_3_in_aaa₃(X, Z, W))
if_delete_3_in_1_aaa₅(X, Y, Z, W, delete_3_out_aaa₃(X, Z, W)) -> delete_3_out_aaa₃(X, ._2₂(Y, Z), W)

The argument filtering Pi contains the following mapping:
[]_0 = []_0
._2₂(x1, x2) = ._2
delete_3_in_aga₃(x1, x2, x3) = delete_3_in_aga₁(x2)
delete_3_out_aga₃(x1, x2, x3) = delete_3_out_aga
if_delete_3_in_1_aga₅(x1, x2, x3, x4, x5) = if_delete_3_in_1_aga₁(x5)
delete_3_in_aaa₃(x1, x2, x3) = delete_3_in_aaa
delete_3_out_aaa₃(x1, x2, x3) = delete_3_out_aaa₁(x2)
if_delete_3_in_1_aaa₅(x1, x2, x3, x4, x5) = if_delete_3_in_1_aaa₁(x5)
PERM_2_IN_AA₂(x1, x2) = PERM_2_IN_AA
IF_PERM_2_IN_1_AA₅(x1, x2, x3, x4, x5) = IF_PERM_2_IN_1_AA₁(x5)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

  ↳ PrologToPiTRSProof

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

IF_PERM_2_IN_1_AA₁(delete_3_out_aga) -> PERM_2_IN_AA
PERM_2_IN_AA -> IF_PERM_2_IN_1_AA₁(delete_3_in_aga₁(._2))

The TRS R consists of the following rules:

delete_3_in_aga₁(._2) -> delete_3_out_aga
delete_3_in_aga₁(._2) -> if_delete_3_in_1_aga₁(delete_3_in_aaa)
if_delete_3_in_1_aga₁(delete_3_out_aaa₁(Z)) -> delete_3_out_aga
delete_3_in_aaa -> delete_3_out_aaa₁(._2)
delete_3_in_aaa -> if_delete_3_in_1_aaa₁(delete_3_in_aaa)
if_delete_3_in_1_aaa₁(delete_3_out_aaa₁(Z)) -> delete_3_out_aaa₁(._2)

The set Q consists of the following terms:

delete_3_in_aga₁(x0)
if_delete_3_in_1_aga₁(x0)
delete_3_in_aaa
if_delete_3_in_1_aaa₁(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {PERM_2_IN_AA, IF_PERM_2_IN_1_AA₁}.
With regard to the inferred argument filtering the predicates were used in the following modes:
sort₂: (f,b)
perm₂: (f,b) (f,f)
delete₃: (f,b,f) (f,f,f)
sorted₁: (b)
le₂: (f,f)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

sort_2_in_ag₂(X, Y) -> if_sort_2_in_1_ag₃(X, Y, perm_2_in_ag₂(X, Y))
perm_2_in_ag₂([]_0, []_0) -> perm_2_out_ag₂([]_0, []_0)
perm_2_in_ag₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> if_perm_2_in_1_ag₅(X, Y, U, V, delete_3_in_aga₃(U, ._2₂(X, Y), Z))
delete_3_in_aga₃(X, ._2₂(X, Y), Y) -> delete_3_out_aga₃(X, ._2₂(X, Y), Y)
delete_3_in_aga₃(X, ._2₂(Y, Z), W) -> if_delete_3_in_1_aga₅(X, Y, Z, W, delete_3_in_aaa₃(X, Z, W))
delete_3_in_aaa₃(X, ._2₂(X, Y), Y) -> delete_3_out_aaa₃(X, ._2₂(X, Y), Y)
delete_3_in_aaa₃(X, ._2₂(Y, Z), W) -> if_delete_3_in_1_aaa₅(X, Y, Z, W, delete_3_in_aaa₃(X, Z, W))
if_delete_3_in_1_aaa₅(X, Y, Z, W, delete_3_out_aaa₃(X, Z, W)) -> delete_3_out_aaa₃(X, ._2₂(Y, Z), W)
if_delete_3_in_1_aga₅(X, Y, Z, W, delete_3_out_aaa₃(X, Z, W)) -> delete_3_out_aga₃(X, ._2₂(Y, Z), W)
if_perm_2_in_1_ag₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> if_perm_2_in_2_ag₆(X, Y, U, V, Z, perm_2_in_aa₂(Z, V))
perm_2_in_aa₂([]_0, []_0) -> perm_2_out_aa₂([]_0, []_0)
perm_2_in_aa₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> if_perm_2_in_1_aa₅(X, Y, U, V, delete_3_in_aga₃(U, ._2₂(X, Y), Z))
if_perm_2_in_1_aa₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> if_perm_2_in_2_aa₆(X, Y, U, V, Z, perm_2_in_aa₂(Z, V))
if_perm_2_in_2_aa₆(X, Y, U, V, Z, perm_2_out_aa₂(Z, V)) -> perm_2_out_aa₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0)))
if_perm_2_in_2_ag₆(X, Y, U, V, Z, perm_2_out_aa₂(Z, V)) -> perm_2_out_ag₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0)))
if_sort_2_in_1_ag₃(X, Y, perm_2_out_ag₂(X, Y)) -> if_sort_2_in_2_ag₃(X, Y, sorted_1_in_g₁(Y))
sorted_1_in_g₁([]_0) -> sorted_1_out_g₁([]_0)
sorted_1_in_g₁(._2₂(X, []_0)) -> sorted_1_out_g₁(._2₂(X, []_0))
sorted_1_in_g₁(._2₂(X, ._2₂(Y, Z))) -> if_sorted_1_in_1_g₄(X, Y, Z, le_2_in_aa₂(X, Y))
le_2_in_aa₂(s_1₁(X), s_1₁(Y)) -> if_le_2_in_1_aa₃(X, Y, le_2_in_aa₂(X, Y))
le_2_in_aa₂(0_0, s_1₁(X)) -> le_2_out_aa₂(0_0, s_1₁(X))
le_2_in_aa₂(0_0, 0_0) -> le_2_out_aa₂(0_0, 0_0)
if_le_2_in_1_aa₃(X, Y, le_2_out_aa₂(X, Y)) -> le_2_out_aa₂(s_1₁(X), s_1₁(Y))
if_sorted_1_in_1_g₄(X, Y, Z, le_2_out_aa₂(X, Y)) -> if_sorted_1_in_2_g₄(X, Y, Z, sorted_1_in_g₁(._2₂(Y, Z)))
if_sorted_1_in_2_g₄(X, Y, Z, sorted_1_out_g₁(._2₂(Y, Z))) -> sorted_1_out_g₁(._2₂(X, ._2₂(Y, Z)))
if_sort_2_in_2_ag₃(X, Y, sorted_1_out_g₁(Y)) -> sort_2_out_ag₂(X, Y)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

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

sort_2_in_ag₂(X, Y) -> if_sort_2_in_1_ag₃(X, Y, perm_2_in_ag₂(X, Y))
perm_2_in_ag₂([]_0, []_0) -> perm_2_out_ag₂([]_0, []_0)
perm_2_in_ag₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> if_perm_2_in_1_ag₅(X, Y, U, V, delete_3_in_aga₃(U, ._2₂(X, Y), Z))
delete_3_in_aga₃(X, ._2₂(X, Y), Y) -> delete_3_out_aga₃(X, ._2₂(X, Y), Y)
delete_3_in_aga₃(X, ._2₂(Y, Z), W) -> if_delete_3_in_1_aga₅(X, Y, Z, W, delete_3_in_aaa₃(X, Z, W))
delete_3_in_aaa₃(X, ._2₂(X, Y), Y) -> delete_3_out_aaa₃(X, ._2₂(X, Y), Y)
delete_3_in_aaa₃(X, ._2₂(Y, Z), W) -> if_delete_3_in_1_aaa₅(X, Y, Z, W, delete_3_in_aaa₃(X, Z, W))
if_delete_3_in_1_aaa₅(X, Y, Z, W, delete_3_out_aaa₃(X, Z, W)) -> delete_3_out_aaa₃(X, ._2₂(Y, Z), W)
if_delete_3_in_1_aga₅(X, Y, Z, W, delete_3_out_aaa₃(X, Z, W)) -> delete_3_out_aga₃(X, ._2₂(Y, Z), W)
if_perm_2_in_1_ag₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> if_perm_2_in_2_ag₆(X, Y, U, V, Z, perm_2_in_aa₂(Z, V))
perm_2_in_aa₂([]_0, []_0) -> perm_2_out_aa₂([]_0, []_0)
perm_2_in_aa₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> if_perm_2_in_1_aa₅(X, Y, U, V, delete_3_in_aga₃(U, ._2₂(X, Y), Z))
if_perm_2_in_1_aa₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> if_perm_2_in_2_aa₆(X, Y, U, V, Z, perm_2_in_aa₂(Z, V))
if_perm_2_in_2_aa₆(X, Y, U, V, Z, perm_2_out_aa₂(Z, V)) -> perm_2_out_aa₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0)))
if_perm_2_in_2_ag₆(X, Y, U, V, Z, perm_2_out_aa₂(Z, V)) -> perm_2_out_ag₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0)))
if_sort_2_in_1_ag₃(X, Y, perm_2_out_ag₂(X, Y)) -> if_sort_2_in_2_ag₃(X, Y, sorted_1_in_g₁(Y))
sorted_1_in_g₁([]_0) -> sorted_1_out_g₁([]_0)
sorted_1_in_g₁(._2₂(X, []_0)) -> sorted_1_out_g₁(._2₂(X, []_0))
sorted_1_in_g₁(._2₂(X, ._2₂(Y, Z))) -> if_sorted_1_in_1_g₄(X, Y, Z, le_2_in_aa₂(X, Y))
le_2_in_aa₂(s_1₁(X), s_1₁(Y)) -> if_le_2_in_1_aa₃(X, Y, le_2_in_aa₂(X, Y))
le_2_in_aa₂(0_0, s_1₁(X)) -> le_2_out_aa₂(0_0, s_1₁(X))
le_2_in_aa₂(0_0, 0_0) -> le_2_out_aa₂(0_0, 0_0)
if_le_2_in_1_aa₃(X, Y, le_2_out_aa₂(X, Y)) -> le_2_out_aa₂(s_1₁(X), s_1₁(Y))
if_sorted_1_in_1_g₄(X, Y, Z, le_2_out_aa₂(X, Y)) -> if_sorted_1_in_2_g₄(X, Y, Z, sorted_1_in_g₁(._2₂(Y, Z)))
if_sorted_1_in_2_g₄(X, Y, Z, sorted_1_out_g₁(._2₂(Y, Z))) -> sorted_1_out_g₁(._2₂(X, ._2₂(Y, Z)))
if_sort_2_in_2_ag₃(X, Y, sorted_1_out_g₁(Y)) -> sort_2_out_ag₂(X, Y)

SORT_2_IN_AG₂(X, Y) -> IF_SORT_2_IN_1_AG₃(X, Y, perm_2_in_ag₂(X, Y))
SORT_2_IN_AG₂(X, Y) -> PERM_2_IN_AG₂(X, Y)
PERM_2_IN_AG₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> IF_PERM_2_IN_1_AG₅(X, Y, U, V, delete_3_in_aga₃(U, ._2₂(X, Y), Z))
PERM_2_IN_AG₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> DELETE_3_IN_AGA₃(U, ._2₂(X, Y), Z)
DELETE_3_IN_AGA₃(X, ._2₂(Y, Z), W) -> IF_DELETE_3_IN_1_AGA₅(X, Y, Z, W, delete_3_in_aaa₃(X, Z, W))
DELETE_3_IN_AGA₃(X, ._2₂(Y, Z), W) -> DELETE_3_IN_AAA₃(X, Z, W)
DELETE_3_IN_AAA₃(X, ._2₂(Y, Z), W) -> IF_DELETE_3_IN_1_AAA₅(X, Y, Z, W, delete_3_in_aaa₃(X, Z, W))
DELETE_3_IN_AAA₃(X, ._2₂(Y, Z), W) -> DELETE_3_IN_AAA₃(X, Z, W)
IF_PERM_2_IN_1_AG₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> IF_PERM_2_IN_2_AG₆(X, Y, U, V, Z, perm_2_in_aa₂(Z, V))
IF_PERM_2_IN_1_AG₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> PERM_2_IN_AA₂(Z, V)
PERM_2_IN_AA₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> IF_PERM_2_IN_1_AA₅(X, Y, U, V, delete_3_in_aga₃(U, ._2₂(X, Y), Z))
PERM_2_IN_AA₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> DELETE_3_IN_AGA₃(U, ._2₂(X, Y), Z)
IF_PERM_2_IN_1_AA₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> IF_PERM_2_IN_2_AA₆(X, Y, U, V, Z, perm_2_in_aa₂(Z, V))
IF_PERM_2_IN_1_AA₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> PERM_2_IN_AA₂(Z, V)
IF_SORT_2_IN_1_AG₃(X, Y, perm_2_out_ag₂(X, Y)) -> IF_SORT_2_IN_2_AG₃(X, Y, sorted_1_in_g₁(Y))
IF_SORT_2_IN_1_AG₃(X, Y, perm_2_out_ag₂(X, Y)) -> SORTED_1_IN_G₁(Y)
SORTED_1_IN_G₁(._2₂(X, ._2₂(Y, Z))) -> IF_SORTED_1_IN_1_G₄(X, Y, Z, le_2_in_aa₂(X, Y))
SORTED_1_IN_G₁(._2₂(X, ._2₂(Y, Z))) -> LE_2_IN_AA₂(X, Y)
LE_2_IN_AA₂(s_1₁(X), s_1₁(Y)) -> IF_LE_2_IN_1_AA₃(X, Y, le_2_in_aa₂(X, Y))
LE_2_IN_AA₂(s_1₁(X), s_1₁(Y)) -> LE_2_IN_AA₂(X, Y)
IF_SORTED_1_IN_1_G₄(X, Y, Z, le_2_out_aa₂(X, Y)) -> IF_SORTED_1_IN_2_G₄(X, Y, Z, sorted_1_in_g₁(._2₂(Y, Z)))
IF_SORTED_1_IN_1_G₄(X, Y, Z, le_2_out_aa₂(X, Y)) -> SORTED_1_IN_G₁(._2₂(Y, Z))

The TRS R consists of the following rules:

sort_2_in_ag₂(X, Y) -> if_sort_2_in_1_ag₃(X, Y, perm_2_in_ag₂(X, Y))
perm_2_in_ag₂([]_0, []_0) -> perm_2_out_ag₂([]_0, []_0)
perm_2_in_ag₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> if_perm_2_in_1_ag₅(X, Y, U, V, delete_3_in_aga₃(U, ._2₂(X, Y), Z))
delete_3_in_aga₃(X, ._2₂(X, Y), Y) -> delete_3_out_aga₃(X, ._2₂(X, Y), Y)
delete_3_in_aga₃(X, ._2₂(Y, Z), W) -> if_delete_3_in_1_aga₅(X, Y, Z, W, delete_3_in_aaa₃(X, Z, W))
delete_3_in_aaa₃(X, ._2₂(X, Y), Y) -> delete_3_out_aaa₃(X, ._2₂(X, Y), Y)
delete_3_in_aaa₃(X, ._2₂(Y, Z), W) -> if_delete_3_in_1_aaa₅(X, Y, Z, W, delete_3_in_aaa₃(X, Z, W))
if_delete_3_in_1_aaa₅(X, Y, Z, W, delete_3_out_aaa₃(X, Z, W)) -> delete_3_out_aaa₃(X, ._2₂(Y, Z), W)
if_delete_3_in_1_aga₅(X, Y, Z, W, delete_3_out_aaa₃(X, Z, W)) -> delete_3_out_aga₃(X, ._2₂(Y, Z), W)
if_perm_2_in_1_ag₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> if_perm_2_in_2_ag₆(X, Y, U, V, Z, perm_2_in_aa₂(Z, V))
perm_2_in_aa₂([]_0, []_0) -> perm_2_out_aa₂([]_0, []_0)
perm_2_in_aa₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> if_perm_2_in_1_aa₅(X, Y, U, V, delete_3_in_aga₃(U, ._2₂(X, Y), Z))
if_perm_2_in_1_aa₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> if_perm_2_in_2_aa₆(X, Y, U, V, Z, perm_2_in_aa₂(Z, V))
if_perm_2_in_2_aa₆(X, Y, U, V, Z, perm_2_out_aa₂(Z, V)) -> perm_2_out_aa₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0)))
if_perm_2_in_2_ag₆(X, Y, U, V, Z, perm_2_out_aa₂(Z, V)) -> perm_2_out_ag₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0)))
if_sort_2_in_1_ag₃(X, Y, perm_2_out_ag₂(X, Y)) -> if_sort_2_in_2_ag₃(X, Y, sorted_1_in_g₁(Y))
sorted_1_in_g₁([]_0) -> sorted_1_out_g₁([]_0)
sorted_1_in_g₁(._2₂(X, []_0)) -> sorted_1_out_g₁(._2₂(X, []_0))
sorted_1_in_g₁(._2₂(X, ._2₂(Y, Z))) -> if_sorted_1_in_1_g₄(X, Y, Z, le_2_in_aa₂(X, Y))
le_2_in_aa₂(s_1₁(X), s_1₁(Y)) -> if_le_2_in_1_aa₃(X, Y, le_2_in_aa₂(X, Y))
le_2_in_aa₂(0_0, s_1₁(X)) -> le_2_out_aa₂(0_0, s_1₁(X))
le_2_in_aa₂(0_0, 0_0) -> le_2_out_aa₂(0_0, 0_0)
if_le_2_in_1_aa₃(X, Y, le_2_out_aa₂(X, Y)) -> le_2_out_aa₂(s_1₁(X), s_1₁(Y))
if_sorted_1_in_1_g₄(X, Y, Z, le_2_out_aa₂(X, Y)) -> if_sorted_1_in_2_g₄(X, Y, Z, sorted_1_in_g₁(._2₂(Y, Z)))
if_sorted_1_in_2_g₄(X, Y, Z, sorted_1_out_g₁(._2₂(Y, Z))) -> sorted_1_out_g₁(._2₂(X, ._2₂(Y, Z)))
if_sort_2_in_2_ag₃(X, Y, sorted_1_out_g₁(Y)) -> sort_2_out_ag₂(X, Y)

The argument filtering Pi contains the following mapping:
sort_2_in_ag₂(x1, x2) = sort_2_in_ag₁(x2)
[]_0 = []_0
._2₂(x1, x2) = ._2
s_1₁(x1) = s_1
0_0 = 0_0
if_sort_2_in_1_ag₃(x1, x2, x3) = if_sort_2_in_1_ag₂(x2, x3)
perm_2_in_ag₂(x1, x2) = perm_2_in_ag₁(x2)
perm_2_out_ag₂(x1, x2) = perm_2_out_ag₂(x1, x2)
if_perm_2_in_1_ag₅(x1, x2, x3, x4, x5) = if_perm_2_in_1_ag₁(x5)
delete_3_in_aga₃(x1, x2, x3) = delete_3_in_aga₁(x2)
delete_3_out_aga₃(x1, x2, x3) = delete_3_out_aga₁(x2)
if_delete_3_in_1_aga₅(x1, x2, x3, x4, x5) = if_delete_3_in_1_aga₁(x5)
delete_3_in_aaa₃(x1, x2, x3) = delete_3_in_aaa
delete_3_out_aaa₃(x1, x2, x3) = delete_3_out_aaa₁(x2)
if_delete_3_in_1_aaa₅(x1, x2, x3, x4, x5) = if_delete_3_in_1_aaa₁(x5)
if_perm_2_in_2_ag₆(x1, x2, x3, x4, x5, x6) = if_perm_2_in_2_ag₁(x6)
perm_2_in_aa₂(x1, x2) = perm_2_in_aa
perm_2_out_aa₂(x1, x2) = perm_2_out_aa₂(x1, x2)
if_perm_2_in_1_aa₅(x1, x2, x3, x4, x5) = if_perm_2_in_1_aa₁(x5)
if_perm_2_in_2_aa₆(x1, x2, x3, x4, x5, x6) = if_perm_2_in_2_aa₁(x6)
if_sort_2_in_2_ag₃(x1, x2, x3) = if_sort_2_in_2_ag₃(x1, x2, x3)
sorted_1_in_g₁(x1) = sorted_1_in_g₁(x1)
sorted_1_out_g₁(x1) = sorted_1_out_g₁(x1)
if_sorted_1_in_1_g₄(x1, x2, x3, x4) = if_sorted_1_in_1_g₁(x4)
le_2_in_aa₂(x1, x2) = le_2_in_aa
if_le_2_in_1_aa₃(x1, x2, x3) = if_le_2_in_1_aa₁(x3)
le_2_out_aa₂(x1, x2) = le_2_out_aa₂(x1, x2)
if_sorted_1_in_2_g₄(x1, x2, x3, x4) = if_sorted_1_in_2_g₁(x4)
sort_2_out_ag₂(x1, x2) = sort_2_out_ag₂(x1, x2)
IF_DELETE_3_IN_1_AAA₅(x1, x2, x3, x4, x5) = IF_DELETE_3_IN_1_AAA₁(x5)
IF_SORTED_1_IN_2_G₄(x1, x2, x3, x4) = IF_SORTED_1_IN_2_G₁(x4)
IF_SORT_2_IN_2_AG₃(x1, x2, x3) = IF_SORT_2_IN_2_AG₃(x1, x2, x3)
IF_SORT_2_IN_1_AG₃(x1, x2, x3) = IF_SORT_2_IN_1_AG₂(x2, x3)
PERM_2_IN_AG₂(x1, x2) = PERM_2_IN_AG₁(x2)
IF_DELETE_3_IN_1_AGA₅(x1, x2, x3, x4, x5) = IF_DELETE_3_IN_1_AGA₁(x5)
IF_PERM_2_IN_2_AA₆(x1, x2, x3, x4, x5, x6) = IF_PERM_2_IN_2_AA₁(x6)
PERM_2_IN_AA₂(x1, x2) = PERM_2_IN_AA
SORTED_1_IN_G₁(x1) = SORTED_1_IN_G₁(x1)
SORT_2_IN_AG₂(x1, x2) = SORT_2_IN_AG₁(x2)
LE_2_IN_AA₂(x1, x2) = LE_2_IN_AA
IF_LE_2_IN_1_AA₃(x1, x2, x3) = IF_LE_2_IN_1_AA₁(x3)
DELETE_3_IN_AGA₃(x1, x2, x3) = DELETE_3_IN_AGA₁(x2)
IF_PERM_2_IN_1_AG₅(x1, x2, x3, x4, x5) = IF_PERM_2_IN_1_AG₁(x5)
IF_PERM_2_IN_2_AG₆(x1, x2, x3, x4, x5, x6) = IF_PERM_2_IN_2_AG₁(x6)
IF_SORTED_1_IN_1_G₄(x1, x2, x3, x4) = IF_SORTED_1_IN_1_G₁(x4)
DELETE_3_IN_AAA₃(x1, x2, x3) = DELETE_3_IN_AAA
IF_PERM_2_IN_1_AA₅(x1, x2, x3, x4, x5) = IF_PERM_2_IN_1_AA₁(x5)

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

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

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

SORT_2_IN_AG₂(X, Y) -> IF_SORT_2_IN_1_AG₃(X, Y, perm_2_in_ag₂(X, Y))
SORT_2_IN_AG₂(X, Y) -> PERM_2_IN_AG₂(X, Y)
PERM_2_IN_AG₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> IF_PERM_2_IN_1_AG₅(X, Y, U, V, delete_3_in_aga₃(U, ._2₂(X, Y), Z))
PERM_2_IN_AG₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> DELETE_3_IN_AGA₃(U, ._2₂(X, Y), Z)
DELETE_3_IN_AGA₃(X, ._2₂(Y, Z), W) -> IF_DELETE_3_IN_1_AGA₅(X, Y, Z, W, delete_3_in_aaa₃(X, Z, W))
DELETE_3_IN_AGA₃(X, ._2₂(Y, Z), W) -> DELETE_3_IN_AAA₃(X, Z, W)
DELETE_3_IN_AAA₃(X, ._2₂(Y, Z), W) -> IF_DELETE_3_IN_1_AAA₅(X, Y, Z, W, delete_3_in_aaa₃(X, Z, W))
DELETE_3_IN_AAA₃(X, ._2₂(Y, Z), W) -> DELETE_3_IN_AAA₃(X, Z, W)
IF_PERM_2_IN_1_AG₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> IF_PERM_2_IN_2_AG₆(X, Y, U, V, Z, perm_2_in_aa₂(Z, V))
IF_PERM_2_IN_1_AG₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> PERM_2_IN_AA₂(Z, V)
PERM_2_IN_AA₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> IF_PERM_2_IN_1_AA₅(X, Y, U, V, delete_3_in_aga₃(U, ._2₂(X, Y), Z))
PERM_2_IN_AA₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> DELETE_3_IN_AGA₃(U, ._2₂(X, Y), Z)
IF_PERM_2_IN_1_AA₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> IF_PERM_2_IN_2_AA₆(X, Y, U, V, Z, perm_2_in_aa₂(Z, V))
IF_PERM_2_IN_1_AA₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> PERM_2_IN_AA₂(Z, V)
IF_SORT_2_IN_1_AG₃(X, Y, perm_2_out_ag₂(X, Y)) -> IF_SORT_2_IN_2_AG₃(X, Y, sorted_1_in_g₁(Y))
IF_SORT_2_IN_1_AG₃(X, Y, perm_2_out_ag₂(X, Y)) -> SORTED_1_IN_G₁(Y)
SORTED_1_IN_G₁(._2₂(X, ._2₂(Y, Z))) -> IF_SORTED_1_IN_1_G₄(X, Y, Z, le_2_in_aa₂(X, Y))
SORTED_1_IN_G₁(._2₂(X, ._2₂(Y, Z))) -> LE_2_IN_AA₂(X, Y)
LE_2_IN_AA₂(s_1₁(X), s_1₁(Y)) -> IF_LE_2_IN_1_AA₃(X, Y, le_2_in_aa₂(X, Y))
LE_2_IN_AA₂(s_1₁(X), s_1₁(Y)) -> LE_2_IN_AA₂(X, Y)
IF_SORTED_1_IN_1_G₄(X, Y, Z, le_2_out_aa₂(X, Y)) -> IF_SORTED_1_IN_2_G₄(X, Y, Z, sorted_1_in_g₁(._2₂(Y, Z)))
IF_SORTED_1_IN_1_G₄(X, Y, Z, le_2_out_aa₂(X, Y)) -> SORTED_1_IN_G₁(._2₂(Y, Z))

The TRS R consists of the following rules:

sort_2_in_ag₂(X, Y) -> if_sort_2_in_1_ag₃(X, Y, perm_2_in_ag₂(X, Y))
perm_2_in_ag₂([]_0, []_0) -> perm_2_out_ag₂([]_0, []_0)
perm_2_in_ag₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> if_perm_2_in_1_ag₅(X, Y, U, V, delete_3_in_aga₃(U, ._2₂(X, Y), Z))
delete_3_in_aga₃(X, ._2₂(X, Y), Y) -> delete_3_out_aga₃(X, ._2₂(X, Y), Y)
delete_3_in_aga₃(X, ._2₂(Y, Z), W) -> if_delete_3_in_1_aga₅(X, Y, Z, W, delete_3_in_aaa₃(X, Z, W))
delete_3_in_aaa₃(X, ._2₂(X, Y), Y) -> delete_3_out_aaa₃(X, ._2₂(X, Y), Y)
delete_3_in_aaa₃(X, ._2₂(Y, Z), W) -> if_delete_3_in_1_aaa₅(X, Y, Z, W, delete_3_in_aaa₃(X, Z, W))
if_delete_3_in_1_aaa₅(X, Y, Z, W, delete_3_out_aaa₃(X, Z, W)) -> delete_3_out_aaa₃(X, ._2₂(Y, Z), W)
if_delete_3_in_1_aga₅(X, Y, Z, W, delete_3_out_aaa₃(X, Z, W)) -> delete_3_out_aga₃(X, ._2₂(Y, Z), W)
if_perm_2_in_1_ag₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> if_perm_2_in_2_ag₆(X, Y, U, V, Z, perm_2_in_aa₂(Z, V))
perm_2_in_aa₂([]_0, []_0) -> perm_2_out_aa₂([]_0, []_0)
perm_2_in_aa₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> if_perm_2_in_1_aa₅(X, Y, U, V, delete_3_in_aga₃(U, ._2₂(X, Y), Z))
if_perm_2_in_1_aa₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> if_perm_2_in_2_aa₆(X, Y, U, V, Z, perm_2_in_aa₂(Z, V))
if_perm_2_in_2_aa₆(X, Y, U, V, Z, perm_2_out_aa₂(Z, V)) -> perm_2_out_aa₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0)))
if_perm_2_in_2_ag₆(X, Y, U, V, Z, perm_2_out_aa₂(Z, V)) -> perm_2_out_ag₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0)))
if_sort_2_in_1_ag₃(X, Y, perm_2_out_ag₂(X, Y)) -> if_sort_2_in_2_ag₃(X, Y, sorted_1_in_g₁(Y))
sorted_1_in_g₁([]_0) -> sorted_1_out_g₁([]_0)
sorted_1_in_g₁(._2₂(X, []_0)) -> sorted_1_out_g₁(._2₂(X, []_0))
sorted_1_in_g₁(._2₂(X, ._2₂(Y, Z))) -> if_sorted_1_in_1_g₄(X, Y, Z, le_2_in_aa₂(X, Y))
le_2_in_aa₂(s_1₁(X), s_1₁(Y)) -> if_le_2_in_1_aa₃(X, Y, le_2_in_aa₂(X, Y))
le_2_in_aa₂(0_0, s_1₁(X)) -> le_2_out_aa₂(0_0, s_1₁(X))
le_2_in_aa₂(0_0, 0_0) -> le_2_out_aa₂(0_0, 0_0)
if_le_2_in_1_aa₃(X, Y, le_2_out_aa₂(X, Y)) -> le_2_out_aa₂(s_1₁(X), s_1₁(Y))
if_sorted_1_in_1_g₄(X, Y, Z, le_2_out_aa₂(X, Y)) -> if_sorted_1_in_2_g₄(X, Y, Z, sorted_1_in_g₁(._2₂(Y, Z)))
if_sorted_1_in_2_g₄(X, Y, Z, sorted_1_out_g₁(._2₂(Y, Z))) -> sorted_1_out_g₁(._2₂(X, ._2₂(Y, Z)))
if_sort_2_in_2_ag₃(X, Y, sorted_1_out_g₁(Y)) -> sort_2_out_ag₂(X, Y)

The argument filtering Pi contains the following mapping:
sort_2_in_ag₂(x1, x2) = sort_2_in_ag₁(x2)
[]_0 = []_0
._2₂(x1, x2) = ._2
s_1₁(x1) = s_1
0_0 = 0_0
if_sort_2_in_1_ag₃(x1, x2, x3) = if_sort_2_in_1_ag₂(x2, x3)
perm_2_in_ag₂(x1, x2) = perm_2_in_ag₁(x2)
perm_2_out_ag₂(x1, x2) = perm_2_out_ag₂(x1, x2)
if_perm_2_in_1_ag₅(x1, x2, x3, x4, x5) = if_perm_2_in_1_ag₁(x5)
delete_3_in_aga₃(x1, x2, x3) = delete_3_in_aga₁(x2)
delete_3_out_aga₃(x1, x2, x3) = delete_3_out_aga₁(x2)
if_delete_3_in_1_aga₅(x1, x2, x3, x4, x5) = if_delete_3_in_1_aga₁(x5)
delete_3_in_aaa₃(x1, x2, x3) = delete_3_in_aaa
delete_3_out_aaa₃(x1, x2, x3) = delete_3_out_aaa₁(x2)
if_delete_3_in_1_aaa₅(x1, x2, x3, x4, x5) = if_delete_3_in_1_aaa₁(x5)
if_perm_2_in_2_ag₆(x1, x2, x3, x4, x5, x6) = if_perm_2_in_2_ag₁(x6)
perm_2_in_aa₂(x1, x2) = perm_2_in_aa
perm_2_out_aa₂(x1, x2) = perm_2_out_aa₂(x1, x2)
if_perm_2_in_1_aa₅(x1, x2, x3, x4, x5) = if_perm_2_in_1_aa₁(x5)
if_perm_2_in_2_aa₆(x1, x2, x3, x4, x5, x6) = if_perm_2_in_2_aa₁(x6)
if_sort_2_in_2_ag₃(x1, x2, x3) = if_sort_2_in_2_ag₃(x1, x2, x3)
sorted_1_in_g₁(x1) = sorted_1_in_g₁(x1)
sorted_1_out_g₁(x1) = sorted_1_out_g₁(x1)
if_sorted_1_in_1_g₄(x1, x2, x3, x4) = if_sorted_1_in_1_g₁(x4)
le_2_in_aa₂(x1, x2) = le_2_in_aa
if_le_2_in_1_aa₃(x1, x2, x3) = if_le_2_in_1_aa₁(x3)
le_2_out_aa₂(x1, x2) = le_2_out_aa₂(x1, x2)
if_sorted_1_in_2_g₄(x1, x2, x3, x4) = if_sorted_1_in_2_g₁(x4)
sort_2_out_ag₂(x1, x2) = sort_2_out_ag₂(x1, x2)
IF_DELETE_3_IN_1_AAA₅(x1, x2, x3, x4, x5) = IF_DELETE_3_IN_1_AAA₁(x5)
IF_SORTED_1_IN_2_G₄(x1, x2, x3, x4) = IF_SORTED_1_IN_2_G₁(x4)
IF_SORT_2_IN_2_AG₃(x1, x2, x3) = IF_SORT_2_IN_2_AG₃(x1, x2, x3)
IF_SORT_2_IN_1_AG₃(x1, x2, x3) = IF_SORT_2_IN_1_AG₂(x2, x3)
PERM_2_IN_AG₂(x1, x2) = PERM_2_IN_AG₁(x2)
IF_DELETE_3_IN_1_AGA₅(x1, x2, x3, x4, x5) = IF_DELETE_3_IN_1_AGA₁(x5)
IF_PERM_2_IN_2_AA₆(x1, x2, x3, x4, x5, x6) = IF_PERM_2_IN_2_AA₁(x6)
PERM_2_IN_AA₂(x1, x2) = PERM_2_IN_AA
SORTED_1_IN_G₁(x1) = SORTED_1_IN_G₁(x1)
SORT_2_IN_AG₂(x1, x2) = SORT_2_IN_AG₁(x2)
LE_2_IN_AA₂(x1, x2) = LE_2_IN_AA
IF_LE_2_IN_1_AA₃(x1, x2, x3) = IF_LE_2_IN_1_AA₁(x3)
DELETE_3_IN_AGA₃(x1, x2, x3) = DELETE_3_IN_AGA₁(x2)
IF_PERM_2_IN_1_AG₅(x1, x2, x3, x4, x5) = IF_PERM_2_IN_1_AG₁(x5)
IF_PERM_2_IN_2_AG₆(x1, x2, x3, x4, x5, x6) = IF_PERM_2_IN_2_AG₁(x6)
IF_SORTED_1_IN_1_G₄(x1, x2, x3, x4) = IF_SORTED_1_IN_1_G₁(x4)
DELETE_3_IN_AAA₃(x1, x2, x3) = DELETE_3_IN_AAA
IF_PERM_2_IN_1_AA₅(x1, x2, x3, x4, x5) = IF_PERM_2_IN_1_AA₁(x5)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph contains 4 SCCs with 16 less nodes.

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

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

LE_2_IN_AA₂(s_1₁(X), s_1₁(Y)) -> LE_2_IN_AA₂(X, Y)

The TRS R consists of the following rules:

sort_2_in_ag₂(X, Y) -> if_sort_2_in_1_ag₃(X, Y, perm_2_in_ag₂(X, Y))
perm_2_in_ag₂([]_0, []_0) -> perm_2_out_ag₂([]_0, []_0)
perm_2_in_ag₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> if_perm_2_in_1_ag₅(X, Y, U, V, delete_3_in_aga₃(U, ._2₂(X, Y), Z))
delete_3_in_aga₃(X, ._2₂(X, Y), Y) -> delete_3_out_aga₃(X, ._2₂(X, Y), Y)
delete_3_in_aga₃(X, ._2₂(Y, Z), W) -> if_delete_3_in_1_aga₅(X, Y, Z, W, delete_3_in_aaa₃(X, Z, W))
delete_3_in_aaa₃(X, ._2₂(X, Y), Y) -> delete_3_out_aaa₃(X, ._2₂(X, Y), Y)
delete_3_in_aaa₃(X, ._2₂(Y, Z), W) -> if_delete_3_in_1_aaa₅(X, Y, Z, W, delete_3_in_aaa₃(X, Z, W))
if_delete_3_in_1_aaa₅(X, Y, Z, W, delete_3_out_aaa₃(X, Z, W)) -> delete_3_out_aaa₃(X, ._2₂(Y, Z), W)
if_delete_3_in_1_aga₅(X, Y, Z, W, delete_3_out_aaa₃(X, Z, W)) -> delete_3_out_aga₃(X, ._2₂(Y, Z), W)
if_perm_2_in_1_ag₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> if_perm_2_in_2_ag₆(X, Y, U, V, Z, perm_2_in_aa₂(Z, V))
perm_2_in_aa₂([]_0, []_0) -> perm_2_out_aa₂([]_0, []_0)
perm_2_in_aa₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> if_perm_2_in_1_aa₅(X, Y, U, V, delete_3_in_aga₃(U, ._2₂(X, Y), Z))
if_perm_2_in_1_aa₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> if_perm_2_in_2_aa₆(X, Y, U, V, Z, perm_2_in_aa₂(Z, V))
if_perm_2_in_2_aa₆(X, Y, U, V, Z, perm_2_out_aa₂(Z, V)) -> perm_2_out_aa₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0)))
if_perm_2_in_2_ag₆(X, Y, U, V, Z, perm_2_out_aa₂(Z, V)) -> perm_2_out_ag₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0)))
if_sort_2_in_1_ag₃(X, Y, perm_2_out_ag₂(X, Y)) -> if_sort_2_in_2_ag₃(X, Y, sorted_1_in_g₁(Y))
sorted_1_in_g₁([]_0) -> sorted_1_out_g₁([]_0)
sorted_1_in_g₁(._2₂(X, []_0)) -> sorted_1_out_g₁(._2₂(X, []_0))
sorted_1_in_g₁(._2₂(X, ._2₂(Y, Z))) -> if_sorted_1_in_1_g₄(X, Y, Z, le_2_in_aa₂(X, Y))
le_2_in_aa₂(s_1₁(X), s_1₁(Y)) -> if_le_2_in_1_aa₃(X, Y, le_2_in_aa₂(X, Y))
le_2_in_aa₂(0_0, s_1₁(X)) -> le_2_out_aa₂(0_0, s_1₁(X))
le_2_in_aa₂(0_0, 0_0) -> le_2_out_aa₂(0_0, 0_0)
if_le_2_in_1_aa₃(X, Y, le_2_out_aa₂(X, Y)) -> le_2_out_aa₂(s_1₁(X), s_1₁(Y))
if_sorted_1_in_1_g₄(X, Y, Z, le_2_out_aa₂(X, Y)) -> if_sorted_1_in_2_g₄(X, Y, Z, sorted_1_in_g₁(._2₂(Y, Z)))
if_sorted_1_in_2_g₄(X, Y, Z, sorted_1_out_g₁(._2₂(Y, Z))) -> sorted_1_out_g₁(._2₂(X, ._2₂(Y, Z)))
if_sort_2_in_2_ag₃(X, Y, sorted_1_out_g₁(Y)) -> sort_2_out_ag₂(X, Y)

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

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

LE_2_IN_AA₂(s_1₁(X), s_1₁(Y)) -> LE_2_IN_AA₂(X, Y)

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

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

LE_2_IN_AA -> LE_2_IN_AA

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {LE_2_IN_AA}.

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

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

IF_SORTED_1_IN_1_G₄(X, Y, Z, le_2_out_aa₂(X, Y)) -> SORTED_1_IN_G₁(._2₂(Y, Z))
SORTED_1_IN_G₁(._2₂(X, ._2₂(Y, Z))) -> IF_SORTED_1_IN_1_G₄(X, Y, Z, le_2_in_aa₂(X, Y))

The TRS R consists of the following rules:

sort_2_in_ag₂(X, Y) -> if_sort_2_in_1_ag₃(X, Y, perm_2_in_ag₂(X, Y))
perm_2_in_ag₂([]_0, []_0) -> perm_2_out_ag₂([]_0, []_0)
perm_2_in_ag₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> if_perm_2_in_1_ag₅(X, Y, U, V, delete_3_in_aga₃(U, ._2₂(X, Y), Z))
delete_3_in_aga₃(X, ._2₂(X, Y), Y) -> delete_3_out_aga₃(X, ._2₂(X, Y), Y)
delete_3_in_aga₃(X, ._2₂(Y, Z), W) -> if_delete_3_in_1_aga₅(X, Y, Z, W, delete_3_in_aaa₃(X, Z, W))
delete_3_in_aaa₃(X, ._2₂(X, Y), Y) -> delete_3_out_aaa₃(X, ._2₂(X, Y), Y)
delete_3_in_aaa₃(X, ._2₂(Y, Z), W) -> if_delete_3_in_1_aaa₅(X, Y, Z, W, delete_3_in_aaa₃(X, Z, W))
if_delete_3_in_1_aaa₅(X, Y, Z, W, delete_3_out_aaa₃(X, Z, W)) -> delete_3_out_aaa₃(X, ._2₂(Y, Z), W)
if_delete_3_in_1_aga₅(X, Y, Z, W, delete_3_out_aaa₃(X, Z, W)) -> delete_3_out_aga₃(X, ._2₂(Y, Z), W)
if_perm_2_in_1_ag₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> if_perm_2_in_2_ag₆(X, Y, U, V, Z, perm_2_in_aa₂(Z, V))
perm_2_in_aa₂([]_0, []_0) -> perm_2_out_aa₂([]_0, []_0)
perm_2_in_aa₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> if_perm_2_in_1_aa₅(X, Y, U, V, delete_3_in_aga₃(U, ._2₂(X, Y), Z))
if_perm_2_in_1_aa₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> if_perm_2_in_2_aa₆(X, Y, U, V, Z, perm_2_in_aa₂(Z, V))
if_perm_2_in_2_aa₆(X, Y, U, V, Z, perm_2_out_aa₂(Z, V)) -> perm_2_out_aa₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0)))
if_perm_2_in_2_ag₆(X, Y, U, V, Z, perm_2_out_aa₂(Z, V)) -> perm_2_out_ag₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0)))
if_sort_2_in_1_ag₃(X, Y, perm_2_out_ag₂(X, Y)) -> if_sort_2_in_2_ag₃(X, Y, sorted_1_in_g₁(Y))
sorted_1_in_g₁([]_0) -> sorted_1_out_g₁([]_0)
sorted_1_in_g₁(._2₂(X, []_0)) -> sorted_1_out_g₁(._2₂(X, []_0))
sorted_1_in_g₁(._2₂(X, ._2₂(Y, Z))) -> if_sorted_1_in_1_g₄(X, Y, Z, le_2_in_aa₂(X, Y))
le_2_in_aa₂(s_1₁(X), s_1₁(Y)) -> if_le_2_in_1_aa₃(X, Y, le_2_in_aa₂(X, Y))
le_2_in_aa₂(0_0, s_1₁(X)) -> le_2_out_aa₂(0_0, s_1₁(X))
le_2_in_aa₂(0_0, 0_0) -> le_2_out_aa₂(0_0, 0_0)
if_le_2_in_1_aa₃(X, Y, le_2_out_aa₂(X, Y)) -> le_2_out_aa₂(s_1₁(X), s_1₁(Y))
if_sorted_1_in_1_g₄(X, Y, Z, le_2_out_aa₂(X, Y)) -> if_sorted_1_in_2_g₄(X, Y, Z, sorted_1_in_g₁(._2₂(Y, Z)))
if_sorted_1_in_2_g₄(X, Y, Z, sorted_1_out_g₁(._2₂(Y, Z))) -> sorted_1_out_g₁(._2₂(X, ._2₂(Y, Z)))
if_sort_2_in_2_ag₃(X, Y, sorted_1_out_g₁(Y)) -> sort_2_out_ag₂(X, Y)

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

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

IF_SORTED_1_IN_1_G₄(X, Y, Z, le_2_out_aa₂(X, Y)) -> SORTED_1_IN_G₁(._2₂(Y, Z))
SORTED_1_IN_G₁(._2₂(X, ._2₂(Y, Z))) -> IF_SORTED_1_IN_1_G₄(X, Y, Z, le_2_in_aa₂(X, Y))

The TRS R consists of the following rules:

le_2_in_aa₂(s_1₁(X), s_1₁(Y)) -> if_le_2_in_1_aa₃(X, Y, le_2_in_aa₂(X, Y))
le_2_in_aa₂(0_0, s_1₁(X)) -> le_2_out_aa₂(0_0, s_1₁(X))
le_2_in_aa₂(0_0, 0_0) -> le_2_out_aa₂(0_0, 0_0)
if_le_2_in_1_aa₃(X, Y, le_2_out_aa₂(X, Y)) -> le_2_out_aa₂(s_1₁(X), s_1₁(Y))

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

              ↳ PiDP

              ↳ PiDP

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

IF_SORTED_1_IN_1_G₁(le_2_out_aa₂(X, Y)) -> SORTED_1_IN_G₁(._2)
SORTED_1_IN_G₁(._2) -> IF_SORTED_1_IN_1_G₁(le_2_in_aa)

The TRS R consists of the following rules:

le_2_in_aa -> if_le_2_in_1_aa₁(le_2_in_aa)
le_2_in_aa -> le_2_out_aa₂(0_0, s_1)
le_2_in_aa -> le_2_out_aa₂(0_0, 0_0)
if_le_2_in_1_aa₁(le_2_out_aa₂(X, Y)) -> le_2_out_aa₂(s_1, s_1)

The set Q consists of the following terms:

le_2_in_aa
if_le_2_in_1_aa₁(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {SORTED_1_IN_G₁, IF_SORTED_1_IN_1_G₁}.

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

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

DELETE_3_IN_AAA₃(X, ._2₂(Y, Z), W) -> DELETE_3_IN_AAA₃(X, Z, W)

The TRS R consists of the following rules:

sort_2_in_ag₂(X, Y) -> if_sort_2_in_1_ag₃(X, Y, perm_2_in_ag₂(X, Y))
perm_2_in_ag₂([]_0, []_0) -> perm_2_out_ag₂([]_0, []_0)
perm_2_in_ag₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> if_perm_2_in_1_ag₅(X, Y, U, V, delete_3_in_aga₃(U, ._2₂(X, Y), Z))
delete_3_in_aga₃(X, ._2₂(X, Y), Y) -> delete_3_out_aga₃(X, ._2₂(X, Y), Y)
delete_3_in_aga₃(X, ._2₂(Y, Z), W) -> if_delete_3_in_1_aga₅(X, Y, Z, W, delete_3_in_aaa₃(X, Z, W))
delete_3_in_aaa₃(X, ._2₂(X, Y), Y) -> delete_3_out_aaa₃(X, ._2₂(X, Y), Y)
delete_3_in_aaa₃(X, ._2₂(Y, Z), W) -> if_delete_3_in_1_aaa₅(X, Y, Z, W, delete_3_in_aaa₃(X, Z, W))
if_delete_3_in_1_aaa₅(X, Y, Z, W, delete_3_out_aaa₃(X, Z, W)) -> delete_3_out_aaa₃(X, ._2₂(Y, Z), W)
if_delete_3_in_1_aga₅(X, Y, Z, W, delete_3_out_aaa₃(X, Z, W)) -> delete_3_out_aga₃(X, ._2₂(Y, Z), W)
if_perm_2_in_1_ag₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> if_perm_2_in_2_ag₆(X, Y, U, V, Z, perm_2_in_aa₂(Z, V))
perm_2_in_aa₂([]_0, []_0) -> perm_2_out_aa₂([]_0, []_0)
perm_2_in_aa₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> if_perm_2_in_1_aa₅(X, Y, U, V, delete_3_in_aga₃(U, ._2₂(X, Y), Z))
if_perm_2_in_1_aa₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> if_perm_2_in_2_aa₆(X, Y, U, V, Z, perm_2_in_aa₂(Z, V))
if_perm_2_in_2_aa₆(X, Y, U, V, Z, perm_2_out_aa₂(Z, V)) -> perm_2_out_aa₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0)))
if_perm_2_in_2_ag₆(X, Y, U, V, Z, perm_2_out_aa₂(Z, V)) -> perm_2_out_ag₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0)))
if_sort_2_in_1_ag₃(X, Y, perm_2_out_ag₂(X, Y)) -> if_sort_2_in_2_ag₃(X, Y, sorted_1_in_g₁(Y))
sorted_1_in_g₁([]_0) -> sorted_1_out_g₁([]_0)
sorted_1_in_g₁(._2₂(X, []_0)) -> sorted_1_out_g₁(._2₂(X, []_0))
sorted_1_in_g₁(._2₂(X, ._2₂(Y, Z))) -> if_sorted_1_in_1_g₄(X, Y, Z, le_2_in_aa₂(X, Y))
le_2_in_aa₂(s_1₁(X), s_1₁(Y)) -> if_le_2_in_1_aa₃(X, Y, le_2_in_aa₂(X, Y))
le_2_in_aa₂(0_0, s_1₁(X)) -> le_2_out_aa₂(0_0, s_1₁(X))
le_2_in_aa₂(0_0, 0_0) -> le_2_out_aa₂(0_0, 0_0)
if_le_2_in_1_aa₃(X, Y, le_2_out_aa₂(X, Y)) -> le_2_out_aa₂(s_1₁(X), s_1₁(Y))
if_sorted_1_in_1_g₄(X, Y, Z, le_2_out_aa₂(X, Y)) -> if_sorted_1_in_2_g₄(X, Y, Z, sorted_1_in_g₁(._2₂(Y, Z)))
if_sorted_1_in_2_g₄(X, Y, Z, sorted_1_out_g₁(._2₂(Y, Z))) -> sorted_1_out_g₁(._2₂(X, ._2₂(Y, Z)))
if_sort_2_in_2_ag₃(X, Y, sorted_1_out_g₁(Y)) -> sort_2_out_ag₂(X, Y)

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

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

DELETE_3_IN_AAA₃(X, ._2₂(Y, Z), W) -> DELETE_3_IN_AAA₃(X, Z, W)

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

              ↳ PiDP

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

DELETE_3_IN_AAA -> DELETE_3_IN_AAA

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {DELETE_3_IN_AAA}.

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

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

IF_PERM_2_IN_1_AA₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> PERM_2_IN_AA₂(Z, V)
PERM_2_IN_AA₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> IF_PERM_2_IN_1_AA₅(X, Y, U, V, delete_3_in_aga₃(U, ._2₂(X, Y), Z))

The TRS R consists of the following rules:

sort_2_in_ag₂(X, Y) -> if_sort_2_in_1_ag₃(X, Y, perm_2_in_ag₂(X, Y))
perm_2_in_ag₂([]_0, []_0) -> perm_2_out_ag₂([]_0, []_0)
perm_2_in_ag₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> if_perm_2_in_1_ag₅(X, Y, U, V, delete_3_in_aga₃(U, ._2₂(X, Y), Z))
delete_3_in_aga₃(X, ._2₂(X, Y), Y) -> delete_3_out_aga₃(X, ._2₂(X, Y), Y)
delete_3_in_aga₃(X, ._2₂(Y, Z), W) -> if_delete_3_in_1_aga₅(X, Y, Z, W, delete_3_in_aaa₃(X, Z, W))
delete_3_in_aaa₃(X, ._2₂(X, Y), Y) -> delete_3_out_aaa₃(X, ._2₂(X, Y), Y)
delete_3_in_aaa₃(X, ._2₂(Y, Z), W) -> if_delete_3_in_1_aaa₅(X, Y, Z, W, delete_3_in_aaa₃(X, Z, W))
if_delete_3_in_1_aaa₅(X, Y, Z, W, delete_3_out_aaa₃(X, Z, W)) -> delete_3_out_aaa₃(X, ._2₂(Y, Z), W)
if_delete_3_in_1_aga₅(X, Y, Z, W, delete_3_out_aaa₃(X, Z, W)) -> delete_3_out_aga₃(X, ._2₂(Y, Z), W)
if_perm_2_in_1_ag₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> if_perm_2_in_2_ag₆(X, Y, U, V, Z, perm_2_in_aa₂(Z, V))
perm_2_in_aa₂([]_0, []_0) -> perm_2_out_aa₂([]_0, []_0)
perm_2_in_aa₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> if_perm_2_in_1_aa₅(X, Y, U, V, delete_3_in_aga₃(U, ._2₂(X, Y), Z))
if_perm_2_in_1_aa₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> if_perm_2_in_2_aa₆(X, Y, U, V, Z, perm_2_in_aa₂(Z, V))
if_perm_2_in_2_aa₆(X, Y, U, V, Z, perm_2_out_aa₂(Z, V)) -> perm_2_out_aa₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0)))
if_perm_2_in_2_ag₆(X, Y, U, V, Z, perm_2_out_aa₂(Z, V)) -> perm_2_out_ag₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0)))
if_sort_2_in_1_ag₃(X, Y, perm_2_out_ag₂(X, Y)) -> if_sort_2_in_2_ag₃(X, Y, sorted_1_in_g₁(Y))
sorted_1_in_g₁([]_0) -> sorted_1_out_g₁([]_0)
sorted_1_in_g₁(._2₂(X, []_0)) -> sorted_1_out_g₁(._2₂(X, []_0))
sorted_1_in_g₁(._2₂(X, ._2₂(Y, Z))) -> if_sorted_1_in_1_g₄(X, Y, Z, le_2_in_aa₂(X, Y))
le_2_in_aa₂(s_1₁(X), s_1₁(Y)) -> if_le_2_in_1_aa₃(X, Y, le_2_in_aa₂(X, Y))
le_2_in_aa₂(0_0, s_1₁(X)) -> le_2_out_aa₂(0_0, s_1₁(X))
le_2_in_aa₂(0_0, 0_0) -> le_2_out_aa₂(0_0, 0_0)
if_le_2_in_1_aa₃(X, Y, le_2_out_aa₂(X, Y)) -> le_2_out_aa₂(s_1₁(X), s_1₁(Y))
if_sorted_1_in_1_g₄(X, Y, Z, le_2_out_aa₂(X, Y)) -> if_sorted_1_in_2_g₄(X, Y, Z, sorted_1_in_g₁(._2₂(Y, Z)))
if_sorted_1_in_2_g₄(X, Y, Z, sorted_1_out_g₁(._2₂(Y, Z))) -> sorted_1_out_g₁(._2₂(X, ._2₂(Y, Z)))
if_sort_2_in_2_ag₃(X, Y, sorted_1_out_g₁(Y)) -> sort_2_out_ag₂(X, Y)

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

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

IF_PERM_2_IN_1_AA₅(X, Y, U, V, delete_3_out_aga₃(U, ._2₂(X, Y), Z)) -> PERM_2_IN_AA₂(Z, V)
PERM_2_IN_AA₂(._2₂(X, ._2₂(Y, []_0)), ._2₂(U, ._2₂(V, []_0))) -> IF_PERM_2_IN_1_AA₅(X, Y, U, V, delete_3_in_aga₃(U, ._2₂(X, Y), Z))

The TRS R consists of the following rules:

delete_3_in_aga₃(X, ._2₂(X, Y), Y) -> delete_3_out_aga₃(X, ._2₂(X, Y), Y)
delete_3_in_aga₃(X, ._2₂(Y, Z), W) -> if_delete_3_in_1_aga₅(X, Y, Z, W, delete_3_in_aaa₃(X, Z, W))
if_delete_3_in_1_aga₅(X, Y, Z, W, delete_3_out_aaa₃(X, Z, W)) -> delete_3_out_aga₃(X, ._2₂(Y, Z), W)
delete_3_in_aaa₃(X, ._2₂(X, Y), Y) -> delete_3_out_aaa₃(X, ._2₂(X, Y), Y)
delete_3_in_aaa₃(X, ._2₂(Y, Z), W) -> if_delete_3_in_1_aaa₅(X, Y, Z, W, delete_3_in_aaa₃(X, Z, W))
if_delete_3_in_1_aaa₅(X, Y, Z, W, delete_3_out_aaa₃(X, Z, W)) -> delete_3_out_aaa₃(X, ._2₂(Y, Z), W)

The argument filtering Pi contains the following mapping:
[]_0 = []_0
._2₂(x1, x2) = ._2
delete_3_in_aga₃(x1, x2, x3) = delete_3_in_aga₁(x2)
delete_3_out_aga₃(x1, x2, x3) = delete_3_out_aga₁(x2)
if_delete_3_in_1_aga₅(x1, x2, x3, x4, x5) = if_delete_3_in_1_aga₁(x5)
delete_3_in_aaa₃(x1, x2, x3) = delete_3_in_aaa
delete_3_out_aaa₃(x1, x2, x3) = delete_3_out_aaa₁(x2)
if_delete_3_in_1_aaa₅(x1, x2, x3, x4, x5) = if_delete_3_in_1_aaa₁(x5)
PERM_2_IN_AA₂(x1, x2) = PERM_2_IN_AA
IF_PERM_2_IN_1_AA₅(x1, x2, x3, x4, x5) = IF_PERM_2_IN_1_AA₁(x5)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

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

IF_PERM_2_IN_1_AA₁(delete_3_out_aga₁(._2)) -> PERM_2_IN_AA
PERM_2_IN_AA -> IF_PERM_2_IN_1_AA₁(delete_3_in_aga₁(._2))

The TRS R consists of the following rules:

delete_3_in_aga₁(._2) -> delete_3_out_aga₁(._2)
delete_3_in_aga₁(._2) -> if_delete_3_in_1_aga₁(delete_3_in_aaa)
if_delete_3_in_1_aga₁(delete_3_out_aaa₁(Z)) -> delete_3_out_aga₁(._2)
delete_3_in_aaa -> delete_3_out_aaa₁(._2)
delete_3_in_aaa -> if_delete_3_in_1_aaa₁(delete_3_in_aaa)
if_delete_3_in_1_aaa₁(delete_3_out_aaa₁(Z)) -> delete_3_out_aaa₁(._2)

The set Q consists of the following terms:

delete_3_in_aga₁(x0)
if_delete_3_in_1_aga₁(x0)
delete_3_in_aaa
if_delete_3_in_1_aaa₁(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {PERM_2_IN_AA, IF_PERM_2_IN_1_AA₁}.