↳ PROLOG
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
With regard to the inferred argument filtering the predicates were used in the following modes:
rem3: (b,f,b) (f,b,b)
sub3: (b,b,f) (f,f,f) (f,b,f)
geq2: (b,b) (f,f)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
rem_3_in_gag3(X, Y, R) -> if_rem_3_in_1_gag4(X, Y, R, notZero_1_in_a1(Y))
notZero_1_in_a1(s_11(X)) -> notZero_1_out_a1(s_11(X))
if_rem_3_in_1_gag4(X, Y, R, notZero_1_out_a1(Y)) -> if_rem_3_in_2_gag4(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_aaa3(X, Y, Z))
sub_3_in_aaa3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aaa4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aaa3(X, 0_0, X) -> sub_3_out_aaa3(X, 0_0, X)
if_sub_3_in_1_aaa4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aaa3(s_11(X), s_11(Y), Z)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_rem_3_in_2_gag4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, R) -> if_rem_3_in_1_agg4(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_agg4(X, Y, R, notZero_1_out_g1(Y)) -> if_rem_3_in_2_agg4(X, Y, R, sub_3_in_aga3(X, Y, Z))
sub_3_in_aga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aga4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
if_sub_3_in_1_aga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aga3(s_11(X), s_11(Y), Z)
sub_3_in_aga3(X, 0_0, X) -> sub_3_out_aga3(X, 0_0, X)
if_rem_3_in_2_agg4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, X) -> if_rem_3_in_4_agg3(X, Y, notZero_1_in_g1(Y))
if_rem_3_in_4_agg3(X, Y, notZero_1_out_g1(Y)) -> if_rem_3_in_5_agg3(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_aa2(X, Y))
geq_2_in_aa2(s_11(X), s_11(Y)) -> if_geq_2_in_1_aa3(X, Y, geq_2_in_aa2(X, Y))
geq_2_in_aa2(X, 0_0) -> geq_2_out_aa2(X, 0_0)
if_geq_2_in_1_aa3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_aa2(s_11(X), s_11(Y))
if_geq_2_in_1_gg3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_gg2(s_11(X), s_11(Y))
geq_2_in_gg2(X, 0_0) -> geq_2_out_gg2(X, 0_0)
if_rem_3_in_5_agg3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_agg3(X, Y, X)
if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_agg3(X, Y, R)
if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_gag3(X, Y, R)
rem_3_in_gag3(X, Y, X) -> if_rem_3_in_4_gag3(X, Y, notZero_1_in_a1(Y))
if_rem_3_in_4_gag3(X, Y, notZero_1_out_a1(Y)) -> if_rem_3_in_5_gag3(X, Y, geq_2_in_gg2(X, Y))
if_rem_3_in_5_gag3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_gag3(X, Y, X)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PrologToPiTRSProof
rem_3_in_gag3(X, Y, R) -> if_rem_3_in_1_gag4(X, Y, R, notZero_1_in_a1(Y))
notZero_1_in_a1(s_11(X)) -> notZero_1_out_a1(s_11(X))
if_rem_3_in_1_gag4(X, Y, R, notZero_1_out_a1(Y)) -> if_rem_3_in_2_gag4(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_aaa3(X, Y, Z))
sub_3_in_aaa3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aaa4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aaa3(X, 0_0, X) -> sub_3_out_aaa3(X, 0_0, X)
if_sub_3_in_1_aaa4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aaa3(s_11(X), s_11(Y), Z)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_rem_3_in_2_gag4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, R) -> if_rem_3_in_1_agg4(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_agg4(X, Y, R, notZero_1_out_g1(Y)) -> if_rem_3_in_2_agg4(X, Y, R, sub_3_in_aga3(X, Y, Z))
sub_3_in_aga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aga4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
if_sub_3_in_1_aga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aga3(s_11(X), s_11(Y), Z)
sub_3_in_aga3(X, 0_0, X) -> sub_3_out_aga3(X, 0_0, X)
if_rem_3_in_2_agg4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, X) -> if_rem_3_in_4_agg3(X, Y, notZero_1_in_g1(Y))
if_rem_3_in_4_agg3(X, Y, notZero_1_out_g1(Y)) -> if_rem_3_in_5_agg3(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_aa2(X, Y))
geq_2_in_aa2(s_11(X), s_11(Y)) -> if_geq_2_in_1_aa3(X, Y, geq_2_in_aa2(X, Y))
geq_2_in_aa2(X, 0_0) -> geq_2_out_aa2(X, 0_0)
if_geq_2_in_1_aa3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_aa2(s_11(X), s_11(Y))
if_geq_2_in_1_gg3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_gg2(s_11(X), s_11(Y))
geq_2_in_gg2(X, 0_0) -> geq_2_out_gg2(X, 0_0)
if_rem_3_in_5_agg3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_agg3(X, Y, X)
if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_agg3(X, Y, R)
if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_gag3(X, Y, R)
rem_3_in_gag3(X, Y, X) -> if_rem_3_in_4_gag3(X, Y, notZero_1_in_a1(Y))
if_rem_3_in_4_gag3(X, Y, notZero_1_out_a1(Y)) -> if_rem_3_in_5_gag3(X, Y, geq_2_in_gg2(X, Y))
if_rem_3_in_5_gag3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_gag3(X, Y, X)
REM_3_IN_GAG3(X, Y, R) -> IF_REM_3_IN_1_GAG4(X, Y, R, notZero_1_in_a1(Y))
REM_3_IN_GAG3(X, Y, R) -> NOTZERO_1_IN_A1(Y)
IF_REM_3_IN_1_GAG4(X, Y, R, notZero_1_out_a1(Y)) -> IF_REM_3_IN_2_GAG4(X, Y, R, sub_3_in_gga3(X, Y, Z))
IF_REM_3_IN_1_GAG4(X, Y, R, notZero_1_out_a1(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_aaa3(X, Y, Z))
SUB_3_IN_GGA3(s_11(X), s_11(Y), Z) -> SUB_3_IN_AAA3(X, Y, Z)
SUB_3_IN_AAA3(s_11(X), s_11(Y), Z) -> IF_SUB_3_IN_1_AAA4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
SUB_3_IN_AAA3(s_11(X), s_11(Y), Z) -> SUB_3_IN_AAA3(X, Y, Z)
IF_REM_3_IN_2_GAG4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> IF_REM_3_IN_3_GAG5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
IF_REM_3_IN_2_GAG4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> REM_3_IN_AGG3(Z, Y, R)
REM_3_IN_AGG3(X, Y, R) -> IF_REM_3_IN_1_AGG4(X, Y, R, notZero_1_in_g1(Y))
REM_3_IN_AGG3(X, Y, R) -> NOTZERO_1_IN_G1(Y)
IF_REM_3_IN_1_AGG4(X, Y, R, notZero_1_out_g1(Y)) -> IF_REM_3_IN_2_AGG4(X, Y, R, sub_3_in_aga3(X, Y, Z))
IF_REM_3_IN_1_AGG4(X, Y, R, notZero_1_out_g1(Y)) -> SUB_3_IN_AGA3(X, Y, Z)
SUB_3_IN_AGA3(s_11(X), s_11(Y), Z) -> IF_SUB_3_IN_1_AGA4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
SUB_3_IN_AGA3(s_11(X), s_11(Y), Z) -> SUB_3_IN_AAA3(X, Y, Z)
IF_REM_3_IN_2_AGG4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> IF_REM_3_IN_3_AGG5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
IF_REM_3_IN_2_AGG4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> REM_3_IN_AGG3(Z, Y, R)
REM_3_IN_AGG3(X, Y, X) -> IF_REM_3_IN_4_AGG3(X, Y, notZero_1_in_g1(Y))
REM_3_IN_AGG3(X, Y, X) -> NOTZERO_1_IN_G1(Y)
IF_REM_3_IN_4_AGG3(X, Y, notZero_1_out_g1(Y)) -> IF_REM_3_IN_5_AGG3(X, Y, geq_2_in_gg2(X, Y))
IF_REM_3_IN_4_AGG3(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_aa2(X, Y))
GEQ_2_IN_GG2(s_11(X), s_11(Y)) -> GEQ_2_IN_AA2(X, Y)
GEQ_2_IN_AA2(s_11(X), s_11(Y)) -> IF_GEQ_2_IN_1_AA3(X, Y, geq_2_in_aa2(X, Y))
GEQ_2_IN_AA2(s_11(X), s_11(Y)) -> GEQ_2_IN_AA2(X, Y)
REM_3_IN_GAG3(X, Y, X) -> IF_REM_3_IN_4_GAG3(X, Y, notZero_1_in_a1(Y))
REM_3_IN_GAG3(X, Y, X) -> NOTZERO_1_IN_A1(Y)
IF_REM_3_IN_4_GAG3(X, Y, notZero_1_out_a1(Y)) -> IF_REM_3_IN_5_GAG3(X, Y, geq_2_in_gg2(X, Y))
IF_REM_3_IN_4_GAG3(X, Y, notZero_1_out_a1(Y)) -> GEQ_2_IN_GG2(X, Y)
rem_3_in_gag3(X, Y, R) -> if_rem_3_in_1_gag4(X, Y, R, notZero_1_in_a1(Y))
notZero_1_in_a1(s_11(X)) -> notZero_1_out_a1(s_11(X))
if_rem_3_in_1_gag4(X, Y, R, notZero_1_out_a1(Y)) -> if_rem_3_in_2_gag4(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_aaa3(X, Y, Z))
sub_3_in_aaa3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aaa4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aaa3(X, 0_0, X) -> sub_3_out_aaa3(X, 0_0, X)
if_sub_3_in_1_aaa4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aaa3(s_11(X), s_11(Y), Z)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_rem_3_in_2_gag4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, R) -> if_rem_3_in_1_agg4(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_agg4(X, Y, R, notZero_1_out_g1(Y)) -> if_rem_3_in_2_agg4(X, Y, R, sub_3_in_aga3(X, Y, Z))
sub_3_in_aga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aga4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
if_sub_3_in_1_aga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aga3(s_11(X), s_11(Y), Z)
sub_3_in_aga3(X, 0_0, X) -> sub_3_out_aga3(X, 0_0, X)
if_rem_3_in_2_agg4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, X) -> if_rem_3_in_4_agg3(X, Y, notZero_1_in_g1(Y))
if_rem_3_in_4_agg3(X, Y, notZero_1_out_g1(Y)) -> if_rem_3_in_5_agg3(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_aa2(X, Y))
geq_2_in_aa2(s_11(X), s_11(Y)) -> if_geq_2_in_1_aa3(X, Y, geq_2_in_aa2(X, Y))
geq_2_in_aa2(X, 0_0) -> geq_2_out_aa2(X, 0_0)
if_geq_2_in_1_aa3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_aa2(s_11(X), s_11(Y))
if_geq_2_in_1_gg3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_gg2(s_11(X), s_11(Y))
geq_2_in_gg2(X, 0_0) -> geq_2_out_gg2(X, 0_0)
if_rem_3_in_5_agg3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_agg3(X, Y, X)
if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_agg3(X, Y, R)
if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_gag3(X, Y, R)
rem_3_in_gag3(X, Y, X) -> if_rem_3_in_4_gag3(X, Y, notZero_1_in_a1(Y))
if_rem_3_in_4_gag3(X, Y, notZero_1_out_a1(Y)) -> if_rem_3_in_5_gag3(X, Y, geq_2_in_gg2(X, Y))
if_rem_3_in_5_gag3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_gag3(X, Y, X)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PrologToPiTRSProof
REM_3_IN_GAG3(X, Y, R) -> IF_REM_3_IN_1_GAG4(X, Y, R, notZero_1_in_a1(Y))
REM_3_IN_GAG3(X, Y, R) -> NOTZERO_1_IN_A1(Y)
IF_REM_3_IN_1_GAG4(X, Y, R, notZero_1_out_a1(Y)) -> IF_REM_3_IN_2_GAG4(X, Y, R, sub_3_in_gga3(X, Y, Z))
IF_REM_3_IN_1_GAG4(X, Y, R, notZero_1_out_a1(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_aaa3(X, Y, Z))
SUB_3_IN_GGA3(s_11(X), s_11(Y), Z) -> SUB_3_IN_AAA3(X, Y, Z)
SUB_3_IN_AAA3(s_11(X), s_11(Y), Z) -> IF_SUB_3_IN_1_AAA4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
SUB_3_IN_AAA3(s_11(X), s_11(Y), Z) -> SUB_3_IN_AAA3(X, Y, Z)
IF_REM_3_IN_2_GAG4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> IF_REM_3_IN_3_GAG5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
IF_REM_3_IN_2_GAG4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> REM_3_IN_AGG3(Z, Y, R)
REM_3_IN_AGG3(X, Y, R) -> IF_REM_3_IN_1_AGG4(X, Y, R, notZero_1_in_g1(Y))
REM_3_IN_AGG3(X, Y, R) -> NOTZERO_1_IN_G1(Y)
IF_REM_3_IN_1_AGG4(X, Y, R, notZero_1_out_g1(Y)) -> IF_REM_3_IN_2_AGG4(X, Y, R, sub_3_in_aga3(X, Y, Z))
IF_REM_3_IN_1_AGG4(X, Y, R, notZero_1_out_g1(Y)) -> SUB_3_IN_AGA3(X, Y, Z)
SUB_3_IN_AGA3(s_11(X), s_11(Y), Z) -> IF_SUB_3_IN_1_AGA4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
SUB_3_IN_AGA3(s_11(X), s_11(Y), Z) -> SUB_3_IN_AAA3(X, Y, Z)
IF_REM_3_IN_2_AGG4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> IF_REM_3_IN_3_AGG5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
IF_REM_3_IN_2_AGG4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> REM_3_IN_AGG3(Z, Y, R)
REM_3_IN_AGG3(X, Y, X) -> IF_REM_3_IN_4_AGG3(X, Y, notZero_1_in_g1(Y))
REM_3_IN_AGG3(X, Y, X) -> NOTZERO_1_IN_G1(Y)
IF_REM_3_IN_4_AGG3(X, Y, notZero_1_out_g1(Y)) -> IF_REM_3_IN_5_AGG3(X, Y, geq_2_in_gg2(X, Y))
IF_REM_3_IN_4_AGG3(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_aa2(X, Y))
GEQ_2_IN_GG2(s_11(X), s_11(Y)) -> GEQ_2_IN_AA2(X, Y)
GEQ_2_IN_AA2(s_11(X), s_11(Y)) -> IF_GEQ_2_IN_1_AA3(X, Y, geq_2_in_aa2(X, Y))
GEQ_2_IN_AA2(s_11(X), s_11(Y)) -> GEQ_2_IN_AA2(X, Y)
REM_3_IN_GAG3(X, Y, X) -> IF_REM_3_IN_4_GAG3(X, Y, notZero_1_in_a1(Y))
REM_3_IN_GAG3(X, Y, X) -> NOTZERO_1_IN_A1(Y)
IF_REM_3_IN_4_GAG3(X, Y, notZero_1_out_a1(Y)) -> IF_REM_3_IN_5_GAG3(X, Y, geq_2_in_gg2(X, Y))
IF_REM_3_IN_4_GAG3(X, Y, notZero_1_out_a1(Y)) -> GEQ_2_IN_GG2(X, Y)
rem_3_in_gag3(X, Y, R) -> if_rem_3_in_1_gag4(X, Y, R, notZero_1_in_a1(Y))
notZero_1_in_a1(s_11(X)) -> notZero_1_out_a1(s_11(X))
if_rem_3_in_1_gag4(X, Y, R, notZero_1_out_a1(Y)) -> if_rem_3_in_2_gag4(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_aaa3(X, Y, Z))
sub_3_in_aaa3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aaa4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aaa3(X, 0_0, X) -> sub_3_out_aaa3(X, 0_0, X)
if_sub_3_in_1_aaa4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aaa3(s_11(X), s_11(Y), Z)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_rem_3_in_2_gag4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, R) -> if_rem_3_in_1_agg4(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_agg4(X, Y, R, notZero_1_out_g1(Y)) -> if_rem_3_in_2_agg4(X, Y, R, sub_3_in_aga3(X, Y, Z))
sub_3_in_aga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aga4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
if_sub_3_in_1_aga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aga3(s_11(X), s_11(Y), Z)
sub_3_in_aga3(X, 0_0, X) -> sub_3_out_aga3(X, 0_0, X)
if_rem_3_in_2_agg4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, X) -> if_rem_3_in_4_agg3(X, Y, notZero_1_in_g1(Y))
if_rem_3_in_4_agg3(X, Y, notZero_1_out_g1(Y)) -> if_rem_3_in_5_agg3(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_aa2(X, Y))
geq_2_in_aa2(s_11(X), s_11(Y)) -> if_geq_2_in_1_aa3(X, Y, geq_2_in_aa2(X, Y))
geq_2_in_aa2(X, 0_0) -> geq_2_out_aa2(X, 0_0)
if_geq_2_in_1_aa3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_aa2(s_11(X), s_11(Y))
if_geq_2_in_1_gg3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_gg2(s_11(X), s_11(Y))
geq_2_in_gg2(X, 0_0) -> geq_2_out_gg2(X, 0_0)
if_rem_3_in_5_agg3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_agg3(X, Y, X)
if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_agg3(X, Y, R)
if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_gag3(X, Y, R)
rem_3_in_gag3(X, Y, X) -> if_rem_3_in_4_gag3(X, Y, notZero_1_in_a1(Y))
if_rem_3_in_4_gag3(X, Y, notZero_1_out_a1(Y)) -> if_rem_3_in_5_gag3(X, Y, geq_2_in_gg2(X, Y))
if_rem_3_in_5_gag3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_gag3(X, Y, X)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDP
↳ PrologToPiTRSProof
GEQ_2_IN_AA2(s_11(X), s_11(Y)) -> GEQ_2_IN_AA2(X, Y)
rem_3_in_gag3(X, Y, R) -> if_rem_3_in_1_gag4(X, Y, R, notZero_1_in_a1(Y))
notZero_1_in_a1(s_11(X)) -> notZero_1_out_a1(s_11(X))
if_rem_3_in_1_gag4(X, Y, R, notZero_1_out_a1(Y)) -> if_rem_3_in_2_gag4(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_aaa3(X, Y, Z))
sub_3_in_aaa3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aaa4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aaa3(X, 0_0, X) -> sub_3_out_aaa3(X, 0_0, X)
if_sub_3_in_1_aaa4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aaa3(s_11(X), s_11(Y), Z)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_rem_3_in_2_gag4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, R) -> if_rem_3_in_1_agg4(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_agg4(X, Y, R, notZero_1_out_g1(Y)) -> if_rem_3_in_2_agg4(X, Y, R, sub_3_in_aga3(X, Y, Z))
sub_3_in_aga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aga4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
if_sub_3_in_1_aga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aga3(s_11(X), s_11(Y), Z)
sub_3_in_aga3(X, 0_0, X) -> sub_3_out_aga3(X, 0_0, X)
if_rem_3_in_2_agg4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, X) -> if_rem_3_in_4_agg3(X, Y, notZero_1_in_g1(Y))
if_rem_3_in_4_agg3(X, Y, notZero_1_out_g1(Y)) -> if_rem_3_in_5_agg3(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_aa2(X, Y))
geq_2_in_aa2(s_11(X), s_11(Y)) -> if_geq_2_in_1_aa3(X, Y, geq_2_in_aa2(X, Y))
geq_2_in_aa2(X, 0_0) -> geq_2_out_aa2(X, 0_0)
if_geq_2_in_1_aa3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_aa2(s_11(X), s_11(Y))
if_geq_2_in_1_gg3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_gg2(s_11(X), s_11(Y))
geq_2_in_gg2(X, 0_0) -> geq_2_out_gg2(X, 0_0)
if_rem_3_in_5_agg3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_agg3(X, Y, X)
if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_agg3(X, Y, R)
if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_gag3(X, Y, R)
rem_3_in_gag3(X, Y, X) -> if_rem_3_in_4_gag3(X, Y, notZero_1_in_a1(Y))
if_rem_3_in_4_gag3(X, Y, notZero_1_out_a1(Y)) -> if_rem_3_in_5_gag3(X, Y, geq_2_in_gg2(X, Y))
if_rem_3_in_5_gag3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_gag3(X, Y, X)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
↳ PiDP
↳ PrologToPiTRSProof
GEQ_2_IN_AA2(s_11(X), s_11(Y)) -> GEQ_2_IN_AA2(X, Y)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ PiDP
↳ PiDP
↳ PrologToPiTRSProof
GEQ_2_IN_AA -> GEQ_2_IN_AA
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PrologToPiTRSProof
SUB_3_IN_AAA3(s_11(X), s_11(Y), Z) -> SUB_3_IN_AAA3(X, Y, Z)
rem_3_in_gag3(X, Y, R) -> if_rem_3_in_1_gag4(X, Y, R, notZero_1_in_a1(Y))
notZero_1_in_a1(s_11(X)) -> notZero_1_out_a1(s_11(X))
if_rem_3_in_1_gag4(X, Y, R, notZero_1_out_a1(Y)) -> if_rem_3_in_2_gag4(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_aaa3(X, Y, Z))
sub_3_in_aaa3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aaa4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aaa3(X, 0_0, X) -> sub_3_out_aaa3(X, 0_0, X)
if_sub_3_in_1_aaa4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aaa3(s_11(X), s_11(Y), Z)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_rem_3_in_2_gag4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, R) -> if_rem_3_in_1_agg4(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_agg4(X, Y, R, notZero_1_out_g1(Y)) -> if_rem_3_in_2_agg4(X, Y, R, sub_3_in_aga3(X, Y, Z))
sub_3_in_aga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aga4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
if_sub_3_in_1_aga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aga3(s_11(X), s_11(Y), Z)
sub_3_in_aga3(X, 0_0, X) -> sub_3_out_aga3(X, 0_0, X)
if_rem_3_in_2_agg4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, X) -> if_rem_3_in_4_agg3(X, Y, notZero_1_in_g1(Y))
if_rem_3_in_4_agg3(X, Y, notZero_1_out_g1(Y)) -> if_rem_3_in_5_agg3(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_aa2(X, Y))
geq_2_in_aa2(s_11(X), s_11(Y)) -> if_geq_2_in_1_aa3(X, Y, geq_2_in_aa2(X, Y))
geq_2_in_aa2(X, 0_0) -> geq_2_out_aa2(X, 0_0)
if_geq_2_in_1_aa3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_aa2(s_11(X), s_11(Y))
if_geq_2_in_1_gg3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_gg2(s_11(X), s_11(Y))
geq_2_in_gg2(X, 0_0) -> geq_2_out_gg2(X, 0_0)
if_rem_3_in_5_agg3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_agg3(X, Y, X)
if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_agg3(X, Y, R)
if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_gag3(X, Y, R)
rem_3_in_gag3(X, Y, X) -> if_rem_3_in_4_gag3(X, Y, notZero_1_in_a1(Y))
if_rem_3_in_4_gag3(X, Y, notZero_1_out_a1(Y)) -> if_rem_3_in_5_gag3(X, Y, geq_2_in_gg2(X, Y))
if_rem_3_in_5_gag3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_gag3(X, Y, X)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
↳ PrologToPiTRSProof
SUB_3_IN_AAA3(s_11(X), s_11(Y), Z) -> SUB_3_IN_AAA3(X, Y, Z)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ PiDP
↳ PrologToPiTRSProof
SUB_3_IN_AAA -> SUB_3_IN_AAA
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PrologToPiTRSProof
REM_3_IN_AGG3(X, Y, R) -> IF_REM_3_IN_1_AGG4(X, Y, R, notZero_1_in_g1(Y))
IF_REM_3_IN_2_AGG4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> REM_3_IN_AGG3(Z, Y, R)
IF_REM_3_IN_1_AGG4(X, Y, R, notZero_1_out_g1(Y)) -> IF_REM_3_IN_2_AGG4(X, Y, R, sub_3_in_aga3(X, Y, Z))
rem_3_in_gag3(X, Y, R) -> if_rem_3_in_1_gag4(X, Y, R, notZero_1_in_a1(Y))
notZero_1_in_a1(s_11(X)) -> notZero_1_out_a1(s_11(X))
if_rem_3_in_1_gag4(X, Y, R, notZero_1_out_a1(Y)) -> if_rem_3_in_2_gag4(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_aaa3(X, Y, Z))
sub_3_in_aaa3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aaa4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aaa3(X, 0_0, X) -> sub_3_out_aaa3(X, 0_0, X)
if_sub_3_in_1_aaa4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aaa3(s_11(X), s_11(Y), Z)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_rem_3_in_2_gag4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, R) -> if_rem_3_in_1_agg4(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_agg4(X, Y, R, notZero_1_out_g1(Y)) -> if_rem_3_in_2_agg4(X, Y, R, sub_3_in_aga3(X, Y, Z))
sub_3_in_aga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aga4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
if_sub_3_in_1_aga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aga3(s_11(X), s_11(Y), Z)
sub_3_in_aga3(X, 0_0, X) -> sub_3_out_aga3(X, 0_0, X)
if_rem_3_in_2_agg4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, X) -> if_rem_3_in_4_agg3(X, Y, notZero_1_in_g1(Y))
if_rem_3_in_4_agg3(X, Y, notZero_1_out_g1(Y)) -> if_rem_3_in_5_agg3(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_aa2(X, Y))
geq_2_in_aa2(s_11(X), s_11(Y)) -> if_geq_2_in_1_aa3(X, Y, geq_2_in_aa2(X, Y))
geq_2_in_aa2(X, 0_0) -> geq_2_out_aa2(X, 0_0)
if_geq_2_in_1_aa3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_aa2(s_11(X), s_11(Y))
if_geq_2_in_1_gg3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_gg2(s_11(X), s_11(Y))
geq_2_in_gg2(X, 0_0) -> geq_2_out_gg2(X, 0_0)
if_rem_3_in_5_agg3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_agg3(X, Y, X)
if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_agg3(X, Y, R)
if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_gag3(X, Y, R)
rem_3_in_gag3(X, Y, X) -> if_rem_3_in_4_gag3(X, Y, notZero_1_in_a1(Y))
if_rem_3_in_4_gag3(X, Y, notZero_1_out_a1(Y)) -> if_rem_3_in_5_gag3(X, Y, geq_2_in_gg2(X, Y))
if_rem_3_in_5_gag3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_gag3(X, Y, X)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PrologToPiTRSProof
REM_3_IN_AGG3(X, Y, R) -> IF_REM_3_IN_1_AGG4(X, Y, R, notZero_1_in_g1(Y))
IF_REM_3_IN_2_AGG4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> REM_3_IN_AGG3(Z, Y, R)
IF_REM_3_IN_1_AGG4(X, Y, R, notZero_1_out_g1(Y)) -> IF_REM_3_IN_2_AGG4(X, Y, R, sub_3_in_aga3(X, Y, Z))
notZero_1_in_g1(s_11(X)) -> notZero_1_out_g1(s_11(X))
sub_3_in_aga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aga4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aga3(X, 0_0, X) -> sub_3_out_aga3(X, 0_0, X)
if_sub_3_in_1_aga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aga3(s_11(X), s_11(Y), Z)
sub_3_in_aaa3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aaa4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aaa3(X, 0_0, X) -> sub_3_out_aaa3(X, 0_0, X)
if_sub_3_in_1_aaa4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aaa3(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_AGG2(Y, R) -> IF_REM_3_IN_1_AGG3(Y, R, notZero_1_in_g1(Y))
IF_REM_3_IN_2_AGG3(Y, R, sub_3_out_aga) -> REM_3_IN_AGG2(Y, R)
IF_REM_3_IN_1_AGG3(Y, R, notZero_1_out_g) -> IF_REM_3_IN_2_AGG3(Y, R, sub_3_in_aga1(Y))
notZero_1_in_g1(s_1) -> notZero_1_out_g
sub_3_in_aga1(s_1) -> if_sub_3_in_1_aga1(sub_3_in_aaa)
sub_3_in_aga1(0_0) -> sub_3_out_aga
if_sub_3_in_1_aga1(sub_3_out_aaa1(Y)) -> sub_3_out_aga
sub_3_in_aaa -> if_sub_3_in_1_aaa1(sub_3_in_aaa)
sub_3_in_aaa -> sub_3_out_aaa1(0_0)
if_sub_3_in_1_aaa1(sub_3_out_aaa1(Y)) -> sub_3_out_aaa1(s_1)
notZero_1_in_g1(x0)
sub_3_in_aga1(x0)
if_sub_3_in_1_aga1(x0)
sub_3_in_aaa
if_sub_3_in_1_aaa1(x0)
rem_3_in_gag3(X, Y, R) -> if_rem_3_in_1_gag4(X, Y, R, notZero_1_in_a1(Y))
notZero_1_in_a1(s_11(X)) -> notZero_1_out_a1(s_11(X))
if_rem_3_in_1_gag4(X, Y, R, notZero_1_out_a1(Y)) -> if_rem_3_in_2_gag4(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_aaa3(X, Y, Z))
sub_3_in_aaa3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aaa4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aaa3(X, 0_0, X) -> sub_3_out_aaa3(X, 0_0, X)
if_sub_3_in_1_aaa4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aaa3(s_11(X), s_11(Y), Z)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_rem_3_in_2_gag4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, R) -> if_rem_3_in_1_agg4(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_agg4(X, Y, R, notZero_1_out_g1(Y)) -> if_rem_3_in_2_agg4(X, Y, R, sub_3_in_aga3(X, Y, Z))
sub_3_in_aga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aga4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
if_sub_3_in_1_aga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aga3(s_11(X), s_11(Y), Z)
sub_3_in_aga3(X, 0_0, X) -> sub_3_out_aga3(X, 0_0, X)
if_rem_3_in_2_agg4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, X) -> if_rem_3_in_4_agg3(X, Y, notZero_1_in_g1(Y))
if_rem_3_in_4_agg3(X, Y, notZero_1_out_g1(Y)) -> if_rem_3_in_5_agg3(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_aa2(X, Y))
geq_2_in_aa2(s_11(X), s_11(Y)) -> if_geq_2_in_1_aa3(X, Y, geq_2_in_aa2(X, Y))
geq_2_in_aa2(X, 0_0) -> geq_2_out_aa2(X, 0_0)
if_geq_2_in_1_aa3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_aa2(s_11(X), s_11(Y))
if_geq_2_in_1_gg3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_gg2(s_11(X), s_11(Y))
geq_2_in_gg2(X, 0_0) -> geq_2_out_gg2(X, 0_0)
if_rem_3_in_5_agg3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_agg3(X, Y, X)
if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_agg3(X, Y, R)
if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_gag3(X, Y, R)
rem_3_in_gag3(X, Y, X) -> if_rem_3_in_4_gag3(X, Y, notZero_1_in_a1(Y))
if_rem_3_in_4_gag3(X, Y, notZero_1_out_a1(Y)) -> if_rem_3_in_5_gag3(X, Y, geq_2_in_gg2(X, Y))
if_rem_3_in_5_gag3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_gag3(X, Y, X)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG
↳ PROLOG
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
rem_3_in_gag3(X, Y, R) -> if_rem_3_in_1_gag4(X, Y, R, notZero_1_in_a1(Y))
notZero_1_in_a1(s_11(X)) -> notZero_1_out_a1(s_11(X))
if_rem_3_in_1_gag4(X, Y, R, notZero_1_out_a1(Y)) -> if_rem_3_in_2_gag4(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_aaa3(X, Y, Z))
sub_3_in_aaa3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aaa4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aaa3(X, 0_0, X) -> sub_3_out_aaa3(X, 0_0, X)
if_sub_3_in_1_aaa4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aaa3(s_11(X), s_11(Y), Z)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_rem_3_in_2_gag4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, R) -> if_rem_3_in_1_agg4(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_agg4(X, Y, R, notZero_1_out_g1(Y)) -> if_rem_3_in_2_agg4(X, Y, R, sub_3_in_aga3(X, Y, Z))
sub_3_in_aga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aga4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
if_sub_3_in_1_aga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aga3(s_11(X), s_11(Y), Z)
sub_3_in_aga3(X, 0_0, X) -> sub_3_out_aga3(X, 0_0, X)
if_rem_3_in_2_agg4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, X) -> if_rem_3_in_4_agg3(X, Y, notZero_1_in_g1(Y))
if_rem_3_in_4_agg3(X, Y, notZero_1_out_g1(Y)) -> if_rem_3_in_5_agg3(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_aa2(X, Y))
geq_2_in_aa2(s_11(X), s_11(Y)) -> if_geq_2_in_1_aa3(X, Y, geq_2_in_aa2(X, Y))
geq_2_in_aa2(X, 0_0) -> geq_2_out_aa2(X, 0_0)
if_geq_2_in_1_aa3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_aa2(s_11(X), s_11(Y))
if_geq_2_in_1_gg3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_gg2(s_11(X), s_11(Y))
geq_2_in_gg2(X, 0_0) -> geq_2_out_gg2(X, 0_0)
if_rem_3_in_5_agg3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_agg3(X, Y, X)
if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_agg3(X, Y, R)
if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_gag3(X, Y, R)
rem_3_in_gag3(X, Y, X) -> if_rem_3_in_4_gag3(X, Y, notZero_1_in_a1(Y))
if_rem_3_in_4_gag3(X, Y, notZero_1_out_a1(Y)) -> if_rem_3_in_5_gag3(X, Y, geq_2_in_gg2(X, Y))
if_rem_3_in_5_gag3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_gag3(X, Y, X)
REM_3_IN_GAG3(X, Y, R) -> IF_REM_3_IN_1_GAG4(X, Y, R, notZero_1_in_a1(Y))
REM_3_IN_GAG3(X, Y, R) -> NOTZERO_1_IN_A1(Y)
IF_REM_3_IN_1_GAG4(X, Y, R, notZero_1_out_a1(Y)) -> IF_REM_3_IN_2_GAG4(X, Y, R, sub_3_in_gga3(X, Y, Z))
IF_REM_3_IN_1_GAG4(X, Y, R, notZero_1_out_a1(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_aaa3(X, Y, Z))
SUB_3_IN_GGA3(s_11(X), s_11(Y), Z) -> SUB_3_IN_AAA3(X, Y, Z)
SUB_3_IN_AAA3(s_11(X), s_11(Y), Z) -> IF_SUB_3_IN_1_AAA4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
SUB_3_IN_AAA3(s_11(X), s_11(Y), Z) -> SUB_3_IN_AAA3(X, Y, Z)
IF_REM_3_IN_2_GAG4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> IF_REM_3_IN_3_GAG5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
IF_REM_3_IN_2_GAG4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> REM_3_IN_AGG3(Z, Y, R)
REM_3_IN_AGG3(X, Y, R) -> IF_REM_3_IN_1_AGG4(X, Y, R, notZero_1_in_g1(Y))
REM_3_IN_AGG3(X, Y, R) -> NOTZERO_1_IN_G1(Y)
IF_REM_3_IN_1_AGG4(X, Y, R, notZero_1_out_g1(Y)) -> IF_REM_3_IN_2_AGG4(X, Y, R, sub_3_in_aga3(X, Y, Z))
IF_REM_3_IN_1_AGG4(X, Y, R, notZero_1_out_g1(Y)) -> SUB_3_IN_AGA3(X, Y, Z)
SUB_3_IN_AGA3(s_11(X), s_11(Y), Z) -> IF_SUB_3_IN_1_AGA4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
SUB_3_IN_AGA3(s_11(X), s_11(Y), Z) -> SUB_3_IN_AAA3(X, Y, Z)
IF_REM_3_IN_2_AGG4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> IF_REM_3_IN_3_AGG5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
IF_REM_3_IN_2_AGG4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> REM_3_IN_AGG3(Z, Y, R)
REM_3_IN_AGG3(X, Y, X) -> IF_REM_3_IN_4_AGG3(X, Y, notZero_1_in_g1(Y))
REM_3_IN_AGG3(X, Y, X) -> NOTZERO_1_IN_G1(Y)
IF_REM_3_IN_4_AGG3(X, Y, notZero_1_out_g1(Y)) -> IF_REM_3_IN_5_AGG3(X, Y, geq_2_in_gg2(X, Y))
IF_REM_3_IN_4_AGG3(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_aa2(X, Y))
GEQ_2_IN_GG2(s_11(X), s_11(Y)) -> GEQ_2_IN_AA2(X, Y)
GEQ_2_IN_AA2(s_11(X), s_11(Y)) -> IF_GEQ_2_IN_1_AA3(X, Y, geq_2_in_aa2(X, Y))
GEQ_2_IN_AA2(s_11(X), s_11(Y)) -> GEQ_2_IN_AA2(X, Y)
REM_3_IN_GAG3(X, Y, X) -> IF_REM_3_IN_4_GAG3(X, Y, notZero_1_in_a1(Y))
REM_3_IN_GAG3(X, Y, X) -> NOTZERO_1_IN_A1(Y)
IF_REM_3_IN_4_GAG3(X, Y, notZero_1_out_a1(Y)) -> IF_REM_3_IN_5_GAG3(X, Y, geq_2_in_gg2(X, Y))
IF_REM_3_IN_4_GAG3(X, Y, notZero_1_out_a1(Y)) -> GEQ_2_IN_GG2(X, Y)
rem_3_in_gag3(X, Y, R) -> if_rem_3_in_1_gag4(X, Y, R, notZero_1_in_a1(Y))
notZero_1_in_a1(s_11(X)) -> notZero_1_out_a1(s_11(X))
if_rem_3_in_1_gag4(X, Y, R, notZero_1_out_a1(Y)) -> if_rem_3_in_2_gag4(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_aaa3(X, Y, Z))
sub_3_in_aaa3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aaa4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aaa3(X, 0_0, X) -> sub_3_out_aaa3(X, 0_0, X)
if_sub_3_in_1_aaa4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aaa3(s_11(X), s_11(Y), Z)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_rem_3_in_2_gag4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, R) -> if_rem_3_in_1_agg4(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_agg4(X, Y, R, notZero_1_out_g1(Y)) -> if_rem_3_in_2_agg4(X, Y, R, sub_3_in_aga3(X, Y, Z))
sub_3_in_aga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aga4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
if_sub_3_in_1_aga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aga3(s_11(X), s_11(Y), Z)
sub_3_in_aga3(X, 0_0, X) -> sub_3_out_aga3(X, 0_0, X)
if_rem_3_in_2_agg4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, X) -> if_rem_3_in_4_agg3(X, Y, notZero_1_in_g1(Y))
if_rem_3_in_4_agg3(X, Y, notZero_1_out_g1(Y)) -> if_rem_3_in_5_agg3(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_aa2(X, Y))
geq_2_in_aa2(s_11(X), s_11(Y)) -> if_geq_2_in_1_aa3(X, Y, geq_2_in_aa2(X, Y))
geq_2_in_aa2(X, 0_0) -> geq_2_out_aa2(X, 0_0)
if_geq_2_in_1_aa3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_aa2(s_11(X), s_11(Y))
if_geq_2_in_1_gg3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_gg2(s_11(X), s_11(Y))
geq_2_in_gg2(X, 0_0) -> geq_2_out_gg2(X, 0_0)
if_rem_3_in_5_agg3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_agg3(X, Y, X)
if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_agg3(X, Y, R)
if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_gag3(X, Y, R)
rem_3_in_gag3(X, Y, X) -> if_rem_3_in_4_gag3(X, Y, notZero_1_in_a1(Y))
if_rem_3_in_4_gag3(X, Y, notZero_1_out_a1(Y)) -> if_rem_3_in_5_gag3(X, Y, geq_2_in_gg2(X, Y))
if_rem_3_in_5_gag3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_gag3(X, Y, X)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
REM_3_IN_GAG3(X, Y, R) -> IF_REM_3_IN_1_GAG4(X, Y, R, notZero_1_in_a1(Y))
REM_3_IN_GAG3(X, Y, R) -> NOTZERO_1_IN_A1(Y)
IF_REM_3_IN_1_GAG4(X, Y, R, notZero_1_out_a1(Y)) -> IF_REM_3_IN_2_GAG4(X, Y, R, sub_3_in_gga3(X, Y, Z))
IF_REM_3_IN_1_GAG4(X, Y, R, notZero_1_out_a1(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_aaa3(X, Y, Z))
SUB_3_IN_GGA3(s_11(X), s_11(Y), Z) -> SUB_3_IN_AAA3(X, Y, Z)
SUB_3_IN_AAA3(s_11(X), s_11(Y), Z) -> IF_SUB_3_IN_1_AAA4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
SUB_3_IN_AAA3(s_11(X), s_11(Y), Z) -> SUB_3_IN_AAA3(X, Y, Z)
IF_REM_3_IN_2_GAG4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> IF_REM_3_IN_3_GAG5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
IF_REM_3_IN_2_GAG4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> REM_3_IN_AGG3(Z, Y, R)
REM_3_IN_AGG3(X, Y, R) -> IF_REM_3_IN_1_AGG4(X, Y, R, notZero_1_in_g1(Y))
REM_3_IN_AGG3(X, Y, R) -> NOTZERO_1_IN_G1(Y)
IF_REM_3_IN_1_AGG4(X, Y, R, notZero_1_out_g1(Y)) -> IF_REM_3_IN_2_AGG4(X, Y, R, sub_3_in_aga3(X, Y, Z))
IF_REM_3_IN_1_AGG4(X, Y, R, notZero_1_out_g1(Y)) -> SUB_3_IN_AGA3(X, Y, Z)
SUB_3_IN_AGA3(s_11(X), s_11(Y), Z) -> IF_SUB_3_IN_1_AGA4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
SUB_3_IN_AGA3(s_11(X), s_11(Y), Z) -> SUB_3_IN_AAA3(X, Y, Z)
IF_REM_3_IN_2_AGG4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> IF_REM_3_IN_3_AGG5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
IF_REM_3_IN_2_AGG4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> REM_3_IN_AGG3(Z, Y, R)
REM_3_IN_AGG3(X, Y, X) -> IF_REM_3_IN_4_AGG3(X, Y, notZero_1_in_g1(Y))
REM_3_IN_AGG3(X, Y, X) -> NOTZERO_1_IN_G1(Y)
IF_REM_3_IN_4_AGG3(X, Y, notZero_1_out_g1(Y)) -> IF_REM_3_IN_5_AGG3(X, Y, geq_2_in_gg2(X, Y))
IF_REM_3_IN_4_AGG3(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_aa2(X, Y))
GEQ_2_IN_GG2(s_11(X), s_11(Y)) -> GEQ_2_IN_AA2(X, Y)
GEQ_2_IN_AA2(s_11(X), s_11(Y)) -> IF_GEQ_2_IN_1_AA3(X, Y, geq_2_in_aa2(X, Y))
GEQ_2_IN_AA2(s_11(X), s_11(Y)) -> GEQ_2_IN_AA2(X, Y)
REM_3_IN_GAG3(X, Y, X) -> IF_REM_3_IN_4_GAG3(X, Y, notZero_1_in_a1(Y))
REM_3_IN_GAG3(X, Y, X) -> NOTZERO_1_IN_A1(Y)
IF_REM_3_IN_4_GAG3(X, Y, notZero_1_out_a1(Y)) -> IF_REM_3_IN_5_GAG3(X, Y, geq_2_in_gg2(X, Y))
IF_REM_3_IN_4_GAG3(X, Y, notZero_1_out_a1(Y)) -> GEQ_2_IN_GG2(X, Y)
rem_3_in_gag3(X, Y, R) -> if_rem_3_in_1_gag4(X, Y, R, notZero_1_in_a1(Y))
notZero_1_in_a1(s_11(X)) -> notZero_1_out_a1(s_11(X))
if_rem_3_in_1_gag4(X, Y, R, notZero_1_out_a1(Y)) -> if_rem_3_in_2_gag4(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_aaa3(X, Y, Z))
sub_3_in_aaa3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aaa4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aaa3(X, 0_0, X) -> sub_3_out_aaa3(X, 0_0, X)
if_sub_3_in_1_aaa4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aaa3(s_11(X), s_11(Y), Z)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_rem_3_in_2_gag4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, R) -> if_rem_3_in_1_agg4(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_agg4(X, Y, R, notZero_1_out_g1(Y)) -> if_rem_3_in_2_agg4(X, Y, R, sub_3_in_aga3(X, Y, Z))
sub_3_in_aga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aga4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
if_sub_3_in_1_aga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aga3(s_11(X), s_11(Y), Z)
sub_3_in_aga3(X, 0_0, X) -> sub_3_out_aga3(X, 0_0, X)
if_rem_3_in_2_agg4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, X) -> if_rem_3_in_4_agg3(X, Y, notZero_1_in_g1(Y))
if_rem_3_in_4_agg3(X, Y, notZero_1_out_g1(Y)) -> if_rem_3_in_5_agg3(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_aa2(X, Y))
geq_2_in_aa2(s_11(X), s_11(Y)) -> if_geq_2_in_1_aa3(X, Y, geq_2_in_aa2(X, Y))
geq_2_in_aa2(X, 0_0) -> geq_2_out_aa2(X, 0_0)
if_geq_2_in_1_aa3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_aa2(s_11(X), s_11(Y))
if_geq_2_in_1_gg3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_gg2(s_11(X), s_11(Y))
geq_2_in_gg2(X, 0_0) -> geq_2_out_gg2(X, 0_0)
if_rem_3_in_5_agg3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_agg3(X, Y, X)
if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_agg3(X, Y, R)
if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_gag3(X, Y, R)
rem_3_in_gag3(X, Y, X) -> if_rem_3_in_4_gag3(X, Y, notZero_1_in_a1(Y))
if_rem_3_in_4_gag3(X, Y, notZero_1_out_a1(Y)) -> if_rem_3_in_5_gag3(X, Y, geq_2_in_gg2(X, Y))
if_rem_3_in_5_gag3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_gag3(X, Y, X)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDP
GEQ_2_IN_AA2(s_11(X), s_11(Y)) -> GEQ_2_IN_AA2(X, Y)
rem_3_in_gag3(X, Y, R) -> if_rem_3_in_1_gag4(X, Y, R, notZero_1_in_a1(Y))
notZero_1_in_a1(s_11(X)) -> notZero_1_out_a1(s_11(X))
if_rem_3_in_1_gag4(X, Y, R, notZero_1_out_a1(Y)) -> if_rem_3_in_2_gag4(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_aaa3(X, Y, Z))
sub_3_in_aaa3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aaa4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aaa3(X, 0_0, X) -> sub_3_out_aaa3(X, 0_0, X)
if_sub_3_in_1_aaa4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aaa3(s_11(X), s_11(Y), Z)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_rem_3_in_2_gag4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, R) -> if_rem_3_in_1_agg4(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_agg4(X, Y, R, notZero_1_out_g1(Y)) -> if_rem_3_in_2_agg4(X, Y, R, sub_3_in_aga3(X, Y, Z))
sub_3_in_aga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aga4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
if_sub_3_in_1_aga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aga3(s_11(X), s_11(Y), Z)
sub_3_in_aga3(X, 0_0, X) -> sub_3_out_aga3(X, 0_0, X)
if_rem_3_in_2_agg4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, X) -> if_rem_3_in_4_agg3(X, Y, notZero_1_in_g1(Y))
if_rem_3_in_4_agg3(X, Y, notZero_1_out_g1(Y)) -> if_rem_3_in_5_agg3(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_aa2(X, Y))
geq_2_in_aa2(s_11(X), s_11(Y)) -> if_geq_2_in_1_aa3(X, Y, geq_2_in_aa2(X, Y))
geq_2_in_aa2(X, 0_0) -> geq_2_out_aa2(X, 0_0)
if_geq_2_in_1_aa3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_aa2(s_11(X), s_11(Y))
if_geq_2_in_1_gg3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_gg2(s_11(X), s_11(Y))
geq_2_in_gg2(X, 0_0) -> geq_2_out_gg2(X, 0_0)
if_rem_3_in_5_agg3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_agg3(X, Y, X)
if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_agg3(X, Y, R)
if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_gag3(X, Y, R)
rem_3_in_gag3(X, Y, X) -> if_rem_3_in_4_gag3(X, Y, notZero_1_in_a1(Y))
if_rem_3_in_4_gag3(X, Y, notZero_1_out_a1(Y)) -> if_rem_3_in_5_gag3(X, Y, geq_2_in_gg2(X, Y))
if_rem_3_in_5_gag3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_gag3(X, Y, X)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDP
↳ PiDP
GEQ_2_IN_AA2(s_11(X), s_11(Y)) -> GEQ_2_IN_AA2(X, Y)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
SUB_3_IN_AAA3(s_11(X), s_11(Y), Z) -> SUB_3_IN_AAA3(X, Y, Z)
rem_3_in_gag3(X, Y, R) -> if_rem_3_in_1_gag4(X, Y, R, notZero_1_in_a1(Y))
notZero_1_in_a1(s_11(X)) -> notZero_1_out_a1(s_11(X))
if_rem_3_in_1_gag4(X, Y, R, notZero_1_out_a1(Y)) -> if_rem_3_in_2_gag4(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_aaa3(X, Y, Z))
sub_3_in_aaa3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aaa4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aaa3(X, 0_0, X) -> sub_3_out_aaa3(X, 0_0, X)
if_sub_3_in_1_aaa4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aaa3(s_11(X), s_11(Y), Z)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_rem_3_in_2_gag4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, R) -> if_rem_3_in_1_agg4(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_agg4(X, Y, R, notZero_1_out_g1(Y)) -> if_rem_3_in_2_agg4(X, Y, R, sub_3_in_aga3(X, Y, Z))
sub_3_in_aga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aga4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
if_sub_3_in_1_aga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aga3(s_11(X), s_11(Y), Z)
sub_3_in_aga3(X, 0_0, X) -> sub_3_out_aga3(X, 0_0, X)
if_rem_3_in_2_agg4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, X) -> if_rem_3_in_4_agg3(X, Y, notZero_1_in_g1(Y))
if_rem_3_in_4_agg3(X, Y, notZero_1_out_g1(Y)) -> if_rem_3_in_5_agg3(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_aa2(X, Y))
geq_2_in_aa2(s_11(X), s_11(Y)) -> if_geq_2_in_1_aa3(X, Y, geq_2_in_aa2(X, Y))
geq_2_in_aa2(X, 0_0) -> geq_2_out_aa2(X, 0_0)
if_geq_2_in_1_aa3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_aa2(s_11(X), s_11(Y))
if_geq_2_in_1_gg3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_gg2(s_11(X), s_11(Y))
geq_2_in_gg2(X, 0_0) -> geq_2_out_gg2(X, 0_0)
if_rem_3_in_5_agg3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_agg3(X, Y, X)
if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_agg3(X, Y, R)
if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_gag3(X, Y, R)
rem_3_in_gag3(X, Y, X) -> if_rem_3_in_4_gag3(X, Y, notZero_1_in_a1(Y))
if_rem_3_in_4_gag3(X, Y, notZero_1_out_a1(Y)) -> if_rem_3_in_5_gag3(X, Y, geq_2_in_gg2(X, Y))
if_rem_3_in_5_gag3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_gag3(X, Y, X)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
REM_3_IN_AGG3(X, Y, R) -> IF_REM_3_IN_1_AGG4(X, Y, R, notZero_1_in_g1(Y))
IF_REM_3_IN_2_AGG4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> REM_3_IN_AGG3(Z, Y, R)
IF_REM_3_IN_1_AGG4(X, Y, R, notZero_1_out_g1(Y)) -> IF_REM_3_IN_2_AGG4(X, Y, R, sub_3_in_aga3(X, Y, Z))
rem_3_in_gag3(X, Y, R) -> if_rem_3_in_1_gag4(X, Y, R, notZero_1_in_a1(Y))
notZero_1_in_a1(s_11(X)) -> notZero_1_out_a1(s_11(X))
if_rem_3_in_1_gag4(X, Y, R, notZero_1_out_a1(Y)) -> if_rem_3_in_2_gag4(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_aaa3(X, Y, Z))
sub_3_in_aaa3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aaa4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aaa3(X, 0_0, X) -> sub_3_out_aaa3(X, 0_0, X)
if_sub_3_in_1_aaa4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aaa3(s_11(X), s_11(Y), Z)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_rem_3_in_2_gag4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, R) -> if_rem_3_in_1_agg4(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_agg4(X, Y, R, notZero_1_out_g1(Y)) -> if_rem_3_in_2_agg4(X, Y, R, sub_3_in_aga3(X, Y, Z))
sub_3_in_aga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aga4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
if_sub_3_in_1_aga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aga3(s_11(X), s_11(Y), Z)
sub_3_in_aga3(X, 0_0, X) -> sub_3_out_aga3(X, 0_0, X)
if_rem_3_in_2_agg4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, X) -> if_rem_3_in_4_agg3(X, Y, notZero_1_in_g1(Y))
if_rem_3_in_4_agg3(X, Y, notZero_1_out_g1(Y)) -> if_rem_3_in_5_agg3(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_aa2(X, Y))
geq_2_in_aa2(s_11(X), s_11(Y)) -> if_geq_2_in_1_aa3(X, Y, geq_2_in_aa2(X, Y))
geq_2_in_aa2(X, 0_0) -> geq_2_out_aa2(X, 0_0)
if_geq_2_in_1_aa3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_aa2(s_11(X), s_11(Y))
if_geq_2_in_1_gg3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_gg2(s_11(X), s_11(Y))
geq_2_in_gg2(X, 0_0) -> geq_2_out_gg2(X, 0_0)
if_rem_3_in_5_agg3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_agg3(X, Y, X)
if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_agg3(X, Y, R)
if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_gag3(X, Y, R)
rem_3_in_gag3(X, Y, X) -> if_rem_3_in_4_gag3(X, Y, notZero_1_in_a1(Y))
if_rem_3_in_4_gag3(X, Y, notZero_1_out_a1(Y)) -> if_rem_3_in_5_gag3(X, Y, geq_2_in_gg2(X, Y))
if_rem_3_in_5_gag3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_gag3(X, Y, X)