↳ PROLOG
↳ PrologToPiTRSProof
With regard to the inferred argument filtering the predicates were used in the following modes:
perm2: (b,f)
ap13: (f,f,b)
ap23: (b,b,f)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
perm_2_in_ga2(nil_0, nil_0) -> perm_2_out_ga2(nil_0, nil_0)
perm_2_in_ga2(Xs, cons_22(X, Ys)) -> if_perm_2_in_1_ga4(Xs, X, Ys, ap1_3_in_aag3(X1s, cons_22(X, X2s), Xs))
ap1_3_in_aag3(nil_0, X, X) -> ap1_3_out_aag3(nil_0, X, X)
ap1_3_in_aag3(cons_22(H, X), Y, cons_22(H, Z)) -> if_ap1_3_in_1_aag5(H, X, Y, Z, ap1_3_in_aag3(X, Y, Z))
if_ap1_3_in_1_aag5(H, X, Y, Z, ap1_3_out_aag3(X, Y, Z)) -> ap1_3_out_aag3(cons_22(H, X), Y, cons_22(H, Z))
if_perm_2_in_1_ga4(Xs, X, Ys, ap1_3_out_aag3(X1s, cons_22(X, X2s), Xs)) -> if_perm_2_in_2_ga6(Xs, X, Ys, X1s, X2s, ap2_3_in_gga3(X1s, X2s, Zs))
ap2_3_in_gga3(nil_0, X, X) -> ap2_3_out_gga3(nil_0, X, X)
ap2_3_in_gga3(cons_22(H, X), Y, cons_22(H, Z)) -> if_ap2_3_in_1_gga5(H, X, Y, Z, ap2_3_in_gga3(X, Y, Z))
if_ap2_3_in_1_gga5(H, X, Y, Z, ap2_3_out_gga3(X, Y, Z)) -> ap2_3_out_gga3(cons_22(H, X), Y, cons_22(H, Z))
if_perm_2_in_2_ga6(Xs, X, Ys, X1s, X2s, ap2_3_out_gga3(X1s, X2s, Zs)) -> if_perm_2_in_3_ga5(Xs, X, Ys, Zs, perm_2_in_ga2(Zs, Ys))
if_perm_2_in_3_ga5(Xs, X, Ys, Zs, perm_2_out_ga2(Zs, Ys)) -> perm_2_out_ga2(Xs, cons_22(X, Ys))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
perm_2_in_ga2(nil_0, nil_0) -> perm_2_out_ga2(nil_0, nil_0)
perm_2_in_ga2(Xs, cons_22(X, Ys)) -> if_perm_2_in_1_ga4(Xs, X, Ys, ap1_3_in_aag3(X1s, cons_22(X, X2s), Xs))
ap1_3_in_aag3(nil_0, X, X) -> ap1_3_out_aag3(nil_0, X, X)
ap1_3_in_aag3(cons_22(H, X), Y, cons_22(H, Z)) -> if_ap1_3_in_1_aag5(H, X, Y, Z, ap1_3_in_aag3(X, Y, Z))
if_ap1_3_in_1_aag5(H, X, Y, Z, ap1_3_out_aag3(X, Y, Z)) -> ap1_3_out_aag3(cons_22(H, X), Y, cons_22(H, Z))
if_perm_2_in_1_ga4(Xs, X, Ys, ap1_3_out_aag3(X1s, cons_22(X, X2s), Xs)) -> if_perm_2_in_2_ga6(Xs, X, Ys, X1s, X2s, ap2_3_in_gga3(X1s, X2s, Zs))
ap2_3_in_gga3(nil_0, X, X) -> ap2_3_out_gga3(nil_0, X, X)
ap2_3_in_gga3(cons_22(H, X), Y, cons_22(H, Z)) -> if_ap2_3_in_1_gga5(H, X, Y, Z, ap2_3_in_gga3(X, Y, Z))
if_ap2_3_in_1_gga5(H, X, Y, Z, ap2_3_out_gga3(X, Y, Z)) -> ap2_3_out_gga3(cons_22(H, X), Y, cons_22(H, Z))
if_perm_2_in_2_ga6(Xs, X, Ys, X1s, X2s, ap2_3_out_gga3(X1s, X2s, Zs)) -> if_perm_2_in_3_ga5(Xs, X, Ys, Zs, perm_2_in_ga2(Zs, Ys))
if_perm_2_in_3_ga5(Xs, X, Ys, Zs, perm_2_out_ga2(Zs, Ys)) -> perm_2_out_ga2(Xs, cons_22(X, Ys))
PERM_2_IN_GA2(Xs, cons_22(X, Ys)) -> IF_PERM_2_IN_1_GA4(Xs, X, Ys, ap1_3_in_aag3(X1s, cons_22(X, X2s), Xs))
PERM_2_IN_GA2(Xs, cons_22(X, Ys)) -> AP1_3_IN_AAG3(X1s, cons_22(X, X2s), Xs)
AP1_3_IN_AAG3(cons_22(H, X), Y, cons_22(H, Z)) -> IF_AP1_3_IN_1_AAG5(H, X, Y, Z, ap1_3_in_aag3(X, Y, Z))
AP1_3_IN_AAG3(cons_22(H, X), Y, cons_22(H, Z)) -> AP1_3_IN_AAG3(X, Y, Z)
IF_PERM_2_IN_1_GA4(Xs, X, Ys, ap1_3_out_aag3(X1s, cons_22(X, X2s), Xs)) -> IF_PERM_2_IN_2_GA6(Xs, X, Ys, X1s, X2s, ap2_3_in_gga3(X1s, X2s, Zs))
IF_PERM_2_IN_1_GA4(Xs, X, Ys, ap1_3_out_aag3(X1s, cons_22(X, X2s), Xs)) -> AP2_3_IN_GGA3(X1s, X2s, Zs)
AP2_3_IN_GGA3(cons_22(H, X), Y, cons_22(H, Z)) -> IF_AP2_3_IN_1_GGA5(H, X, Y, Z, ap2_3_in_gga3(X, Y, Z))
AP2_3_IN_GGA3(cons_22(H, X), Y, cons_22(H, Z)) -> AP2_3_IN_GGA3(X, Y, Z)
IF_PERM_2_IN_2_GA6(Xs, X, Ys, X1s, X2s, ap2_3_out_gga3(X1s, X2s, Zs)) -> IF_PERM_2_IN_3_GA5(Xs, X, Ys, Zs, perm_2_in_ga2(Zs, Ys))
IF_PERM_2_IN_2_GA6(Xs, X, Ys, X1s, X2s, ap2_3_out_gga3(X1s, X2s, Zs)) -> PERM_2_IN_GA2(Zs, Ys)
perm_2_in_ga2(nil_0, nil_0) -> perm_2_out_ga2(nil_0, nil_0)
perm_2_in_ga2(Xs, cons_22(X, Ys)) -> if_perm_2_in_1_ga4(Xs, X, Ys, ap1_3_in_aag3(X1s, cons_22(X, X2s), Xs))
ap1_3_in_aag3(nil_0, X, X) -> ap1_3_out_aag3(nil_0, X, X)
ap1_3_in_aag3(cons_22(H, X), Y, cons_22(H, Z)) -> if_ap1_3_in_1_aag5(H, X, Y, Z, ap1_3_in_aag3(X, Y, Z))
if_ap1_3_in_1_aag5(H, X, Y, Z, ap1_3_out_aag3(X, Y, Z)) -> ap1_3_out_aag3(cons_22(H, X), Y, cons_22(H, Z))
if_perm_2_in_1_ga4(Xs, X, Ys, ap1_3_out_aag3(X1s, cons_22(X, X2s), Xs)) -> if_perm_2_in_2_ga6(Xs, X, Ys, X1s, X2s, ap2_3_in_gga3(X1s, X2s, Zs))
ap2_3_in_gga3(nil_0, X, X) -> ap2_3_out_gga3(nil_0, X, X)
ap2_3_in_gga3(cons_22(H, X), Y, cons_22(H, Z)) -> if_ap2_3_in_1_gga5(H, X, Y, Z, ap2_3_in_gga3(X, Y, Z))
if_ap2_3_in_1_gga5(H, X, Y, Z, ap2_3_out_gga3(X, Y, Z)) -> ap2_3_out_gga3(cons_22(H, X), Y, cons_22(H, Z))
if_perm_2_in_2_ga6(Xs, X, Ys, X1s, X2s, ap2_3_out_gga3(X1s, X2s, Zs)) -> if_perm_2_in_3_ga5(Xs, X, Ys, Zs, perm_2_in_ga2(Zs, Ys))
if_perm_2_in_3_ga5(Xs, X, Ys, Zs, perm_2_out_ga2(Zs, Ys)) -> perm_2_out_ga2(Xs, cons_22(X, Ys))
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
PERM_2_IN_GA2(Xs, cons_22(X, Ys)) -> IF_PERM_2_IN_1_GA4(Xs, X, Ys, ap1_3_in_aag3(X1s, cons_22(X, X2s), Xs))
PERM_2_IN_GA2(Xs, cons_22(X, Ys)) -> AP1_3_IN_AAG3(X1s, cons_22(X, X2s), Xs)
AP1_3_IN_AAG3(cons_22(H, X), Y, cons_22(H, Z)) -> IF_AP1_3_IN_1_AAG5(H, X, Y, Z, ap1_3_in_aag3(X, Y, Z))
AP1_3_IN_AAG3(cons_22(H, X), Y, cons_22(H, Z)) -> AP1_3_IN_AAG3(X, Y, Z)
IF_PERM_2_IN_1_GA4(Xs, X, Ys, ap1_3_out_aag3(X1s, cons_22(X, X2s), Xs)) -> IF_PERM_2_IN_2_GA6(Xs, X, Ys, X1s, X2s, ap2_3_in_gga3(X1s, X2s, Zs))
IF_PERM_2_IN_1_GA4(Xs, X, Ys, ap1_3_out_aag3(X1s, cons_22(X, X2s), Xs)) -> AP2_3_IN_GGA3(X1s, X2s, Zs)
AP2_3_IN_GGA3(cons_22(H, X), Y, cons_22(H, Z)) -> IF_AP2_3_IN_1_GGA5(H, X, Y, Z, ap2_3_in_gga3(X, Y, Z))
AP2_3_IN_GGA3(cons_22(H, X), Y, cons_22(H, Z)) -> AP2_3_IN_GGA3(X, Y, Z)
IF_PERM_2_IN_2_GA6(Xs, X, Ys, X1s, X2s, ap2_3_out_gga3(X1s, X2s, Zs)) -> IF_PERM_2_IN_3_GA5(Xs, X, Ys, Zs, perm_2_in_ga2(Zs, Ys))
IF_PERM_2_IN_2_GA6(Xs, X, Ys, X1s, X2s, ap2_3_out_gga3(X1s, X2s, Zs)) -> PERM_2_IN_GA2(Zs, Ys)
perm_2_in_ga2(nil_0, nil_0) -> perm_2_out_ga2(nil_0, nil_0)
perm_2_in_ga2(Xs, cons_22(X, Ys)) -> if_perm_2_in_1_ga4(Xs, X, Ys, ap1_3_in_aag3(X1s, cons_22(X, X2s), Xs))
ap1_3_in_aag3(nil_0, X, X) -> ap1_3_out_aag3(nil_0, X, X)
ap1_3_in_aag3(cons_22(H, X), Y, cons_22(H, Z)) -> if_ap1_3_in_1_aag5(H, X, Y, Z, ap1_3_in_aag3(X, Y, Z))
if_ap1_3_in_1_aag5(H, X, Y, Z, ap1_3_out_aag3(X, Y, Z)) -> ap1_3_out_aag3(cons_22(H, X), Y, cons_22(H, Z))
if_perm_2_in_1_ga4(Xs, X, Ys, ap1_3_out_aag3(X1s, cons_22(X, X2s), Xs)) -> if_perm_2_in_2_ga6(Xs, X, Ys, X1s, X2s, ap2_3_in_gga3(X1s, X2s, Zs))
ap2_3_in_gga3(nil_0, X, X) -> ap2_3_out_gga3(nil_0, X, X)
ap2_3_in_gga3(cons_22(H, X), Y, cons_22(H, Z)) -> if_ap2_3_in_1_gga5(H, X, Y, Z, ap2_3_in_gga3(X, Y, Z))
if_ap2_3_in_1_gga5(H, X, Y, Z, ap2_3_out_gga3(X, Y, Z)) -> ap2_3_out_gga3(cons_22(H, X), Y, cons_22(H, Z))
if_perm_2_in_2_ga6(Xs, X, Ys, X1s, X2s, ap2_3_out_gga3(X1s, X2s, Zs)) -> if_perm_2_in_3_ga5(Xs, X, Ys, Zs, perm_2_in_ga2(Zs, Ys))
if_perm_2_in_3_ga5(Xs, X, Ys, Zs, perm_2_out_ga2(Zs, Ys)) -> perm_2_out_ga2(Xs, cons_22(X, Ys))
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDP
AP2_3_IN_GGA3(cons_22(H, X), Y, cons_22(H, Z)) -> AP2_3_IN_GGA3(X, Y, Z)
perm_2_in_ga2(nil_0, nil_0) -> perm_2_out_ga2(nil_0, nil_0)
perm_2_in_ga2(Xs, cons_22(X, Ys)) -> if_perm_2_in_1_ga4(Xs, X, Ys, ap1_3_in_aag3(X1s, cons_22(X, X2s), Xs))
ap1_3_in_aag3(nil_0, X, X) -> ap1_3_out_aag3(nil_0, X, X)
ap1_3_in_aag3(cons_22(H, X), Y, cons_22(H, Z)) -> if_ap1_3_in_1_aag5(H, X, Y, Z, ap1_3_in_aag3(X, Y, Z))
if_ap1_3_in_1_aag5(H, X, Y, Z, ap1_3_out_aag3(X, Y, Z)) -> ap1_3_out_aag3(cons_22(H, X), Y, cons_22(H, Z))
if_perm_2_in_1_ga4(Xs, X, Ys, ap1_3_out_aag3(X1s, cons_22(X, X2s), Xs)) -> if_perm_2_in_2_ga6(Xs, X, Ys, X1s, X2s, ap2_3_in_gga3(X1s, X2s, Zs))
ap2_3_in_gga3(nil_0, X, X) -> ap2_3_out_gga3(nil_0, X, X)
ap2_3_in_gga3(cons_22(H, X), Y, cons_22(H, Z)) -> if_ap2_3_in_1_gga5(H, X, Y, Z, ap2_3_in_gga3(X, Y, Z))
if_ap2_3_in_1_gga5(H, X, Y, Z, ap2_3_out_gga3(X, Y, Z)) -> ap2_3_out_gga3(cons_22(H, X), Y, cons_22(H, Z))
if_perm_2_in_2_ga6(Xs, X, Ys, X1s, X2s, ap2_3_out_gga3(X1s, X2s, Zs)) -> if_perm_2_in_3_ga5(Xs, X, Ys, Zs, perm_2_in_ga2(Zs, Ys))
if_perm_2_in_3_ga5(Xs, X, Ys, Zs, perm_2_out_ga2(Zs, Ys)) -> perm_2_out_ga2(Xs, cons_22(X, Ys))
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
↳ PiDP
AP2_3_IN_GGA3(cons_22(H, X), Y, cons_22(H, Z)) -> AP2_3_IN_GGA3(X, Y, Z)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
↳ PiDP
↳ PiDP
AP2_3_IN_GGA2(cons_22(H, X), Y) -> AP2_3_IN_GGA2(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
AP1_3_IN_AAG3(cons_22(H, X), Y, cons_22(H, Z)) -> AP1_3_IN_AAG3(X, Y, Z)
perm_2_in_ga2(nil_0, nil_0) -> perm_2_out_ga2(nil_0, nil_0)
perm_2_in_ga2(Xs, cons_22(X, Ys)) -> if_perm_2_in_1_ga4(Xs, X, Ys, ap1_3_in_aag3(X1s, cons_22(X, X2s), Xs))
ap1_3_in_aag3(nil_0, X, X) -> ap1_3_out_aag3(nil_0, X, X)
ap1_3_in_aag3(cons_22(H, X), Y, cons_22(H, Z)) -> if_ap1_3_in_1_aag5(H, X, Y, Z, ap1_3_in_aag3(X, Y, Z))
if_ap1_3_in_1_aag5(H, X, Y, Z, ap1_3_out_aag3(X, Y, Z)) -> ap1_3_out_aag3(cons_22(H, X), Y, cons_22(H, Z))
if_perm_2_in_1_ga4(Xs, X, Ys, ap1_3_out_aag3(X1s, cons_22(X, X2s), Xs)) -> if_perm_2_in_2_ga6(Xs, X, Ys, X1s, X2s, ap2_3_in_gga3(X1s, X2s, Zs))
ap2_3_in_gga3(nil_0, X, X) -> ap2_3_out_gga3(nil_0, X, X)
ap2_3_in_gga3(cons_22(H, X), Y, cons_22(H, Z)) -> if_ap2_3_in_1_gga5(H, X, Y, Z, ap2_3_in_gga3(X, Y, Z))
if_ap2_3_in_1_gga5(H, X, Y, Z, ap2_3_out_gga3(X, Y, Z)) -> ap2_3_out_gga3(cons_22(H, X), Y, cons_22(H, Z))
if_perm_2_in_2_ga6(Xs, X, Ys, X1s, X2s, ap2_3_out_gga3(X1s, X2s, Zs)) -> if_perm_2_in_3_ga5(Xs, X, Ys, Zs, perm_2_in_ga2(Zs, Ys))
if_perm_2_in_3_ga5(Xs, X, Ys, Zs, perm_2_out_ga2(Zs, Ys)) -> perm_2_out_ga2(Xs, cons_22(X, Ys))
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
AP1_3_IN_AAG3(cons_22(H, X), Y, cons_22(H, Z)) -> AP1_3_IN_AAG3(X, Y, Z)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
↳ PiDP
AP1_3_IN_AAG1(cons_22(H, Z)) -> AP1_3_IN_AAG1(Z)
From the DPs we obtained the following set of size-change graphs:
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
IF_PERM_2_IN_1_GA4(Xs, X, Ys, ap1_3_out_aag3(X1s, cons_22(X, X2s), Xs)) -> IF_PERM_2_IN_2_GA6(Xs, X, Ys, X1s, X2s, ap2_3_in_gga3(X1s, X2s, Zs))
PERM_2_IN_GA2(Xs, cons_22(X, Ys)) -> IF_PERM_2_IN_1_GA4(Xs, X, Ys, ap1_3_in_aag3(X1s, cons_22(X, X2s), Xs))
IF_PERM_2_IN_2_GA6(Xs, X, Ys, X1s, X2s, ap2_3_out_gga3(X1s, X2s, Zs)) -> PERM_2_IN_GA2(Zs, Ys)
perm_2_in_ga2(nil_0, nil_0) -> perm_2_out_ga2(nil_0, nil_0)
perm_2_in_ga2(Xs, cons_22(X, Ys)) -> if_perm_2_in_1_ga4(Xs, X, Ys, ap1_3_in_aag3(X1s, cons_22(X, X2s), Xs))
ap1_3_in_aag3(nil_0, X, X) -> ap1_3_out_aag3(nil_0, X, X)
ap1_3_in_aag3(cons_22(H, X), Y, cons_22(H, Z)) -> if_ap1_3_in_1_aag5(H, X, Y, Z, ap1_3_in_aag3(X, Y, Z))
if_ap1_3_in_1_aag5(H, X, Y, Z, ap1_3_out_aag3(X, Y, Z)) -> ap1_3_out_aag3(cons_22(H, X), Y, cons_22(H, Z))
if_perm_2_in_1_ga4(Xs, X, Ys, ap1_3_out_aag3(X1s, cons_22(X, X2s), Xs)) -> if_perm_2_in_2_ga6(Xs, X, Ys, X1s, X2s, ap2_3_in_gga3(X1s, X2s, Zs))
ap2_3_in_gga3(nil_0, X, X) -> ap2_3_out_gga3(nil_0, X, X)
ap2_3_in_gga3(cons_22(H, X), Y, cons_22(H, Z)) -> if_ap2_3_in_1_gga5(H, X, Y, Z, ap2_3_in_gga3(X, Y, Z))
if_ap2_3_in_1_gga5(H, X, Y, Z, ap2_3_out_gga3(X, Y, Z)) -> ap2_3_out_gga3(cons_22(H, X), Y, cons_22(H, Z))
if_perm_2_in_2_ga6(Xs, X, Ys, X1s, X2s, ap2_3_out_gga3(X1s, X2s, Zs)) -> if_perm_2_in_3_ga5(Xs, X, Ys, Zs, perm_2_in_ga2(Zs, Ys))
if_perm_2_in_3_ga5(Xs, X, Ys, Zs, perm_2_out_ga2(Zs, Ys)) -> perm_2_out_ga2(Xs, cons_22(X, Ys))
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
IF_PERM_2_IN_1_GA4(Xs, X, Ys, ap1_3_out_aag3(X1s, cons_22(X, X2s), Xs)) -> IF_PERM_2_IN_2_GA6(Xs, X, Ys, X1s, X2s, ap2_3_in_gga3(X1s, X2s, Zs))
PERM_2_IN_GA2(Xs, cons_22(X, Ys)) -> IF_PERM_2_IN_1_GA4(Xs, X, Ys, ap1_3_in_aag3(X1s, cons_22(X, X2s), Xs))
IF_PERM_2_IN_2_GA6(Xs, X, Ys, X1s, X2s, ap2_3_out_gga3(X1s, X2s, Zs)) -> PERM_2_IN_GA2(Zs, Ys)
ap2_3_in_gga3(nil_0, X, X) -> ap2_3_out_gga3(nil_0, X, X)
ap2_3_in_gga3(cons_22(H, X), Y, cons_22(H, Z)) -> if_ap2_3_in_1_gga5(H, X, Y, Z, ap2_3_in_gga3(X, Y, Z))
ap1_3_in_aag3(nil_0, X, X) -> ap1_3_out_aag3(nil_0, X, X)
ap1_3_in_aag3(cons_22(H, X), Y, cons_22(H, Z)) -> if_ap1_3_in_1_aag5(H, X, Y, Z, ap1_3_in_aag3(X, Y, Z))
if_ap2_3_in_1_gga5(H, X, Y, Z, ap2_3_out_gga3(X, Y, Z)) -> ap2_3_out_gga3(cons_22(H, X), Y, cons_22(H, Z))
if_ap1_3_in_1_aag5(H, X, Y, Z, ap1_3_out_aag3(X, Y, Z)) -> ap1_3_out_aag3(cons_22(H, X), Y, cons_22(H, Z))
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ RuleRemovalProof
IF_PERM_2_IN_1_GA1(ap1_3_out_aag2(X1s, cons_22(X, X2s))) -> IF_PERM_2_IN_2_GA2(X, ap2_3_in_gga2(X1s, X2s))
PERM_2_IN_GA1(Xs) -> IF_PERM_2_IN_1_GA1(ap1_3_in_aag1(Xs))
IF_PERM_2_IN_2_GA2(X, ap2_3_out_gga1(Zs)) -> PERM_2_IN_GA1(Zs)
ap2_3_in_gga2(nil_0, X) -> ap2_3_out_gga1(X)
ap2_3_in_gga2(cons_22(H, X), Y) -> if_ap2_3_in_1_gga2(H, ap2_3_in_gga2(X, Y))
ap1_3_in_aag1(X) -> ap1_3_out_aag2(nil_0, X)
ap1_3_in_aag1(cons_22(H, Z)) -> if_ap1_3_in_1_aag2(H, ap1_3_in_aag1(Z))
if_ap2_3_in_1_gga2(H, ap2_3_out_gga1(Z)) -> ap2_3_out_gga1(cons_22(H, Z))
if_ap1_3_in_1_aag2(H, ap1_3_out_aag2(X, Y)) -> ap1_3_out_aag2(cons_22(H, X), Y)
ap2_3_in_gga2(x0, x1)
ap1_3_in_aag1(x0)
if_ap2_3_in_1_gga2(x0, x1)
if_ap1_3_in_1_aag2(x0, x1)
ap2_3_in_gga2(nil_0, X) -> ap2_3_out_gga1(X)
POL(nil_0) = 2
POL(ap2_3_out_gga1(x1)) = 1 + x1
POL(if_ap1_3_in_1_aag2(x1, x2)) = 1 + x1 + x2
POL(IF_PERM_2_IN_2_GA2(x1, x2)) = 1 + x1 + x2
POL(ap2_3_in_gga2(x1, x2)) = x1 + x2
POL(IF_PERM_2_IN_1_GA1(x1)) = x1
POL(ap1_3_in_aag1(x1)) = 2 + x1
POL(if_ap2_3_in_1_gga2(x1, x2)) = 1 + x1 + x2
POL(cons_22(x1, x2)) = 1 + x1 + x2
POL(ap1_3_out_aag2(x1, x2)) = x1 + x2
POL(PERM_2_IN_GA1(x1)) = 2 + x1
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ QDPPoloProof
IF_PERM_2_IN_1_GA1(ap1_3_out_aag2(X1s, cons_22(X, X2s))) -> IF_PERM_2_IN_2_GA2(X, ap2_3_in_gga2(X1s, X2s))
PERM_2_IN_GA1(Xs) -> IF_PERM_2_IN_1_GA1(ap1_3_in_aag1(Xs))
IF_PERM_2_IN_2_GA2(X, ap2_3_out_gga1(Zs)) -> PERM_2_IN_GA1(Zs)
ap2_3_in_gga2(cons_22(H, X), Y) -> if_ap2_3_in_1_gga2(H, ap2_3_in_gga2(X, Y))
ap1_3_in_aag1(X) -> ap1_3_out_aag2(nil_0, X)
ap1_3_in_aag1(cons_22(H, Z)) -> if_ap1_3_in_1_aag2(H, ap1_3_in_aag1(Z))
if_ap2_3_in_1_gga2(H, ap2_3_out_gga1(Z)) -> ap2_3_out_gga1(cons_22(H, Z))
if_ap1_3_in_1_aag2(H, ap1_3_out_aag2(X, Y)) -> ap1_3_out_aag2(cons_22(H, X), Y)
ap2_3_in_gga2(x0, x1)
ap1_3_in_aag1(x0)
if_ap2_3_in_1_gga2(x0, x1)
if_ap1_3_in_1_aag2(x0, x1)
The remaining Dependency Pairs were at least non-strictly be oriented.
IF_PERM_2_IN_2_GA2(X, ap2_3_out_gga1(Zs)) -> PERM_2_IN_GA1(Zs)
With the implicit AFS we had to orient the following set of usable rules non-strictly.
IF_PERM_2_IN_1_GA1(ap1_3_out_aag2(X1s, cons_22(X, X2s))) -> IF_PERM_2_IN_2_GA2(X, ap2_3_in_gga2(X1s, X2s))
PERM_2_IN_GA1(Xs) -> IF_PERM_2_IN_1_GA1(ap1_3_in_aag1(Xs))
Used ordering: POLO with Polynomial interpretation:
if_ap2_3_in_1_gga2(H, ap2_3_out_gga1(Z)) -> ap2_3_out_gga1(cons_22(H, Z))
ap2_3_in_gga2(cons_22(H, X), Y) -> if_ap2_3_in_1_gga2(H, ap2_3_in_gga2(X, Y))
POL(nil_0) = 0
POL(ap2_3_out_gga1(x1)) = 1
POL(if_ap1_3_in_1_aag2(x1, x2)) = 0
POL(IF_PERM_2_IN_2_GA2(x1, x2)) = x2
POL(ap2_3_in_gga2(x1, x2)) = 0
POL(IF_PERM_2_IN_1_GA1(x1)) = 0
POL(ap1_3_in_aag1(x1)) = 0
POL(if_ap2_3_in_1_gga2(x1, x2)) = x2
POL(cons_22(x1, x2)) = 0
POL(ap1_3_out_aag2(x1, x2)) = 0
POL(PERM_2_IN_GA1(x1)) = 0
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ QDPPoloProof
↳ QDP
↳ DependencyGraphProof
IF_PERM_2_IN_1_GA1(ap1_3_out_aag2(X1s, cons_22(X, X2s))) -> IF_PERM_2_IN_2_GA2(X, ap2_3_in_gga2(X1s, X2s))
PERM_2_IN_GA1(Xs) -> IF_PERM_2_IN_1_GA1(ap1_3_in_aag1(Xs))
ap2_3_in_gga2(cons_22(H, X), Y) -> if_ap2_3_in_1_gga2(H, ap2_3_in_gga2(X, Y))
ap1_3_in_aag1(X) -> ap1_3_out_aag2(nil_0, X)
ap1_3_in_aag1(cons_22(H, Z)) -> if_ap1_3_in_1_aag2(H, ap1_3_in_aag1(Z))
if_ap2_3_in_1_gga2(H, ap2_3_out_gga1(Z)) -> ap2_3_out_gga1(cons_22(H, Z))
if_ap1_3_in_1_aag2(H, ap1_3_out_aag2(X, Y)) -> ap1_3_out_aag2(cons_22(H, X), Y)
ap2_3_in_gga2(x0, x1)
ap1_3_in_aag1(x0)
if_ap2_3_in_1_gga2(x0, x1)
if_ap1_3_in_1_aag2(x0, x1)