↳ PROLOG
↳ PrologToPiTRSProof
With regard to the inferred argument filtering the predicates were used in the following modes:
sort2: (b,f)
perm2: (b,f)
delete3: (f,b,f)
sorted1: (b)
le2: (b,b)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
sort_2_in_ga2(X, Y) -> if_sort_2_in_1_ga3(X, Y, perm_2_in_ga2(X, Y))
perm_2_in_ga2([]_0, []_0) -> perm_2_out_ga2([]_0, []_0)
perm_2_in_ga2(._22(X, ._22(Y, []_0)), ._22(U, ._22(V, []_0))) -> if_perm_2_in_1_ga5(X, Y, U, V, delete_3_in_aga3(U, ._22(X, Y), Z))
delete_3_in_aga3(X, ._22(X, Y), Y) -> delete_3_out_aga3(X, ._22(X, Y), Y)
delete_3_in_aga3(X, ._22(Y, Z), W) -> if_delete_3_in_1_aga5(X, Y, Z, W, delete_3_in_aga3(X, Z, W))
if_delete_3_in_1_aga5(X, Y, Z, W, delete_3_out_aga3(X, Z, W)) -> delete_3_out_aga3(X, ._22(Y, Z), W)
if_perm_2_in_1_ga5(X, Y, U, V, delete_3_out_aga3(U, ._22(X, Y), Z)) -> if_perm_2_in_2_ga6(X, Y, U, V, Z, perm_2_in_ga2(Z, V))
if_perm_2_in_2_ga6(X, Y, U, V, Z, perm_2_out_ga2(Z, V)) -> perm_2_out_ga2(._22(X, ._22(Y, []_0)), ._22(U, ._22(V, []_0)))
if_sort_2_in_1_ga3(X, Y, perm_2_out_ga2(X, Y)) -> if_sort_2_in_2_ga3(X, Y, sorted_1_in_g1(Y))
sorted_1_in_g1([]_0) -> sorted_1_out_g1([]_0)
sorted_1_in_g1(._22(X, []_0)) -> sorted_1_out_g1(._22(X, []_0))
sorted_1_in_g1(._22(X, ._22(Y, Z))) -> if_sorted_1_in_1_g4(X, Y, Z, le_2_in_gg2(X, Y))
le_2_in_gg2(s_11(X), s_11(Y)) -> if_le_2_in_1_gg3(X, Y, le_2_in_gg2(X, Y))
le_2_in_gg2(0_0, s_11(X)) -> le_2_out_gg2(0_0, s_11(X))
le_2_in_gg2(0_0, 0_0) -> le_2_out_gg2(0_0, 0_0)
if_le_2_in_1_gg3(X, Y, le_2_out_gg2(X, Y)) -> le_2_out_gg2(s_11(X), s_11(Y))
if_sorted_1_in_1_g4(X, Y, Z, le_2_out_gg2(X, Y)) -> if_sorted_1_in_2_g4(X, Y, Z, sorted_1_in_g1(._22(Y, Z)))
if_sorted_1_in_2_g4(X, Y, Z, sorted_1_out_g1(._22(Y, Z))) -> sorted_1_out_g1(._22(X, ._22(Y, Z)))
if_sort_2_in_2_ga3(X, Y, sorted_1_out_g1(Y)) -> sort_2_out_ga2(X, Y)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
sort_2_in_ga2(X, Y) -> if_sort_2_in_1_ga3(X, Y, perm_2_in_ga2(X, Y))
perm_2_in_ga2([]_0, []_0) -> perm_2_out_ga2([]_0, []_0)
perm_2_in_ga2(._22(X, ._22(Y, []_0)), ._22(U, ._22(V, []_0))) -> if_perm_2_in_1_ga5(X, Y, U, V, delete_3_in_aga3(U, ._22(X, Y), Z))
delete_3_in_aga3(X, ._22(X, Y), Y) -> delete_3_out_aga3(X, ._22(X, Y), Y)
delete_3_in_aga3(X, ._22(Y, Z), W) -> if_delete_3_in_1_aga5(X, Y, Z, W, delete_3_in_aga3(X, Z, W))
if_delete_3_in_1_aga5(X, Y, Z, W, delete_3_out_aga3(X, Z, W)) -> delete_3_out_aga3(X, ._22(Y, Z), W)
if_perm_2_in_1_ga5(X, Y, U, V, delete_3_out_aga3(U, ._22(X, Y), Z)) -> if_perm_2_in_2_ga6(X, Y, U, V, Z, perm_2_in_ga2(Z, V))
if_perm_2_in_2_ga6(X, Y, U, V, Z, perm_2_out_ga2(Z, V)) -> perm_2_out_ga2(._22(X, ._22(Y, []_0)), ._22(U, ._22(V, []_0)))
if_sort_2_in_1_ga3(X, Y, perm_2_out_ga2(X, Y)) -> if_sort_2_in_2_ga3(X, Y, sorted_1_in_g1(Y))
sorted_1_in_g1([]_0) -> sorted_1_out_g1([]_0)
sorted_1_in_g1(._22(X, []_0)) -> sorted_1_out_g1(._22(X, []_0))
sorted_1_in_g1(._22(X, ._22(Y, Z))) -> if_sorted_1_in_1_g4(X, Y, Z, le_2_in_gg2(X, Y))
le_2_in_gg2(s_11(X), s_11(Y)) -> if_le_2_in_1_gg3(X, Y, le_2_in_gg2(X, Y))
le_2_in_gg2(0_0, s_11(X)) -> le_2_out_gg2(0_0, s_11(X))
le_2_in_gg2(0_0, 0_0) -> le_2_out_gg2(0_0, 0_0)
if_le_2_in_1_gg3(X, Y, le_2_out_gg2(X, Y)) -> le_2_out_gg2(s_11(X), s_11(Y))
if_sorted_1_in_1_g4(X, Y, Z, le_2_out_gg2(X, Y)) -> if_sorted_1_in_2_g4(X, Y, Z, sorted_1_in_g1(._22(Y, Z)))
if_sorted_1_in_2_g4(X, Y, Z, sorted_1_out_g1(._22(Y, Z))) -> sorted_1_out_g1(._22(X, ._22(Y, Z)))
if_sort_2_in_2_ga3(X, Y, sorted_1_out_g1(Y)) -> sort_2_out_ga2(X, Y)
SORT_2_IN_GA2(X, Y) -> IF_SORT_2_IN_1_GA3(X, Y, perm_2_in_ga2(X, Y))
SORT_2_IN_GA2(X, Y) -> PERM_2_IN_GA2(X, Y)
PERM_2_IN_GA2(._22(X, ._22(Y, []_0)), ._22(U, ._22(V, []_0))) -> IF_PERM_2_IN_1_GA5(X, Y, U, V, delete_3_in_aga3(U, ._22(X, Y), Z))
PERM_2_IN_GA2(._22(X, ._22(Y, []_0)), ._22(U, ._22(V, []_0))) -> DELETE_3_IN_AGA3(U, ._22(X, Y), Z)
DELETE_3_IN_AGA3(X, ._22(Y, Z), W) -> IF_DELETE_3_IN_1_AGA5(X, Y, Z, W, delete_3_in_aga3(X, Z, W))
DELETE_3_IN_AGA3(X, ._22(Y, Z), W) -> DELETE_3_IN_AGA3(X, Z, W)
IF_PERM_2_IN_1_GA5(X, Y, U, V, delete_3_out_aga3(U, ._22(X, Y), Z)) -> IF_PERM_2_IN_2_GA6(X, Y, U, V, Z, perm_2_in_ga2(Z, V))
IF_PERM_2_IN_1_GA5(X, Y, U, V, delete_3_out_aga3(U, ._22(X, Y), Z)) -> PERM_2_IN_GA2(Z, V)
IF_SORT_2_IN_1_GA3(X, Y, perm_2_out_ga2(X, Y)) -> IF_SORT_2_IN_2_GA3(X, Y, sorted_1_in_g1(Y))
IF_SORT_2_IN_1_GA3(X, Y, perm_2_out_ga2(X, Y)) -> SORTED_1_IN_G1(Y)
SORTED_1_IN_G1(._22(X, ._22(Y, Z))) -> IF_SORTED_1_IN_1_G4(X, Y, Z, le_2_in_gg2(X, Y))
SORTED_1_IN_G1(._22(X, ._22(Y, Z))) -> LE_2_IN_GG2(X, Y)
LE_2_IN_GG2(s_11(X), s_11(Y)) -> IF_LE_2_IN_1_GG3(X, Y, le_2_in_gg2(X, Y))
LE_2_IN_GG2(s_11(X), s_11(Y)) -> LE_2_IN_GG2(X, Y)
IF_SORTED_1_IN_1_G4(X, Y, Z, le_2_out_gg2(X, Y)) -> IF_SORTED_1_IN_2_G4(X, Y, Z, sorted_1_in_g1(._22(Y, Z)))
IF_SORTED_1_IN_1_G4(X, Y, Z, le_2_out_gg2(X, Y)) -> SORTED_1_IN_G1(._22(Y, Z))
sort_2_in_ga2(X, Y) -> if_sort_2_in_1_ga3(X, Y, perm_2_in_ga2(X, Y))
perm_2_in_ga2([]_0, []_0) -> perm_2_out_ga2([]_0, []_0)
perm_2_in_ga2(._22(X, ._22(Y, []_0)), ._22(U, ._22(V, []_0))) -> if_perm_2_in_1_ga5(X, Y, U, V, delete_3_in_aga3(U, ._22(X, Y), Z))
delete_3_in_aga3(X, ._22(X, Y), Y) -> delete_3_out_aga3(X, ._22(X, Y), Y)
delete_3_in_aga3(X, ._22(Y, Z), W) -> if_delete_3_in_1_aga5(X, Y, Z, W, delete_3_in_aga3(X, Z, W))
if_delete_3_in_1_aga5(X, Y, Z, W, delete_3_out_aga3(X, Z, W)) -> delete_3_out_aga3(X, ._22(Y, Z), W)
if_perm_2_in_1_ga5(X, Y, U, V, delete_3_out_aga3(U, ._22(X, Y), Z)) -> if_perm_2_in_2_ga6(X, Y, U, V, Z, perm_2_in_ga2(Z, V))
if_perm_2_in_2_ga6(X, Y, U, V, Z, perm_2_out_ga2(Z, V)) -> perm_2_out_ga2(._22(X, ._22(Y, []_0)), ._22(U, ._22(V, []_0)))
if_sort_2_in_1_ga3(X, Y, perm_2_out_ga2(X, Y)) -> if_sort_2_in_2_ga3(X, Y, sorted_1_in_g1(Y))
sorted_1_in_g1([]_0) -> sorted_1_out_g1([]_0)
sorted_1_in_g1(._22(X, []_0)) -> sorted_1_out_g1(._22(X, []_0))
sorted_1_in_g1(._22(X, ._22(Y, Z))) -> if_sorted_1_in_1_g4(X, Y, Z, le_2_in_gg2(X, Y))
le_2_in_gg2(s_11(X), s_11(Y)) -> if_le_2_in_1_gg3(X, Y, le_2_in_gg2(X, Y))
le_2_in_gg2(0_0, s_11(X)) -> le_2_out_gg2(0_0, s_11(X))
le_2_in_gg2(0_0, 0_0) -> le_2_out_gg2(0_0, 0_0)
if_le_2_in_1_gg3(X, Y, le_2_out_gg2(X, Y)) -> le_2_out_gg2(s_11(X), s_11(Y))
if_sorted_1_in_1_g4(X, Y, Z, le_2_out_gg2(X, Y)) -> if_sorted_1_in_2_g4(X, Y, Z, sorted_1_in_g1(._22(Y, Z)))
if_sorted_1_in_2_g4(X, Y, Z, sorted_1_out_g1(._22(Y, Z))) -> sorted_1_out_g1(._22(X, ._22(Y, Z)))
if_sort_2_in_2_ga3(X, Y, sorted_1_out_g1(Y)) -> sort_2_out_ga2(X, Y)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
SORT_2_IN_GA2(X, Y) -> IF_SORT_2_IN_1_GA3(X, Y, perm_2_in_ga2(X, Y))
SORT_2_IN_GA2(X, Y) -> PERM_2_IN_GA2(X, Y)
PERM_2_IN_GA2(._22(X, ._22(Y, []_0)), ._22(U, ._22(V, []_0))) -> IF_PERM_2_IN_1_GA5(X, Y, U, V, delete_3_in_aga3(U, ._22(X, Y), Z))
PERM_2_IN_GA2(._22(X, ._22(Y, []_0)), ._22(U, ._22(V, []_0))) -> DELETE_3_IN_AGA3(U, ._22(X, Y), Z)
DELETE_3_IN_AGA3(X, ._22(Y, Z), W) -> IF_DELETE_3_IN_1_AGA5(X, Y, Z, W, delete_3_in_aga3(X, Z, W))
DELETE_3_IN_AGA3(X, ._22(Y, Z), W) -> DELETE_3_IN_AGA3(X, Z, W)
IF_PERM_2_IN_1_GA5(X, Y, U, V, delete_3_out_aga3(U, ._22(X, Y), Z)) -> IF_PERM_2_IN_2_GA6(X, Y, U, V, Z, perm_2_in_ga2(Z, V))
IF_PERM_2_IN_1_GA5(X, Y, U, V, delete_3_out_aga3(U, ._22(X, Y), Z)) -> PERM_2_IN_GA2(Z, V)
IF_SORT_2_IN_1_GA3(X, Y, perm_2_out_ga2(X, Y)) -> IF_SORT_2_IN_2_GA3(X, Y, sorted_1_in_g1(Y))
IF_SORT_2_IN_1_GA3(X, Y, perm_2_out_ga2(X, Y)) -> SORTED_1_IN_G1(Y)
SORTED_1_IN_G1(._22(X, ._22(Y, Z))) -> IF_SORTED_1_IN_1_G4(X, Y, Z, le_2_in_gg2(X, Y))
SORTED_1_IN_G1(._22(X, ._22(Y, Z))) -> LE_2_IN_GG2(X, Y)
LE_2_IN_GG2(s_11(X), s_11(Y)) -> IF_LE_2_IN_1_GG3(X, Y, le_2_in_gg2(X, Y))
LE_2_IN_GG2(s_11(X), s_11(Y)) -> LE_2_IN_GG2(X, Y)
IF_SORTED_1_IN_1_G4(X, Y, Z, le_2_out_gg2(X, Y)) -> IF_SORTED_1_IN_2_G4(X, Y, Z, sorted_1_in_g1(._22(Y, Z)))
IF_SORTED_1_IN_1_G4(X, Y, Z, le_2_out_gg2(X, Y)) -> SORTED_1_IN_G1(._22(Y, Z))
sort_2_in_ga2(X, Y) -> if_sort_2_in_1_ga3(X, Y, perm_2_in_ga2(X, Y))
perm_2_in_ga2([]_0, []_0) -> perm_2_out_ga2([]_0, []_0)
perm_2_in_ga2(._22(X, ._22(Y, []_0)), ._22(U, ._22(V, []_0))) -> if_perm_2_in_1_ga5(X, Y, U, V, delete_3_in_aga3(U, ._22(X, Y), Z))
delete_3_in_aga3(X, ._22(X, Y), Y) -> delete_3_out_aga3(X, ._22(X, Y), Y)
delete_3_in_aga3(X, ._22(Y, Z), W) -> if_delete_3_in_1_aga5(X, Y, Z, W, delete_3_in_aga3(X, Z, W))
if_delete_3_in_1_aga5(X, Y, Z, W, delete_3_out_aga3(X, Z, W)) -> delete_3_out_aga3(X, ._22(Y, Z), W)
if_perm_2_in_1_ga5(X, Y, U, V, delete_3_out_aga3(U, ._22(X, Y), Z)) -> if_perm_2_in_2_ga6(X, Y, U, V, Z, perm_2_in_ga2(Z, V))
if_perm_2_in_2_ga6(X, Y, U, V, Z, perm_2_out_ga2(Z, V)) -> perm_2_out_ga2(._22(X, ._22(Y, []_0)), ._22(U, ._22(V, []_0)))
if_sort_2_in_1_ga3(X, Y, perm_2_out_ga2(X, Y)) -> if_sort_2_in_2_ga3(X, Y, sorted_1_in_g1(Y))
sorted_1_in_g1([]_0) -> sorted_1_out_g1([]_0)
sorted_1_in_g1(._22(X, []_0)) -> sorted_1_out_g1(._22(X, []_0))
sorted_1_in_g1(._22(X, ._22(Y, Z))) -> if_sorted_1_in_1_g4(X, Y, Z, le_2_in_gg2(X, Y))
le_2_in_gg2(s_11(X), s_11(Y)) -> if_le_2_in_1_gg3(X, Y, le_2_in_gg2(X, Y))
le_2_in_gg2(0_0, s_11(X)) -> le_2_out_gg2(0_0, s_11(X))
le_2_in_gg2(0_0, 0_0) -> le_2_out_gg2(0_0, 0_0)
if_le_2_in_1_gg3(X, Y, le_2_out_gg2(X, Y)) -> le_2_out_gg2(s_11(X), s_11(Y))
if_sorted_1_in_1_g4(X, Y, Z, le_2_out_gg2(X, Y)) -> if_sorted_1_in_2_g4(X, Y, Z, sorted_1_in_g1(._22(Y, Z)))
if_sorted_1_in_2_g4(X, Y, Z, sorted_1_out_g1(._22(Y, Z))) -> sorted_1_out_g1(._22(X, ._22(Y, Z)))
if_sort_2_in_2_ga3(X, Y, sorted_1_out_g1(Y)) -> sort_2_out_ga2(X, Y)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDP
↳ PiDP
LE_2_IN_GG2(s_11(X), s_11(Y)) -> LE_2_IN_GG2(X, Y)
sort_2_in_ga2(X, Y) -> if_sort_2_in_1_ga3(X, Y, perm_2_in_ga2(X, Y))
perm_2_in_ga2([]_0, []_0) -> perm_2_out_ga2([]_0, []_0)
perm_2_in_ga2(._22(X, ._22(Y, []_0)), ._22(U, ._22(V, []_0))) -> if_perm_2_in_1_ga5(X, Y, U, V, delete_3_in_aga3(U, ._22(X, Y), Z))
delete_3_in_aga3(X, ._22(X, Y), Y) -> delete_3_out_aga3(X, ._22(X, Y), Y)
delete_3_in_aga3(X, ._22(Y, Z), W) -> if_delete_3_in_1_aga5(X, Y, Z, W, delete_3_in_aga3(X, Z, W))
if_delete_3_in_1_aga5(X, Y, Z, W, delete_3_out_aga3(X, Z, W)) -> delete_3_out_aga3(X, ._22(Y, Z), W)
if_perm_2_in_1_ga5(X, Y, U, V, delete_3_out_aga3(U, ._22(X, Y), Z)) -> if_perm_2_in_2_ga6(X, Y, U, V, Z, perm_2_in_ga2(Z, V))
if_perm_2_in_2_ga6(X, Y, U, V, Z, perm_2_out_ga2(Z, V)) -> perm_2_out_ga2(._22(X, ._22(Y, []_0)), ._22(U, ._22(V, []_0)))
if_sort_2_in_1_ga3(X, Y, perm_2_out_ga2(X, Y)) -> if_sort_2_in_2_ga3(X, Y, sorted_1_in_g1(Y))
sorted_1_in_g1([]_0) -> sorted_1_out_g1([]_0)
sorted_1_in_g1(._22(X, []_0)) -> sorted_1_out_g1(._22(X, []_0))
sorted_1_in_g1(._22(X, ._22(Y, Z))) -> if_sorted_1_in_1_g4(X, Y, Z, le_2_in_gg2(X, Y))
le_2_in_gg2(s_11(X), s_11(Y)) -> if_le_2_in_1_gg3(X, Y, le_2_in_gg2(X, Y))
le_2_in_gg2(0_0, s_11(X)) -> le_2_out_gg2(0_0, s_11(X))
le_2_in_gg2(0_0, 0_0) -> le_2_out_gg2(0_0, 0_0)
if_le_2_in_1_gg3(X, Y, le_2_out_gg2(X, Y)) -> le_2_out_gg2(s_11(X), s_11(Y))
if_sorted_1_in_1_g4(X, Y, Z, le_2_out_gg2(X, Y)) -> if_sorted_1_in_2_g4(X, Y, Z, sorted_1_in_g1(._22(Y, Z)))
if_sorted_1_in_2_g4(X, Y, Z, sorted_1_out_g1(._22(Y, Z))) -> sorted_1_out_g1(._22(X, ._22(Y, Z)))
if_sort_2_in_2_ga3(X, Y, sorted_1_out_g1(Y)) -> sort_2_out_ga2(X, Y)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
↳ PiDP
↳ PiDP
LE_2_IN_GG2(s_11(X), s_11(Y)) -> LE_2_IN_GG2(X, Y)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
↳ PiDP
↳ PiDP
↳ PiDP
LE_2_IN_GG2(s_11(X), s_11(Y)) -> LE_2_IN_GG2(X, Y)
From the DPs we obtained the following set of size-change graphs:
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDP
IF_SORTED_1_IN_1_G4(X, Y, Z, le_2_out_gg2(X, Y)) -> SORTED_1_IN_G1(._22(Y, Z))
SORTED_1_IN_G1(._22(X, ._22(Y, Z))) -> IF_SORTED_1_IN_1_G4(X, Y, Z, le_2_in_gg2(X, Y))
sort_2_in_ga2(X, Y) -> if_sort_2_in_1_ga3(X, Y, perm_2_in_ga2(X, Y))
perm_2_in_ga2([]_0, []_0) -> perm_2_out_ga2([]_0, []_0)
perm_2_in_ga2(._22(X, ._22(Y, []_0)), ._22(U, ._22(V, []_0))) -> if_perm_2_in_1_ga5(X, Y, U, V, delete_3_in_aga3(U, ._22(X, Y), Z))
delete_3_in_aga3(X, ._22(X, Y), Y) -> delete_3_out_aga3(X, ._22(X, Y), Y)
delete_3_in_aga3(X, ._22(Y, Z), W) -> if_delete_3_in_1_aga5(X, Y, Z, W, delete_3_in_aga3(X, Z, W))
if_delete_3_in_1_aga5(X, Y, Z, W, delete_3_out_aga3(X, Z, W)) -> delete_3_out_aga3(X, ._22(Y, Z), W)
if_perm_2_in_1_ga5(X, Y, U, V, delete_3_out_aga3(U, ._22(X, Y), Z)) -> if_perm_2_in_2_ga6(X, Y, U, V, Z, perm_2_in_ga2(Z, V))
if_perm_2_in_2_ga6(X, Y, U, V, Z, perm_2_out_ga2(Z, V)) -> perm_2_out_ga2(._22(X, ._22(Y, []_0)), ._22(U, ._22(V, []_0)))
if_sort_2_in_1_ga3(X, Y, perm_2_out_ga2(X, Y)) -> if_sort_2_in_2_ga3(X, Y, sorted_1_in_g1(Y))
sorted_1_in_g1([]_0) -> sorted_1_out_g1([]_0)
sorted_1_in_g1(._22(X, []_0)) -> sorted_1_out_g1(._22(X, []_0))
sorted_1_in_g1(._22(X, ._22(Y, Z))) -> if_sorted_1_in_1_g4(X, Y, Z, le_2_in_gg2(X, Y))
le_2_in_gg2(s_11(X), s_11(Y)) -> if_le_2_in_1_gg3(X, Y, le_2_in_gg2(X, Y))
le_2_in_gg2(0_0, s_11(X)) -> le_2_out_gg2(0_0, s_11(X))
le_2_in_gg2(0_0, 0_0) -> le_2_out_gg2(0_0, 0_0)
if_le_2_in_1_gg3(X, Y, le_2_out_gg2(X, Y)) -> le_2_out_gg2(s_11(X), s_11(Y))
if_sorted_1_in_1_g4(X, Y, Z, le_2_out_gg2(X, Y)) -> if_sorted_1_in_2_g4(X, Y, Z, sorted_1_in_g1(._22(Y, Z)))
if_sorted_1_in_2_g4(X, Y, Z, sorted_1_out_g1(._22(Y, Z))) -> sorted_1_out_g1(._22(X, ._22(Y, Z)))
if_sort_2_in_2_ga3(X, Y, sorted_1_out_g1(Y)) -> sort_2_out_ga2(X, Y)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
↳ PiDP
IF_SORTED_1_IN_1_G4(X, Y, Z, le_2_out_gg2(X, Y)) -> SORTED_1_IN_G1(._22(Y, Z))
SORTED_1_IN_G1(._22(X, ._22(Y, Z))) -> IF_SORTED_1_IN_1_G4(X, Y, Z, le_2_in_gg2(X, Y))
le_2_in_gg2(s_11(X), s_11(Y)) -> if_le_2_in_1_gg3(X, Y, le_2_in_gg2(X, Y))
le_2_in_gg2(0_0, s_11(X)) -> le_2_out_gg2(0_0, s_11(X))
le_2_in_gg2(0_0, 0_0) -> le_2_out_gg2(0_0, 0_0)
if_le_2_in_1_gg3(X, Y, le_2_out_gg2(X, Y)) -> le_2_out_gg2(s_11(X), s_11(Y))
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPPoloProof
↳ PiDP
↳ PiDP
IF_SORTED_1_IN_1_G3(Y, Z, le_2_out_gg) -> SORTED_1_IN_G1(._22(Y, Z))
SORTED_1_IN_G1(._22(X, ._22(Y, Z))) -> IF_SORTED_1_IN_1_G3(Y, Z, le_2_in_gg2(X, Y))
le_2_in_gg2(s_11(X), s_11(Y)) -> if_le_2_in_1_gg1(le_2_in_gg2(X, Y))
le_2_in_gg2(0_0, s_11(X)) -> le_2_out_gg
le_2_in_gg2(0_0, 0_0) -> le_2_out_gg
if_le_2_in_1_gg1(le_2_out_gg) -> le_2_out_gg
le_2_in_gg2(x0, x1)
if_le_2_in_1_gg1(x0)
The remaining Dependency Pairs were at least non-strictly be oriented.
SORTED_1_IN_G1(._22(X, ._22(Y, Z))) -> IF_SORTED_1_IN_1_G3(Y, Z, le_2_in_gg2(X, Y))
With the implicit AFS there is no usable rule.
IF_SORTED_1_IN_1_G3(Y, Z, le_2_out_gg) -> SORTED_1_IN_G1(._22(Y, Z))
Used ordering: POLO with Polynomial interpretation:
POL(0_0) = 0
POL(SORTED_1_IN_G1(x1)) = x1
POL(._22(x1, x2)) = 1 + x2
POL(le_2_out_gg) = 0
POL(IF_SORTED_1_IN_1_G3(x1, x2, x3)) = 1 + x2
POL(le_2_in_gg2(x1, x2)) = 0
POL(s_11(x1)) = 0
POL(if_le_2_in_1_gg1(x1)) = 0
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPPoloProof
↳ QDP
↳ DependencyGraphProof
↳ PiDP
↳ PiDP
IF_SORTED_1_IN_1_G3(Y, Z, le_2_out_gg) -> SORTED_1_IN_G1(._22(Y, Z))
le_2_in_gg2(s_11(X), s_11(Y)) -> if_le_2_in_1_gg1(le_2_in_gg2(X, Y))
le_2_in_gg2(0_0, s_11(X)) -> le_2_out_gg
le_2_in_gg2(0_0, 0_0) -> le_2_out_gg
if_le_2_in_1_gg1(le_2_out_gg) -> le_2_out_gg
le_2_in_gg2(x0, x1)
if_le_2_in_1_gg1(x0)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
DELETE_3_IN_AGA3(X, ._22(Y, Z), W) -> DELETE_3_IN_AGA3(X, Z, W)
sort_2_in_ga2(X, Y) -> if_sort_2_in_1_ga3(X, Y, perm_2_in_ga2(X, Y))
perm_2_in_ga2([]_0, []_0) -> perm_2_out_ga2([]_0, []_0)
perm_2_in_ga2(._22(X, ._22(Y, []_0)), ._22(U, ._22(V, []_0))) -> if_perm_2_in_1_ga5(X, Y, U, V, delete_3_in_aga3(U, ._22(X, Y), Z))
delete_3_in_aga3(X, ._22(X, Y), Y) -> delete_3_out_aga3(X, ._22(X, Y), Y)
delete_3_in_aga3(X, ._22(Y, Z), W) -> if_delete_3_in_1_aga5(X, Y, Z, W, delete_3_in_aga3(X, Z, W))
if_delete_3_in_1_aga5(X, Y, Z, W, delete_3_out_aga3(X, Z, W)) -> delete_3_out_aga3(X, ._22(Y, Z), W)
if_perm_2_in_1_ga5(X, Y, U, V, delete_3_out_aga3(U, ._22(X, Y), Z)) -> if_perm_2_in_2_ga6(X, Y, U, V, Z, perm_2_in_ga2(Z, V))
if_perm_2_in_2_ga6(X, Y, U, V, Z, perm_2_out_ga2(Z, V)) -> perm_2_out_ga2(._22(X, ._22(Y, []_0)), ._22(U, ._22(V, []_0)))
if_sort_2_in_1_ga3(X, Y, perm_2_out_ga2(X, Y)) -> if_sort_2_in_2_ga3(X, Y, sorted_1_in_g1(Y))
sorted_1_in_g1([]_0) -> sorted_1_out_g1([]_0)
sorted_1_in_g1(._22(X, []_0)) -> sorted_1_out_g1(._22(X, []_0))
sorted_1_in_g1(._22(X, ._22(Y, Z))) -> if_sorted_1_in_1_g4(X, Y, Z, le_2_in_gg2(X, Y))
le_2_in_gg2(s_11(X), s_11(Y)) -> if_le_2_in_1_gg3(X, Y, le_2_in_gg2(X, Y))
le_2_in_gg2(0_0, s_11(X)) -> le_2_out_gg2(0_0, s_11(X))
le_2_in_gg2(0_0, 0_0) -> le_2_out_gg2(0_0, 0_0)
if_le_2_in_1_gg3(X, Y, le_2_out_gg2(X, Y)) -> le_2_out_gg2(s_11(X), s_11(Y))
if_sorted_1_in_1_g4(X, Y, Z, le_2_out_gg2(X, Y)) -> if_sorted_1_in_2_g4(X, Y, Z, sorted_1_in_g1(._22(Y, Z)))
if_sorted_1_in_2_g4(X, Y, Z, sorted_1_out_g1(._22(Y, Z))) -> sorted_1_out_g1(._22(X, ._22(Y, Z)))
if_sort_2_in_2_ga3(X, Y, sorted_1_out_g1(Y)) -> sort_2_out_ga2(X, Y)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
DELETE_3_IN_AGA3(X, ._22(Y, Z), W) -> DELETE_3_IN_AGA3(X, Z, W)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
↳ PiDP
DELETE_3_IN_AGA1(._22(Y, Z)) -> DELETE_3_IN_AGA1(Z)
From the DPs we obtained the following set of size-change graphs:
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
IF_PERM_2_IN_1_GA5(X, Y, U, V, delete_3_out_aga3(U, ._22(X, Y), Z)) -> PERM_2_IN_GA2(Z, V)
PERM_2_IN_GA2(._22(X, ._22(Y, []_0)), ._22(U, ._22(V, []_0))) -> IF_PERM_2_IN_1_GA5(X, Y, U, V, delete_3_in_aga3(U, ._22(X, Y), Z))
sort_2_in_ga2(X, Y) -> if_sort_2_in_1_ga3(X, Y, perm_2_in_ga2(X, Y))
perm_2_in_ga2([]_0, []_0) -> perm_2_out_ga2([]_0, []_0)
perm_2_in_ga2(._22(X, ._22(Y, []_0)), ._22(U, ._22(V, []_0))) -> if_perm_2_in_1_ga5(X, Y, U, V, delete_3_in_aga3(U, ._22(X, Y), Z))
delete_3_in_aga3(X, ._22(X, Y), Y) -> delete_3_out_aga3(X, ._22(X, Y), Y)
delete_3_in_aga3(X, ._22(Y, Z), W) -> if_delete_3_in_1_aga5(X, Y, Z, W, delete_3_in_aga3(X, Z, W))
if_delete_3_in_1_aga5(X, Y, Z, W, delete_3_out_aga3(X, Z, W)) -> delete_3_out_aga3(X, ._22(Y, Z), W)
if_perm_2_in_1_ga5(X, Y, U, V, delete_3_out_aga3(U, ._22(X, Y), Z)) -> if_perm_2_in_2_ga6(X, Y, U, V, Z, perm_2_in_ga2(Z, V))
if_perm_2_in_2_ga6(X, Y, U, V, Z, perm_2_out_ga2(Z, V)) -> perm_2_out_ga2(._22(X, ._22(Y, []_0)), ._22(U, ._22(V, []_0)))
if_sort_2_in_1_ga3(X, Y, perm_2_out_ga2(X, Y)) -> if_sort_2_in_2_ga3(X, Y, sorted_1_in_g1(Y))
sorted_1_in_g1([]_0) -> sorted_1_out_g1([]_0)
sorted_1_in_g1(._22(X, []_0)) -> sorted_1_out_g1(._22(X, []_0))
sorted_1_in_g1(._22(X, ._22(Y, Z))) -> if_sorted_1_in_1_g4(X, Y, Z, le_2_in_gg2(X, Y))
le_2_in_gg2(s_11(X), s_11(Y)) -> if_le_2_in_1_gg3(X, Y, le_2_in_gg2(X, Y))
le_2_in_gg2(0_0, s_11(X)) -> le_2_out_gg2(0_0, s_11(X))
le_2_in_gg2(0_0, 0_0) -> le_2_out_gg2(0_0, 0_0)
if_le_2_in_1_gg3(X, Y, le_2_out_gg2(X, Y)) -> le_2_out_gg2(s_11(X), s_11(Y))
if_sorted_1_in_1_g4(X, Y, Z, le_2_out_gg2(X, Y)) -> if_sorted_1_in_2_g4(X, Y, Z, sorted_1_in_g1(._22(Y, Z)))
if_sorted_1_in_2_g4(X, Y, Z, sorted_1_out_g1(._22(Y, Z))) -> sorted_1_out_g1(._22(X, ._22(Y, Z)))
if_sort_2_in_2_ga3(X, Y, sorted_1_out_g1(Y)) -> sort_2_out_ga2(X, Y)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
IF_PERM_2_IN_1_GA5(X, Y, U, V, delete_3_out_aga3(U, ._22(X, Y), Z)) -> PERM_2_IN_GA2(Z, V)
PERM_2_IN_GA2(._22(X, ._22(Y, []_0)), ._22(U, ._22(V, []_0))) -> IF_PERM_2_IN_1_GA5(X, Y, U, V, delete_3_in_aga3(U, ._22(X, Y), Z))
delete_3_in_aga3(X, ._22(X, Y), Y) -> delete_3_out_aga3(X, ._22(X, Y), Y)
delete_3_in_aga3(X, ._22(Y, Z), W) -> if_delete_3_in_1_aga5(X, Y, Z, W, delete_3_in_aga3(X, Z, W))
if_delete_3_in_1_aga5(X, Y, Z, W, delete_3_out_aga3(X, Z, W)) -> delete_3_out_aga3(X, ._22(Y, Z), W)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPPoloProof
IF_PERM_2_IN_1_GA1(delete_3_out_aga2(U, Z)) -> PERM_2_IN_GA1(Z)
PERM_2_IN_GA1(._22(X, ._22(Y, []_0))) -> IF_PERM_2_IN_1_GA1(delete_3_in_aga1(._22(X, Y)))
delete_3_in_aga1(._22(X, Y)) -> delete_3_out_aga2(X, Y)
delete_3_in_aga1(._22(Y, Z)) -> if_delete_3_in_1_aga1(delete_3_in_aga1(Z))
if_delete_3_in_1_aga1(delete_3_out_aga2(X, W)) -> delete_3_out_aga2(X, W)
delete_3_in_aga1(x0)
if_delete_3_in_1_aga1(x0)
The remaining Dependency Pairs were at least non-strictly be oriented.
PERM_2_IN_GA1(._22(X, ._22(Y, []_0))) -> IF_PERM_2_IN_1_GA1(delete_3_in_aga1(._22(X, Y)))
With the implicit AFS we had to orient the following set of usable rules non-strictly.
IF_PERM_2_IN_1_GA1(delete_3_out_aga2(U, Z)) -> PERM_2_IN_GA1(Z)
Used ordering: POLO with Polynomial interpretation:
if_delete_3_in_1_aga1(delete_3_out_aga2(X, W)) -> delete_3_out_aga2(X, W)
delete_3_in_aga1(._22(Y, Z)) -> if_delete_3_in_1_aga1(delete_3_in_aga1(Z))
delete_3_in_aga1(._22(X, Y)) -> delete_3_out_aga2(X, Y)
POL(._22(x1, x2)) = x1 + x2
POL(IF_PERM_2_IN_1_GA1(x1)) = x1
POL(delete_3_in_aga1(x1)) = x1
POL(if_delete_3_in_1_aga1(x1)) = x1
POL(delete_3_out_aga2(x1, x2)) = x2
POL([]_0) = 1
POL(PERM_2_IN_GA1(x1)) = x1
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPPoloProof
↳ QDP
↳ DependencyGraphProof
IF_PERM_2_IN_1_GA1(delete_3_out_aga2(U, Z)) -> PERM_2_IN_GA1(Z)
delete_3_in_aga1(._22(X, Y)) -> delete_3_out_aga2(X, Y)
delete_3_in_aga1(._22(Y, Z)) -> if_delete_3_in_1_aga1(delete_3_in_aga1(Z))
if_delete_3_in_1_aga1(delete_3_out_aga2(X, W)) -> delete_3_out_aga2(X, W)
delete_3_in_aga1(x0)
if_delete_3_in_1_aga1(x0)