↳ PROLOG
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
With regard to the inferred argument filtering the predicates were used in the following modes:
rem3: (b,b,f)
sub3: (b,b,f)
geq2: (b,b)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
rem_3_in_gga3(X, Y, R) -> if_rem_3_in_1_gga4(X, Y, R, notZero_1_in_g1(Y))
notZero_1_in_g1(s_11(X)) -> notZero_1_out_g1(s_11(X))
if_rem_3_in_1_gga4(X, Y, R, notZero_1_out_g1(Y)) -> if_rem_3_in_2_gga4(X, Y, R, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_gga4(X, Y, Z, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_gga3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
if_rem_3_in_2_gga4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> if_rem_3_in_3_gga5(X, Y, R, Z, rem_3_in_gga3(Z, Y, R))
rem_3_in_gga3(X, Y, X) -> if_rem_3_in_4_gga3(X, Y, notZero_1_in_g1(Y))
if_rem_3_in_4_gga3(X, Y, notZero_1_out_g1(Y)) -> if_rem_3_in_5_gga3(X, Y, geq_2_in_gg2(X, Y))
geq_2_in_gg2(s_11(X), s_11(Y)) -> if_geq_2_in_1_gg3(X, Y, geq_2_in_gg2(X, Y))
geq_2_in_gg2(X, 0_0) -> geq_2_out_gg2(X, 0_0)
if_geq_2_in_1_gg3(X, Y, geq_2_out_gg2(X, Y)) -> geq_2_out_gg2(s_11(X), s_11(Y))
if_rem_3_in_5_gga3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_gga3(X, Y, X)
if_rem_3_in_3_gga5(X, Y, R, Z, rem_3_out_gga3(Z, Y, R)) -> rem_3_out_gga3(X, Y, R)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PrologToPiTRSProof
rem_3_in_gga3(X, Y, R) -> if_rem_3_in_1_gga4(X, Y, R, notZero_1_in_g1(Y))
notZero_1_in_g1(s_11(X)) -> notZero_1_out_g1(s_11(X))
if_rem_3_in_1_gga4(X, Y, R, notZero_1_out_g1(Y)) -> if_rem_3_in_2_gga4(X, Y, R, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_gga4(X, Y, Z, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_gga3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
if_rem_3_in_2_gga4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> if_rem_3_in_3_gga5(X, Y, R, Z, rem_3_in_gga3(Z, Y, R))
rem_3_in_gga3(X, Y, X) -> if_rem_3_in_4_gga3(X, Y, notZero_1_in_g1(Y))
if_rem_3_in_4_gga3(X, Y, notZero_1_out_g1(Y)) -> if_rem_3_in_5_gga3(X, Y, geq_2_in_gg2(X, Y))
geq_2_in_gg2(s_11(X), s_11(Y)) -> if_geq_2_in_1_gg3(X, Y, geq_2_in_gg2(X, Y))
geq_2_in_gg2(X, 0_0) -> geq_2_out_gg2(X, 0_0)
if_geq_2_in_1_gg3(X, Y, geq_2_out_gg2(X, Y)) -> geq_2_out_gg2(s_11(X), s_11(Y))
if_rem_3_in_5_gga3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_gga3(X, Y, X)
if_rem_3_in_3_gga5(X, Y, R, Z, rem_3_out_gga3(Z, Y, R)) -> rem_3_out_gga3(X, Y, R)
REM_3_IN_GGA3(X, Y, R) -> IF_REM_3_IN_1_GGA4(X, Y, R, notZero_1_in_g1(Y))
REM_3_IN_GGA3(X, Y, R) -> NOTZERO_1_IN_G1(Y)
IF_REM_3_IN_1_GGA4(X, Y, R, notZero_1_out_g1(Y)) -> IF_REM_3_IN_2_GGA4(X, Y, R, sub_3_in_gga3(X, Y, Z))
IF_REM_3_IN_1_GGA4(X, Y, R, notZero_1_out_g1(Y)) -> SUB_3_IN_GGA3(X, Y, Z)
SUB_3_IN_GGA3(s_11(X), s_11(Y), Z) -> IF_SUB_3_IN_1_GGA4(X, Y, Z, sub_3_in_gga3(X, Y, Z))
SUB_3_IN_GGA3(s_11(X), s_11(Y), Z) -> SUB_3_IN_GGA3(X, Y, Z)
IF_REM_3_IN_2_GGA4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> IF_REM_3_IN_3_GGA5(X, Y, R, Z, rem_3_in_gga3(Z, Y, R))
IF_REM_3_IN_2_GGA4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> REM_3_IN_GGA3(Z, Y, R)
REM_3_IN_GGA3(X, Y, X) -> IF_REM_3_IN_4_GGA3(X, Y, notZero_1_in_g1(Y))
REM_3_IN_GGA3(X, Y, X) -> NOTZERO_1_IN_G1(Y)
IF_REM_3_IN_4_GGA3(X, Y, notZero_1_out_g1(Y)) -> IF_REM_3_IN_5_GGA3(X, Y, geq_2_in_gg2(X, Y))
IF_REM_3_IN_4_GGA3(X, Y, notZero_1_out_g1(Y)) -> GEQ_2_IN_GG2(X, Y)
GEQ_2_IN_GG2(s_11(X), s_11(Y)) -> IF_GEQ_2_IN_1_GG3(X, Y, geq_2_in_gg2(X, Y))
GEQ_2_IN_GG2(s_11(X), s_11(Y)) -> GEQ_2_IN_GG2(X, Y)
rem_3_in_gga3(X, Y, R) -> if_rem_3_in_1_gga4(X, Y, R, notZero_1_in_g1(Y))
notZero_1_in_g1(s_11(X)) -> notZero_1_out_g1(s_11(X))
if_rem_3_in_1_gga4(X, Y, R, notZero_1_out_g1(Y)) -> if_rem_3_in_2_gga4(X, Y, R, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_gga4(X, Y, Z, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_gga3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
if_rem_3_in_2_gga4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> if_rem_3_in_3_gga5(X, Y, R, Z, rem_3_in_gga3(Z, Y, R))
rem_3_in_gga3(X, Y, X) -> if_rem_3_in_4_gga3(X, Y, notZero_1_in_g1(Y))
if_rem_3_in_4_gga3(X, Y, notZero_1_out_g1(Y)) -> if_rem_3_in_5_gga3(X, Y, geq_2_in_gg2(X, Y))
geq_2_in_gg2(s_11(X), s_11(Y)) -> if_geq_2_in_1_gg3(X, Y, geq_2_in_gg2(X, Y))
geq_2_in_gg2(X, 0_0) -> geq_2_out_gg2(X, 0_0)
if_geq_2_in_1_gg3(X, Y, geq_2_out_gg2(X, Y)) -> geq_2_out_gg2(s_11(X), s_11(Y))
if_rem_3_in_5_gga3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_gga3(X, Y, X)
if_rem_3_in_3_gga5(X, Y, R, Z, rem_3_out_gga3(Z, Y, R)) -> rem_3_out_gga3(X, Y, R)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PrologToPiTRSProof
REM_3_IN_GGA3(X, Y, R) -> IF_REM_3_IN_1_GGA4(X, Y, R, notZero_1_in_g1(Y))
REM_3_IN_GGA3(X, Y, R) -> NOTZERO_1_IN_G1(Y)
IF_REM_3_IN_1_GGA4(X, Y, R, notZero_1_out_g1(Y)) -> IF_REM_3_IN_2_GGA4(X, Y, R, sub_3_in_gga3(X, Y, Z))
IF_REM_3_IN_1_GGA4(X, Y, R, notZero_1_out_g1(Y)) -> SUB_3_IN_GGA3(X, Y, Z)
SUB_3_IN_GGA3(s_11(X), s_11(Y), Z) -> IF_SUB_3_IN_1_GGA4(X, Y, Z, sub_3_in_gga3(X, Y, Z))
SUB_3_IN_GGA3(s_11(X), s_11(Y), Z) -> SUB_3_IN_GGA3(X, Y, Z)
IF_REM_3_IN_2_GGA4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> IF_REM_3_IN_3_GGA5(X, Y, R, Z, rem_3_in_gga3(Z, Y, R))
IF_REM_3_IN_2_GGA4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> REM_3_IN_GGA3(Z, Y, R)
REM_3_IN_GGA3(X, Y, X) -> IF_REM_3_IN_4_GGA3(X, Y, notZero_1_in_g1(Y))
REM_3_IN_GGA3(X, Y, X) -> NOTZERO_1_IN_G1(Y)
IF_REM_3_IN_4_GGA3(X, Y, notZero_1_out_g1(Y)) -> IF_REM_3_IN_5_GGA3(X, Y, geq_2_in_gg2(X, Y))
IF_REM_3_IN_4_GGA3(X, Y, notZero_1_out_g1(Y)) -> GEQ_2_IN_GG2(X, Y)
GEQ_2_IN_GG2(s_11(X), s_11(Y)) -> IF_GEQ_2_IN_1_GG3(X, Y, geq_2_in_gg2(X, Y))
GEQ_2_IN_GG2(s_11(X), s_11(Y)) -> GEQ_2_IN_GG2(X, Y)
rem_3_in_gga3(X, Y, R) -> if_rem_3_in_1_gga4(X, Y, R, notZero_1_in_g1(Y))
notZero_1_in_g1(s_11(X)) -> notZero_1_out_g1(s_11(X))
if_rem_3_in_1_gga4(X, Y, R, notZero_1_out_g1(Y)) -> if_rem_3_in_2_gga4(X, Y, R, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_gga4(X, Y, Z, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_gga3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
if_rem_3_in_2_gga4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> if_rem_3_in_3_gga5(X, Y, R, Z, rem_3_in_gga3(Z, Y, R))
rem_3_in_gga3(X, Y, X) -> if_rem_3_in_4_gga3(X, Y, notZero_1_in_g1(Y))
if_rem_3_in_4_gga3(X, Y, notZero_1_out_g1(Y)) -> if_rem_3_in_5_gga3(X, Y, geq_2_in_gg2(X, Y))
geq_2_in_gg2(s_11(X), s_11(Y)) -> if_geq_2_in_1_gg3(X, Y, geq_2_in_gg2(X, Y))
geq_2_in_gg2(X, 0_0) -> geq_2_out_gg2(X, 0_0)
if_geq_2_in_1_gg3(X, Y, geq_2_out_gg2(X, Y)) -> geq_2_out_gg2(s_11(X), s_11(Y))
if_rem_3_in_5_gga3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_gga3(X, Y, X)
if_rem_3_in_3_gga5(X, Y, R, Z, rem_3_out_gga3(Z, Y, R)) -> rem_3_out_gga3(X, Y, R)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDP
↳ PrologToPiTRSProof
GEQ_2_IN_GG2(s_11(X), s_11(Y)) -> GEQ_2_IN_GG2(X, Y)
rem_3_in_gga3(X, Y, R) -> if_rem_3_in_1_gga4(X, Y, R, notZero_1_in_g1(Y))
notZero_1_in_g1(s_11(X)) -> notZero_1_out_g1(s_11(X))
if_rem_3_in_1_gga4(X, Y, R, notZero_1_out_g1(Y)) -> if_rem_3_in_2_gga4(X, Y, R, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_gga4(X, Y, Z, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_gga3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
if_rem_3_in_2_gga4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> if_rem_3_in_3_gga5(X, Y, R, Z, rem_3_in_gga3(Z, Y, R))
rem_3_in_gga3(X, Y, X) -> if_rem_3_in_4_gga3(X, Y, notZero_1_in_g1(Y))
if_rem_3_in_4_gga3(X, Y, notZero_1_out_g1(Y)) -> if_rem_3_in_5_gga3(X, Y, geq_2_in_gg2(X, Y))
geq_2_in_gg2(s_11(X), s_11(Y)) -> if_geq_2_in_1_gg3(X, Y, geq_2_in_gg2(X, Y))
geq_2_in_gg2(X, 0_0) -> geq_2_out_gg2(X, 0_0)
if_geq_2_in_1_gg3(X, Y, geq_2_out_gg2(X, Y)) -> geq_2_out_gg2(s_11(X), s_11(Y))
if_rem_3_in_5_gga3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_gga3(X, Y, X)
if_rem_3_in_3_gga5(X, Y, R, Z, rem_3_out_gga3(Z, Y, R)) -> rem_3_out_gga3(X, Y, R)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
↳ PiDP
↳ PrologToPiTRSProof
GEQ_2_IN_GG2(s_11(X), s_11(Y)) -> GEQ_2_IN_GG2(X, Y)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
↳ PiDP
↳ PiDP
↳ PrologToPiTRSProof
GEQ_2_IN_GG2(s_11(X), s_11(Y)) -> GEQ_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
↳ PrologToPiTRSProof
SUB_3_IN_GGA3(s_11(X), s_11(Y), Z) -> SUB_3_IN_GGA3(X, Y, Z)
rem_3_in_gga3(X, Y, R) -> if_rem_3_in_1_gga4(X, Y, R, notZero_1_in_g1(Y))
notZero_1_in_g1(s_11(X)) -> notZero_1_out_g1(s_11(X))
if_rem_3_in_1_gga4(X, Y, R, notZero_1_out_g1(Y)) -> if_rem_3_in_2_gga4(X, Y, R, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_gga4(X, Y, Z, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_gga3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
if_rem_3_in_2_gga4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> if_rem_3_in_3_gga5(X, Y, R, Z, rem_3_in_gga3(Z, Y, R))
rem_3_in_gga3(X, Y, X) -> if_rem_3_in_4_gga3(X, Y, notZero_1_in_g1(Y))
if_rem_3_in_4_gga3(X, Y, notZero_1_out_g1(Y)) -> if_rem_3_in_5_gga3(X, Y, geq_2_in_gg2(X, Y))
geq_2_in_gg2(s_11(X), s_11(Y)) -> if_geq_2_in_1_gg3(X, Y, geq_2_in_gg2(X, Y))
geq_2_in_gg2(X, 0_0) -> geq_2_out_gg2(X, 0_0)
if_geq_2_in_1_gg3(X, Y, geq_2_out_gg2(X, Y)) -> geq_2_out_gg2(s_11(X), s_11(Y))
if_rem_3_in_5_gga3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_gga3(X, Y, X)
if_rem_3_in_3_gga5(X, Y, R, Z, rem_3_out_gga3(Z, Y, R)) -> rem_3_out_gga3(X, Y, R)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
↳ PrologToPiTRSProof
SUB_3_IN_GGA3(s_11(X), s_11(Y), Z) -> SUB_3_IN_GGA3(X, Y, Z)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
↳ PiDP
↳ PrologToPiTRSProof
SUB_3_IN_GGA2(s_11(X), s_11(Y)) -> SUB_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
↳ PiDP
↳ UsableRulesProof
↳ PrologToPiTRSProof
REM_3_IN_GGA3(X, Y, R) -> IF_REM_3_IN_1_GGA4(X, Y, R, notZero_1_in_g1(Y))
IF_REM_3_IN_2_GGA4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> REM_3_IN_GGA3(Z, Y, R)
IF_REM_3_IN_1_GGA4(X, Y, R, notZero_1_out_g1(Y)) -> IF_REM_3_IN_2_GGA4(X, Y, R, sub_3_in_gga3(X, Y, Z))
rem_3_in_gga3(X, Y, R) -> if_rem_3_in_1_gga4(X, Y, R, notZero_1_in_g1(Y))
notZero_1_in_g1(s_11(X)) -> notZero_1_out_g1(s_11(X))
if_rem_3_in_1_gga4(X, Y, R, notZero_1_out_g1(Y)) -> if_rem_3_in_2_gga4(X, Y, R, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_gga4(X, Y, Z, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_gga3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
if_rem_3_in_2_gga4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> if_rem_3_in_3_gga5(X, Y, R, Z, rem_3_in_gga3(Z, Y, R))
rem_3_in_gga3(X, Y, X) -> if_rem_3_in_4_gga3(X, Y, notZero_1_in_g1(Y))
if_rem_3_in_4_gga3(X, Y, notZero_1_out_g1(Y)) -> if_rem_3_in_5_gga3(X, Y, geq_2_in_gg2(X, Y))
geq_2_in_gg2(s_11(X), s_11(Y)) -> if_geq_2_in_1_gg3(X, Y, geq_2_in_gg2(X, Y))
geq_2_in_gg2(X, 0_0) -> geq_2_out_gg2(X, 0_0)
if_geq_2_in_1_gg3(X, Y, geq_2_out_gg2(X, Y)) -> geq_2_out_gg2(s_11(X), s_11(Y))
if_rem_3_in_5_gga3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_gga3(X, Y, X)
if_rem_3_in_3_gga5(X, Y, R, Z, rem_3_out_gga3(Z, Y, R)) -> rem_3_out_gga3(X, Y, R)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PrologToPiTRSProof
REM_3_IN_GGA3(X, Y, R) -> IF_REM_3_IN_1_GGA4(X, Y, R, notZero_1_in_g1(Y))
IF_REM_3_IN_2_GGA4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> REM_3_IN_GGA3(Z, Y, R)
IF_REM_3_IN_1_GGA4(X, Y, R, notZero_1_out_g1(Y)) -> IF_REM_3_IN_2_GGA4(X, Y, R, sub_3_in_gga3(X, Y, Z))
notZero_1_in_g1(s_11(X)) -> notZero_1_out_g1(s_11(X))
sub_3_in_gga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_gga4(X, Y, Z, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_gga3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ PrologToPiTRSProof
REM_3_IN_GGA2(X, Y) -> IF_REM_3_IN_1_GGA3(X, Y, notZero_1_in_g1(Y))
IF_REM_3_IN_2_GGA2(Y, sub_3_out_gga1(Z)) -> REM_3_IN_GGA2(Z, Y)
IF_REM_3_IN_1_GGA3(X, Y, notZero_1_out_g) -> IF_REM_3_IN_2_GGA2(Y, sub_3_in_gga2(X, Y))
notZero_1_in_g1(s_11(X)) -> notZero_1_out_g
sub_3_in_gga2(s_11(X), s_11(Y)) -> if_sub_3_in_1_gga1(sub_3_in_gga2(X, Y))
sub_3_in_gga2(X, 0_0) -> sub_3_out_gga1(X)
if_sub_3_in_1_gga1(sub_3_out_gga1(Z)) -> sub_3_out_gga1(Z)
notZero_1_in_g1(x0)
sub_3_in_gga2(x0, x1)
if_sub_3_in_1_gga1(x0)
rem_3_in_gga3(X, Y, R) -> if_rem_3_in_1_gga4(X, Y, R, notZero_1_in_g1(Y))
notZero_1_in_g1(s_11(X)) -> notZero_1_out_g1(s_11(X))
if_rem_3_in_1_gga4(X, Y, R, notZero_1_out_g1(Y)) -> if_rem_3_in_2_gga4(X, Y, R, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_gga4(X, Y, Z, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_gga3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
if_rem_3_in_2_gga4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> if_rem_3_in_3_gga5(X, Y, R, Z, rem_3_in_gga3(Z, Y, R))
rem_3_in_gga3(X, Y, X) -> if_rem_3_in_4_gga3(X, Y, notZero_1_in_g1(Y))
if_rem_3_in_4_gga3(X, Y, notZero_1_out_g1(Y)) -> if_rem_3_in_5_gga3(X, Y, geq_2_in_gg2(X, Y))
geq_2_in_gg2(s_11(X), s_11(Y)) -> if_geq_2_in_1_gg3(X, Y, geq_2_in_gg2(X, Y))
geq_2_in_gg2(X, 0_0) -> geq_2_out_gg2(X, 0_0)
if_geq_2_in_1_gg3(X, Y, geq_2_out_gg2(X, Y)) -> geq_2_out_gg2(s_11(X), s_11(Y))
if_rem_3_in_5_gga3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_gga3(X, Y, X)
if_rem_3_in_3_gga5(X, Y, R, Z, rem_3_out_gga3(Z, Y, R)) -> rem_3_out_gga3(X, Y, R)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG
↳ PROLOG
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
rem_3_in_gga3(X, Y, R) -> if_rem_3_in_1_gga4(X, Y, R, notZero_1_in_g1(Y))
notZero_1_in_g1(s_11(X)) -> notZero_1_out_g1(s_11(X))
if_rem_3_in_1_gga4(X, Y, R, notZero_1_out_g1(Y)) -> if_rem_3_in_2_gga4(X, Y, R, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_gga4(X, Y, Z, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_gga3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
if_rem_3_in_2_gga4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> if_rem_3_in_3_gga5(X, Y, R, Z, rem_3_in_gga3(Z, Y, R))
rem_3_in_gga3(X, Y, X) -> if_rem_3_in_4_gga3(X, Y, notZero_1_in_g1(Y))
if_rem_3_in_4_gga3(X, Y, notZero_1_out_g1(Y)) -> if_rem_3_in_5_gga3(X, Y, geq_2_in_gg2(X, Y))
geq_2_in_gg2(s_11(X), s_11(Y)) -> if_geq_2_in_1_gg3(X, Y, geq_2_in_gg2(X, Y))
geq_2_in_gg2(X, 0_0) -> geq_2_out_gg2(X, 0_0)
if_geq_2_in_1_gg3(X, Y, geq_2_out_gg2(X, Y)) -> geq_2_out_gg2(s_11(X), s_11(Y))
if_rem_3_in_5_gga3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_gga3(X, Y, X)
if_rem_3_in_3_gga5(X, Y, R, Z, rem_3_out_gga3(Z, Y, R)) -> rem_3_out_gga3(X, Y, R)
REM_3_IN_GGA3(X, Y, R) -> IF_REM_3_IN_1_GGA4(X, Y, R, notZero_1_in_g1(Y))
REM_3_IN_GGA3(X, Y, R) -> NOTZERO_1_IN_G1(Y)
IF_REM_3_IN_1_GGA4(X, Y, R, notZero_1_out_g1(Y)) -> IF_REM_3_IN_2_GGA4(X, Y, R, sub_3_in_gga3(X, Y, Z))
IF_REM_3_IN_1_GGA4(X, Y, R, notZero_1_out_g1(Y)) -> SUB_3_IN_GGA3(X, Y, Z)
SUB_3_IN_GGA3(s_11(X), s_11(Y), Z) -> IF_SUB_3_IN_1_GGA4(X, Y, Z, sub_3_in_gga3(X, Y, Z))
SUB_3_IN_GGA3(s_11(X), s_11(Y), Z) -> SUB_3_IN_GGA3(X, Y, Z)
IF_REM_3_IN_2_GGA4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> IF_REM_3_IN_3_GGA5(X, Y, R, Z, rem_3_in_gga3(Z, Y, R))
IF_REM_3_IN_2_GGA4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> REM_3_IN_GGA3(Z, Y, R)
REM_3_IN_GGA3(X, Y, X) -> IF_REM_3_IN_4_GGA3(X, Y, notZero_1_in_g1(Y))
REM_3_IN_GGA3(X, Y, X) -> NOTZERO_1_IN_G1(Y)
IF_REM_3_IN_4_GGA3(X, Y, notZero_1_out_g1(Y)) -> IF_REM_3_IN_5_GGA3(X, Y, geq_2_in_gg2(X, Y))
IF_REM_3_IN_4_GGA3(X, Y, notZero_1_out_g1(Y)) -> GEQ_2_IN_GG2(X, Y)
GEQ_2_IN_GG2(s_11(X), s_11(Y)) -> IF_GEQ_2_IN_1_GG3(X, Y, geq_2_in_gg2(X, Y))
GEQ_2_IN_GG2(s_11(X), s_11(Y)) -> GEQ_2_IN_GG2(X, Y)
rem_3_in_gga3(X, Y, R) -> if_rem_3_in_1_gga4(X, Y, R, notZero_1_in_g1(Y))
notZero_1_in_g1(s_11(X)) -> notZero_1_out_g1(s_11(X))
if_rem_3_in_1_gga4(X, Y, R, notZero_1_out_g1(Y)) -> if_rem_3_in_2_gga4(X, Y, R, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_gga4(X, Y, Z, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_gga3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
if_rem_3_in_2_gga4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> if_rem_3_in_3_gga5(X, Y, R, Z, rem_3_in_gga3(Z, Y, R))
rem_3_in_gga3(X, Y, X) -> if_rem_3_in_4_gga3(X, Y, notZero_1_in_g1(Y))
if_rem_3_in_4_gga3(X, Y, notZero_1_out_g1(Y)) -> if_rem_3_in_5_gga3(X, Y, geq_2_in_gg2(X, Y))
geq_2_in_gg2(s_11(X), s_11(Y)) -> if_geq_2_in_1_gg3(X, Y, geq_2_in_gg2(X, Y))
geq_2_in_gg2(X, 0_0) -> geq_2_out_gg2(X, 0_0)
if_geq_2_in_1_gg3(X, Y, geq_2_out_gg2(X, Y)) -> geq_2_out_gg2(s_11(X), s_11(Y))
if_rem_3_in_5_gga3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_gga3(X, Y, X)
if_rem_3_in_3_gga5(X, Y, R, Z, rem_3_out_gga3(Z, Y, R)) -> rem_3_out_gga3(X, Y, R)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
REM_3_IN_GGA3(X, Y, R) -> IF_REM_3_IN_1_GGA4(X, Y, R, notZero_1_in_g1(Y))
REM_3_IN_GGA3(X, Y, R) -> NOTZERO_1_IN_G1(Y)
IF_REM_3_IN_1_GGA4(X, Y, R, notZero_1_out_g1(Y)) -> IF_REM_3_IN_2_GGA4(X, Y, R, sub_3_in_gga3(X, Y, Z))
IF_REM_3_IN_1_GGA4(X, Y, R, notZero_1_out_g1(Y)) -> SUB_3_IN_GGA3(X, Y, Z)
SUB_3_IN_GGA3(s_11(X), s_11(Y), Z) -> IF_SUB_3_IN_1_GGA4(X, Y, Z, sub_3_in_gga3(X, Y, Z))
SUB_3_IN_GGA3(s_11(X), s_11(Y), Z) -> SUB_3_IN_GGA3(X, Y, Z)
IF_REM_3_IN_2_GGA4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> IF_REM_3_IN_3_GGA5(X, Y, R, Z, rem_3_in_gga3(Z, Y, R))
IF_REM_3_IN_2_GGA4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> REM_3_IN_GGA3(Z, Y, R)
REM_3_IN_GGA3(X, Y, X) -> IF_REM_3_IN_4_GGA3(X, Y, notZero_1_in_g1(Y))
REM_3_IN_GGA3(X, Y, X) -> NOTZERO_1_IN_G1(Y)
IF_REM_3_IN_4_GGA3(X, Y, notZero_1_out_g1(Y)) -> IF_REM_3_IN_5_GGA3(X, Y, geq_2_in_gg2(X, Y))
IF_REM_3_IN_4_GGA3(X, Y, notZero_1_out_g1(Y)) -> GEQ_2_IN_GG2(X, Y)
GEQ_2_IN_GG2(s_11(X), s_11(Y)) -> IF_GEQ_2_IN_1_GG3(X, Y, geq_2_in_gg2(X, Y))
GEQ_2_IN_GG2(s_11(X), s_11(Y)) -> GEQ_2_IN_GG2(X, Y)
rem_3_in_gga3(X, Y, R) -> if_rem_3_in_1_gga4(X, Y, R, notZero_1_in_g1(Y))
notZero_1_in_g1(s_11(X)) -> notZero_1_out_g1(s_11(X))
if_rem_3_in_1_gga4(X, Y, R, notZero_1_out_g1(Y)) -> if_rem_3_in_2_gga4(X, Y, R, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_gga4(X, Y, Z, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_gga3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
if_rem_3_in_2_gga4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> if_rem_3_in_3_gga5(X, Y, R, Z, rem_3_in_gga3(Z, Y, R))
rem_3_in_gga3(X, Y, X) -> if_rem_3_in_4_gga3(X, Y, notZero_1_in_g1(Y))
if_rem_3_in_4_gga3(X, Y, notZero_1_out_g1(Y)) -> if_rem_3_in_5_gga3(X, Y, geq_2_in_gg2(X, Y))
geq_2_in_gg2(s_11(X), s_11(Y)) -> if_geq_2_in_1_gg3(X, Y, geq_2_in_gg2(X, Y))
geq_2_in_gg2(X, 0_0) -> geq_2_out_gg2(X, 0_0)
if_geq_2_in_1_gg3(X, Y, geq_2_out_gg2(X, Y)) -> geq_2_out_gg2(s_11(X), s_11(Y))
if_rem_3_in_5_gga3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_gga3(X, Y, X)
if_rem_3_in_3_gga5(X, Y, R, Z, rem_3_out_gga3(Z, Y, R)) -> rem_3_out_gga3(X, Y, R)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDP
GEQ_2_IN_GG2(s_11(X), s_11(Y)) -> GEQ_2_IN_GG2(X, Y)
rem_3_in_gga3(X, Y, R) -> if_rem_3_in_1_gga4(X, Y, R, notZero_1_in_g1(Y))
notZero_1_in_g1(s_11(X)) -> notZero_1_out_g1(s_11(X))
if_rem_3_in_1_gga4(X, Y, R, notZero_1_out_g1(Y)) -> if_rem_3_in_2_gga4(X, Y, R, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_gga4(X, Y, Z, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_gga3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
if_rem_3_in_2_gga4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> if_rem_3_in_3_gga5(X, Y, R, Z, rem_3_in_gga3(Z, Y, R))
rem_3_in_gga3(X, Y, X) -> if_rem_3_in_4_gga3(X, Y, notZero_1_in_g1(Y))
if_rem_3_in_4_gga3(X, Y, notZero_1_out_g1(Y)) -> if_rem_3_in_5_gga3(X, Y, geq_2_in_gg2(X, Y))
geq_2_in_gg2(s_11(X), s_11(Y)) -> if_geq_2_in_1_gg3(X, Y, geq_2_in_gg2(X, Y))
geq_2_in_gg2(X, 0_0) -> geq_2_out_gg2(X, 0_0)
if_geq_2_in_1_gg3(X, Y, geq_2_out_gg2(X, Y)) -> geq_2_out_gg2(s_11(X), s_11(Y))
if_rem_3_in_5_gga3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_gga3(X, Y, X)
if_rem_3_in_3_gga5(X, Y, R, Z, rem_3_out_gga3(Z, Y, R)) -> rem_3_out_gga3(X, Y, R)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
↳ PiDP
GEQ_2_IN_GG2(s_11(X), s_11(Y)) -> GEQ_2_IN_GG2(X, Y)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
↳ PiDP
↳ PiDP
GEQ_2_IN_GG2(s_11(X), s_11(Y)) -> GEQ_2_IN_GG2(X, Y)
From the DPs we obtained the following set of size-change graphs:
↳ PROLOG
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
SUB_3_IN_GGA3(s_11(X), s_11(Y), Z) -> SUB_3_IN_GGA3(X, Y, Z)
rem_3_in_gga3(X, Y, R) -> if_rem_3_in_1_gga4(X, Y, R, notZero_1_in_g1(Y))
notZero_1_in_g1(s_11(X)) -> notZero_1_out_g1(s_11(X))
if_rem_3_in_1_gga4(X, Y, R, notZero_1_out_g1(Y)) -> if_rem_3_in_2_gga4(X, Y, R, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_gga4(X, Y, Z, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_gga3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
if_rem_3_in_2_gga4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> if_rem_3_in_3_gga5(X, Y, R, Z, rem_3_in_gga3(Z, Y, R))
rem_3_in_gga3(X, Y, X) -> if_rem_3_in_4_gga3(X, Y, notZero_1_in_g1(Y))
if_rem_3_in_4_gga3(X, Y, notZero_1_out_g1(Y)) -> if_rem_3_in_5_gga3(X, Y, geq_2_in_gg2(X, Y))
geq_2_in_gg2(s_11(X), s_11(Y)) -> if_geq_2_in_1_gg3(X, Y, geq_2_in_gg2(X, Y))
geq_2_in_gg2(X, 0_0) -> geq_2_out_gg2(X, 0_0)
if_geq_2_in_1_gg3(X, Y, geq_2_out_gg2(X, Y)) -> geq_2_out_gg2(s_11(X), s_11(Y))
if_rem_3_in_5_gga3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_gga3(X, Y, X)
if_rem_3_in_3_gga5(X, Y, R, Z, rem_3_out_gga3(Z, Y, R)) -> rem_3_out_gga3(X, Y, R)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
SUB_3_IN_GGA3(s_11(X), s_11(Y), Z) -> SUB_3_IN_GGA3(X, Y, Z)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
↳ PiDP
SUB_3_IN_GGA2(s_11(X), s_11(Y)) -> SUB_3_IN_GGA2(X, Y)
From the DPs we obtained the following set of size-change graphs:
↳ PROLOG
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
REM_3_IN_GGA3(X, Y, R) -> IF_REM_3_IN_1_GGA4(X, Y, R, notZero_1_in_g1(Y))
IF_REM_3_IN_2_GGA4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> REM_3_IN_GGA3(Z, Y, R)
IF_REM_3_IN_1_GGA4(X, Y, R, notZero_1_out_g1(Y)) -> IF_REM_3_IN_2_GGA4(X, Y, R, sub_3_in_gga3(X, Y, Z))
rem_3_in_gga3(X, Y, R) -> if_rem_3_in_1_gga4(X, Y, R, notZero_1_in_g1(Y))
notZero_1_in_g1(s_11(X)) -> notZero_1_out_g1(s_11(X))
if_rem_3_in_1_gga4(X, Y, R, notZero_1_out_g1(Y)) -> if_rem_3_in_2_gga4(X, Y, R, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_gga4(X, Y, Z, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_gga3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
if_rem_3_in_2_gga4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> if_rem_3_in_3_gga5(X, Y, R, Z, rem_3_in_gga3(Z, Y, R))
rem_3_in_gga3(X, Y, X) -> if_rem_3_in_4_gga3(X, Y, notZero_1_in_g1(Y))
if_rem_3_in_4_gga3(X, Y, notZero_1_out_g1(Y)) -> if_rem_3_in_5_gga3(X, Y, geq_2_in_gg2(X, Y))
geq_2_in_gg2(s_11(X), s_11(Y)) -> if_geq_2_in_1_gg3(X, Y, geq_2_in_gg2(X, Y))
geq_2_in_gg2(X, 0_0) -> geq_2_out_gg2(X, 0_0)
if_geq_2_in_1_gg3(X, Y, geq_2_out_gg2(X, Y)) -> geq_2_out_gg2(s_11(X), s_11(Y))
if_rem_3_in_5_gga3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_gga3(X, Y, X)
if_rem_3_in_3_gga5(X, Y, R, Z, rem_3_out_gga3(Z, Y, R)) -> rem_3_out_gga3(X, Y, R)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
REM_3_IN_GGA3(X, Y, R) -> IF_REM_3_IN_1_GGA4(X, Y, R, notZero_1_in_g1(Y))
IF_REM_3_IN_2_GGA4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> REM_3_IN_GGA3(Z, Y, R)
IF_REM_3_IN_1_GGA4(X, Y, R, notZero_1_out_g1(Y)) -> IF_REM_3_IN_2_GGA4(X, Y, R, sub_3_in_gga3(X, Y, Z))
notZero_1_in_g1(s_11(X)) -> notZero_1_out_g1(s_11(X))
sub_3_in_gga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_gga4(X, Y, Z, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_gga3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPPoloProof
REM_3_IN_GGA2(X, Y) -> IF_REM_3_IN_1_GGA3(X, Y, notZero_1_in_g1(Y))
IF_REM_3_IN_2_GGA3(X, Y, sub_3_out_gga3(X, Y, Z)) -> REM_3_IN_GGA2(Z, Y)
IF_REM_3_IN_1_GGA3(X, Y, notZero_1_out_g1(Y)) -> IF_REM_3_IN_2_GGA3(X, Y, sub_3_in_gga2(X, Y))
notZero_1_in_g1(s_11(X)) -> notZero_1_out_g1(s_11(X))
sub_3_in_gga2(s_11(X), s_11(Y)) -> if_sub_3_in_1_gga3(X, Y, sub_3_in_gga2(X, Y))
sub_3_in_gga2(X, 0_0) -> sub_3_out_gga3(X, 0_0, X)
if_sub_3_in_1_gga3(X, Y, sub_3_out_gga3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
notZero_1_in_g1(x0)
sub_3_in_gga2(x0, x1)
if_sub_3_in_1_gga3(x0, x1, x2)
The remaining Dependency Pairs were at least non-strictly be oriented.
IF_REM_3_IN_1_GGA3(X, Y, notZero_1_out_g1(Y)) -> IF_REM_3_IN_2_GGA3(X, Y, sub_3_in_gga2(X, Y))
With the implicit AFS we had to orient the following set of usable rules non-strictly.
REM_3_IN_GGA2(X, Y) -> IF_REM_3_IN_1_GGA3(X, Y, notZero_1_in_g1(Y))
IF_REM_3_IN_2_GGA3(X, Y, sub_3_out_gga3(X, Y, Z)) -> REM_3_IN_GGA2(Z, Y)
Used ordering: POLO with Polynomial interpretation:
sub_3_in_gga2(X, 0_0) -> sub_3_out_gga3(X, 0_0, X)
notZero_1_in_g1(s_11(X)) -> notZero_1_out_g1(s_11(X))
if_sub_3_in_1_gga3(X, Y, sub_3_out_gga3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
sub_3_in_gga2(s_11(X), s_11(Y)) -> if_sub_3_in_1_gga3(X, Y, sub_3_in_gga2(X, Y))
POL(0_0) = 0
POL(IF_REM_3_IN_1_GGA3(x1, x2, x3)) = x1 + x3
POL(sub_3_out_gga3(x1, x2, x3)) = x2 + x3
POL(REM_3_IN_GGA2(x1, x2)) = x1 + x2
POL(IF_REM_3_IN_2_GGA3(x1, x2, x3)) = x3
POL(if_sub_3_in_1_gga3(x1, x2, x3)) = 1 + x3
POL(sub_3_in_gga2(x1, x2)) = x1
POL(notZero_1_in_g1(x1)) = x1
POL(s_11(x1)) = 1 + x1
POL(notZero_1_out_g1(x1)) = 1
↳ PROLOG
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPPoloProof
↳ QDP
↳ DependencyGraphProof
REM_3_IN_GGA2(X, Y) -> IF_REM_3_IN_1_GGA3(X, Y, notZero_1_in_g1(Y))
IF_REM_3_IN_2_GGA3(X, Y, sub_3_out_gga3(X, Y, Z)) -> REM_3_IN_GGA2(Z, Y)
notZero_1_in_g1(s_11(X)) -> notZero_1_out_g1(s_11(X))
sub_3_in_gga2(s_11(X), s_11(Y)) -> if_sub_3_in_1_gga3(X, Y, sub_3_in_gga2(X, Y))
sub_3_in_gga2(X, 0_0) -> sub_3_out_gga3(X, 0_0, X)
if_sub_3_in_1_gga3(X, Y, sub_3_out_gga3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
notZero_1_in_g1(x0)
sub_3_in_gga2(x0, x1)
if_sub_3_in_1_gga3(x0, x1, x2)