Left Termination of the query pattern div(b,b,f) w.r.t. the given Prolog program could successfully be proven:



↳ PROLOG
  ↳ PrologToPiTRSProof

div3(X, s1(Y), Z) :- divs3(X, Y, Z).
divs3(00, Y, 00).
divs3(s1(X), Y, 00) :- lss2(X, Y).
divs3(s1(X), Y, s1(Z)) :- sub3(X, Y, R), divs3(R, Y, Z).
lss2(s1(X), s1(Y)) :- lss2(X, Y).
lss2(00, s1(Y)).
sub3(s1(X), s1(Y), Z) :- sub3(X, Y, Z).
sub3(X, 00, X).


With regard to the inferred argument filtering the predicates were used in the following modes:
div3: (b,b,f)
div_s3: (b,b,f)
lss2: (b,b)
sub3: (b,b,f)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:


div_3_in_gga3(X, s_11(Y), Z) -> if_div_3_in_1_gga4(X, Y, Z, div_s_3_in_gga3(X, Y, Z))
div_s_3_in_gga3(0_0, Y, 0_0) -> div_s_3_out_gga3(0_0, Y, 0_0)
div_s_3_in_gga3(s_11(X), Y, 0_0) -> if_div_s_3_in_1_gga3(X, Y, lss_2_in_gg2(X, Y))
lss_2_in_gg2(s_11(X), s_11(Y)) -> if_lss_2_in_1_gg3(X, Y, lss_2_in_gg2(X, Y))
lss_2_in_gg2(0_0, s_11(Y)) -> lss_2_out_gg2(0_0, s_11(Y))
if_lss_2_in_1_gg3(X, Y, lss_2_out_gg2(X, Y)) -> lss_2_out_gg2(s_11(X), s_11(Y))
if_div_s_3_in_1_gga3(X, Y, lss_2_out_gg2(X, Y)) -> div_s_3_out_gga3(s_11(X), Y, 0_0)
div_s_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_div_s_3_in_2_gga4(X, Y, Z, sub_3_in_gga3(X, Y, R))
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_div_s_3_in_2_gga4(X, Y, Z, sub_3_out_gga3(X, Y, R)) -> if_div_s_3_in_3_gga5(X, Y, Z, R, div_s_3_in_gga3(R, Y, Z))
if_div_s_3_in_3_gga5(X, Y, Z, R, div_s_3_out_gga3(R, Y, Z)) -> div_s_3_out_gga3(s_11(X), Y, s_11(Z))
if_div_3_in_1_gga4(X, Y, Z, div_s_3_out_gga3(X, Y, Z)) -> div_3_out_gga3(X, s_11(Y), Z)

The argument filtering Pi contains the following mapping:
div_3_in_gga3(x1, x2, x3)  =  div_3_in_gga2(x1, x2)
s_11(x1)  =  s_11(x1)
0_0  =  0_0
if_div_3_in_1_gga4(x1, x2, x3, x4)  =  if_div_3_in_1_gga1(x4)
div_s_3_in_gga3(x1, x2, x3)  =  div_s_3_in_gga2(x1, x2)
div_s_3_out_gga3(x1, x2, x3)  =  div_s_3_out_gga1(x3)
if_div_s_3_in_1_gga3(x1, x2, x3)  =  if_div_s_3_in_1_gga1(x3)
lss_2_in_gg2(x1, x2)  =  lss_2_in_gg2(x1, x2)
if_lss_2_in_1_gg3(x1, x2, x3)  =  if_lss_2_in_1_gg1(x3)
lss_2_out_gg2(x1, x2)  =  lss_2_out_gg
if_div_s_3_in_2_gga4(x1, x2, x3, x4)  =  if_div_s_3_in_2_gga2(x2, x4)
sub_3_in_gga3(x1, x2, x3)  =  sub_3_in_gga2(x1, x2)
if_sub_3_in_1_gga4(x1, x2, x3, x4)  =  if_sub_3_in_1_gga1(x4)
sub_3_out_gga3(x1, x2, x3)  =  sub_3_out_gga1(x3)
if_div_s_3_in_3_gga5(x1, x2, x3, x4, x5)  =  if_div_s_3_in_3_gga1(x5)
div_3_out_gga3(x1, x2, x3)  =  div_3_out_gga1(x3)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof

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

div_3_in_gga3(X, s_11(Y), Z) -> if_div_3_in_1_gga4(X, Y, Z, div_s_3_in_gga3(X, Y, Z))
div_s_3_in_gga3(0_0, Y, 0_0) -> div_s_3_out_gga3(0_0, Y, 0_0)
div_s_3_in_gga3(s_11(X), Y, 0_0) -> if_div_s_3_in_1_gga3(X, Y, lss_2_in_gg2(X, Y))
lss_2_in_gg2(s_11(X), s_11(Y)) -> if_lss_2_in_1_gg3(X, Y, lss_2_in_gg2(X, Y))
lss_2_in_gg2(0_0, s_11(Y)) -> lss_2_out_gg2(0_0, s_11(Y))
if_lss_2_in_1_gg3(X, Y, lss_2_out_gg2(X, Y)) -> lss_2_out_gg2(s_11(X), s_11(Y))
if_div_s_3_in_1_gga3(X, Y, lss_2_out_gg2(X, Y)) -> div_s_3_out_gga3(s_11(X), Y, 0_0)
div_s_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_div_s_3_in_2_gga4(X, Y, Z, sub_3_in_gga3(X, Y, R))
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_div_s_3_in_2_gga4(X, Y, Z, sub_3_out_gga3(X, Y, R)) -> if_div_s_3_in_3_gga5(X, Y, Z, R, div_s_3_in_gga3(R, Y, Z))
if_div_s_3_in_3_gga5(X, Y, Z, R, div_s_3_out_gga3(R, Y, Z)) -> div_s_3_out_gga3(s_11(X), Y, s_11(Z))
if_div_3_in_1_gga4(X, Y, Z, div_s_3_out_gga3(X, Y, Z)) -> div_3_out_gga3(X, s_11(Y), Z)

The argument filtering Pi contains the following mapping:
div_3_in_gga3(x1, x2, x3)  =  div_3_in_gga2(x1, x2)
s_11(x1)  =  s_11(x1)
0_0  =  0_0
if_div_3_in_1_gga4(x1, x2, x3, x4)  =  if_div_3_in_1_gga1(x4)
div_s_3_in_gga3(x1, x2, x3)  =  div_s_3_in_gga2(x1, x2)
div_s_3_out_gga3(x1, x2, x3)  =  div_s_3_out_gga1(x3)
if_div_s_3_in_1_gga3(x1, x2, x3)  =  if_div_s_3_in_1_gga1(x3)
lss_2_in_gg2(x1, x2)  =  lss_2_in_gg2(x1, x2)
if_lss_2_in_1_gg3(x1, x2, x3)  =  if_lss_2_in_1_gg1(x3)
lss_2_out_gg2(x1, x2)  =  lss_2_out_gg
if_div_s_3_in_2_gga4(x1, x2, x3, x4)  =  if_div_s_3_in_2_gga2(x2, x4)
sub_3_in_gga3(x1, x2, x3)  =  sub_3_in_gga2(x1, x2)
if_sub_3_in_1_gga4(x1, x2, x3, x4)  =  if_sub_3_in_1_gga1(x4)
sub_3_out_gga3(x1, x2, x3)  =  sub_3_out_gga1(x3)
if_div_s_3_in_3_gga5(x1, x2, x3, x4, x5)  =  if_div_s_3_in_3_gga1(x5)
div_3_out_gga3(x1, x2, x3)  =  div_3_out_gga1(x3)


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

DIV_3_IN_GGA3(X, s_11(Y), Z) -> IF_DIV_3_IN_1_GGA4(X, Y, Z, div_s_3_in_gga3(X, Y, Z))
DIV_3_IN_GGA3(X, s_11(Y), Z) -> DIV_S_3_IN_GGA3(X, Y, Z)
DIV_S_3_IN_GGA3(s_11(X), Y, 0_0) -> IF_DIV_S_3_IN_1_GGA3(X, Y, lss_2_in_gg2(X, Y))
DIV_S_3_IN_GGA3(s_11(X), Y, 0_0) -> LSS_2_IN_GG2(X, Y)
LSS_2_IN_GG2(s_11(X), s_11(Y)) -> IF_LSS_2_IN_1_GG3(X, Y, lss_2_in_gg2(X, Y))
LSS_2_IN_GG2(s_11(X), s_11(Y)) -> LSS_2_IN_GG2(X, Y)
DIV_S_3_IN_GGA3(s_11(X), Y, s_11(Z)) -> IF_DIV_S_3_IN_2_GGA4(X, Y, Z, sub_3_in_gga3(X, Y, R))
DIV_S_3_IN_GGA3(s_11(X), Y, s_11(Z)) -> SUB_3_IN_GGA3(X, Y, R)
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_DIV_S_3_IN_2_GGA4(X, Y, Z, sub_3_out_gga3(X, Y, R)) -> IF_DIV_S_3_IN_3_GGA5(X, Y, Z, R, div_s_3_in_gga3(R, Y, Z))
IF_DIV_S_3_IN_2_GGA4(X, Y, Z, sub_3_out_gga3(X, Y, R)) -> DIV_S_3_IN_GGA3(R, Y, Z)

The TRS R consists of the following rules:

div_3_in_gga3(X, s_11(Y), Z) -> if_div_3_in_1_gga4(X, Y, Z, div_s_3_in_gga3(X, Y, Z))
div_s_3_in_gga3(0_0, Y, 0_0) -> div_s_3_out_gga3(0_0, Y, 0_0)
div_s_3_in_gga3(s_11(X), Y, 0_0) -> if_div_s_3_in_1_gga3(X, Y, lss_2_in_gg2(X, Y))
lss_2_in_gg2(s_11(X), s_11(Y)) -> if_lss_2_in_1_gg3(X, Y, lss_2_in_gg2(X, Y))
lss_2_in_gg2(0_0, s_11(Y)) -> lss_2_out_gg2(0_0, s_11(Y))
if_lss_2_in_1_gg3(X, Y, lss_2_out_gg2(X, Y)) -> lss_2_out_gg2(s_11(X), s_11(Y))
if_div_s_3_in_1_gga3(X, Y, lss_2_out_gg2(X, Y)) -> div_s_3_out_gga3(s_11(X), Y, 0_0)
div_s_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_div_s_3_in_2_gga4(X, Y, Z, sub_3_in_gga3(X, Y, R))
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_div_s_3_in_2_gga4(X, Y, Z, sub_3_out_gga3(X, Y, R)) -> if_div_s_3_in_3_gga5(X, Y, Z, R, div_s_3_in_gga3(R, Y, Z))
if_div_s_3_in_3_gga5(X, Y, Z, R, div_s_3_out_gga3(R, Y, Z)) -> div_s_3_out_gga3(s_11(X), Y, s_11(Z))
if_div_3_in_1_gga4(X, Y, Z, div_s_3_out_gga3(X, Y, Z)) -> div_3_out_gga3(X, s_11(Y), Z)

The argument filtering Pi contains the following mapping:
div_3_in_gga3(x1, x2, x3)  =  div_3_in_gga2(x1, x2)
s_11(x1)  =  s_11(x1)
0_0  =  0_0
if_div_3_in_1_gga4(x1, x2, x3, x4)  =  if_div_3_in_1_gga1(x4)
div_s_3_in_gga3(x1, x2, x3)  =  div_s_3_in_gga2(x1, x2)
div_s_3_out_gga3(x1, x2, x3)  =  div_s_3_out_gga1(x3)
if_div_s_3_in_1_gga3(x1, x2, x3)  =  if_div_s_3_in_1_gga1(x3)
lss_2_in_gg2(x1, x2)  =  lss_2_in_gg2(x1, x2)
if_lss_2_in_1_gg3(x1, x2, x3)  =  if_lss_2_in_1_gg1(x3)
lss_2_out_gg2(x1, x2)  =  lss_2_out_gg
if_div_s_3_in_2_gga4(x1, x2, x3, x4)  =  if_div_s_3_in_2_gga2(x2, x4)
sub_3_in_gga3(x1, x2, x3)  =  sub_3_in_gga2(x1, x2)
if_sub_3_in_1_gga4(x1, x2, x3, x4)  =  if_sub_3_in_1_gga1(x4)
sub_3_out_gga3(x1, x2, x3)  =  sub_3_out_gga1(x3)
if_div_s_3_in_3_gga5(x1, x2, x3, x4, x5)  =  if_div_s_3_in_3_gga1(x5)
div_3_out_gga3(x1, x2, x3)  =  div_3_out_gga1(x3)
DIV_3_IN_GGA3(x1, x2, x3)  =  DIV_3_IN_GGA2(x1, x2)
IF_LSS_2_IN_1_GG3(x1, x2, x3)  =  IF_LSS_2_IN_1_GG1(x3)
IF_DIV_S_3_IN_3_GGA5(x1, x2, x3, x4, x5)  =  IF_DIV_S_3_IN_3_GGA1(x5)
IF_SUB_3_IN_1_GGA4(x1, x2, x3, x4)  =  IF_SUB_3_IN_1_GGA1(x4)
IF_DIV_3_IN_1_GGA4(x1, x2, x3, x4)  =  IF_DIV_3_IN_1_GGA1(x4)
IF_DIV_S_3_IN_1_GGA3(x1, x2, x3)  =  IF_DIV_S_3_IN_1_GGA1(x3)
DIV_S_3_IN_GGA3(x1, x2, x3)  =  DIV_S_3_IN_GGA2(x1, x2)
LSS_2_IN_GG2(x1, x2)  =  LSS_2_IN_GG2(x1, x2)
SUB_3_IN_GGA3(x1, x2, x3)  =  SUB_3_IN_GGA2(x1, x2)
IF_DIV_S_3_IN_2_GGA4(x1, x2, x3, x4)  =  IF_DIV_S_3_IN_2_GGA2(x2, x4)

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

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof

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

DIV_3_IN_GGA3(X, s_11(Y), Z) -> IF_DIV_3_IN_1_GGA4(X, Y, Z, div_s_3_in_gga3(X, Y, Z))
DIV_3_IN_GGA3(X, s_11(Y), Z) -> DIV_S_3_IN_GGA3(X, Y, Z)
DIV_S_3_IN_GGA3(s_11(X), Y, 0_0) -> IF_DIV_S_3_IN_1_GGA3(X, Y, lss_2_in_gg2(X, Y))
DIV_S_3_IN_GGA3(s_11(X), Y, 0_0) -> LSS_2_IN_GG2(X, Y)
LSS_2_IN_GG2(s_11(X), s_11(Y)) -> IF_LSS_2_IN_1_GG3(X, Y, lss_2_in_gg2(X, Y))
LSS_2_IN_GG2(s_11(X), s_11(Y)) -> LSS_2_IN_GG2(X, Y)
DIV_S_3_IN_GGA3(s_11(X), Y, s_11(Z)) -> IF_DIV_S_3_IN_2_GGA4(X, Y, Z, sub_3_in_gga3(X, Y, R))
DIV_S_3_IN_GGA3(s_11(X), Y, s_11(Z)) -> SUB_3_IN_GGA3(X, Y, R)
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_DIV_S_3_IN_2_GGA4(X, Y, Z, sub_3_out_gga3(X, Y, R)) -> IF_DIV_S_3_IN_3_GGA5(X, Y, Z, R, div_s_3_in_gga3(R, Y, Z))
IF_DIV_S_3_IN_2_GGA4(X, Y, Z, sub_3_out_gga3(X, Y, R)) -> DIV_S_3_IN_GGA3(R, Y, Z)

The TRS R consists of the following rules:

div_3_in_gga3(X, s_11(Y), Z) -> if_div_3_in_1_gga4(X, Y, Z, div_s_3_in_gga3(X, Y, Z))
div_s_3_in_gga3(0_0, Y, 0_0) -> div_s_3_out_gga3(0_0, Y, 0_0)
div_s_3_in_gga3(s_11(X), Y, 0_0) -> if_div_s_3_in_1_gga3(X, Y, lss_2_in_gg2(X, Y))
lss_2_in_gg2(s_11(X), s_11(Y)) -> if_lss_2_in_1_gg3(X, Y, lss_2_in_gg2(X, Y))
lss_2_in_gg2(0_0, s_11(Y)) -> lss_2_out_gg2(0_0, s_11(Y))
if_lss_2_in_1_gg3(X, Y, lss_2_out_gg2(X, Y)) -> lss_2_out_gg2(s_11(X), s_11(Y))
if_div_s_3_in_1_gga3(X, Y, lss_2_out_gg2(X, Y)) -> div_s_3_out_gga3(s_11(X), Y, 0_0)
div_s_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_div_s_3_in_2_gga4(X, Y, Z, sub_3_in_gga3(X, Y, R))
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_div_s_3_in_2_gga4(X, Y, Z, sub_3_out_gga3(X, Y, R)) -> if_div_s_3_in_3_gga5(X, Y, Z, R, div_s_3_in_gga3(R, Y, Z))
if_div_s_3_in_3_gga5(X, Y, Z, R, div_s_3_out_gga3(R, Y, Z)) -> div_s_3_out_gga3(s_11(X), Y, s_11(Z))
if_div_3_in_1_gga4(X, Y, Z, div_s_3_out_gga3(X, Y, Z)) -> div_3_out_gga3(X, s_11(Y), Z)

The argument filtering Pi contains the following mapping:
div_3_in_gga3(x1, x2, x3)  =  div_3_in_gga2(x1, x2)
s_11(x1)  =  s_11(x1)
0_0  =  0_0
if_div_3_in_1_gga4(x1, x2, x3, x4)  =  if_div_3_in_1_gga1(x4)
div_s_3_in_gga3(x1, x2, x3)  =  div_s_3_in_gga2(x1, x2)
div_s_3_out_gga3(x1, x2, x3)  =  div_s_3_out_gga1(x3)
if_div_s_3_in_1_gga3(x1, x2, x3)  =  if_div_s_3_in_1_gga1(x3)
lss_2_in_gg2(x1, x2)  =  lss_2_in_gg2(x1, x2)
if_lss_2_in_1_gg3(x1, x2, x3)  =  if_lss_2_in_1_gg1(x3)
lss_2_out_gg2(x1, x2)  =  lss_2_out_gg
if_div_s_3_in_2_gga4(x1, x2, x3, x4)  =  if_div_s_3_in_2_gga2(x2, x4)
sub_3_in_gga3(x1, x2, x3)  =  sub_3_in_gga2(x1, x2)
if_sub_3_in_1_gga4(x1, x2, x3, x4)  =  if_sub_3_in_1_gga1(x4)
sub_3_out_gga3(x1, x2, x3)  =  sub_3_out_gga1(x3)
if_div_s_3_in_3_gga5(x1, x2, x3, x4, x5)  =  if_div_s_3_in_3_gga1(x5)
div_3_out_gga3(x1, x2, x3)  =  div_3_out_gga1(x3)
DIV_3_IN_GGA3(x1, x2, x3)  =  DIV_3_IN_GGA2(x1, x2)
IF_LSS_2_IN_1_GG3(x1, x2, x3)  =  IF_LSS_2_IN_1_GG1(x3)
IF_DIV_S_3_IN_3_GGA5(x1, x2, x3, x4, x5)  =  IF_DIV_S_3_IN_3_GGA1(x5)
IF_SUB_3_IN_1_GGA4(x1, x2, x3, x4)  =  IF_SUB_3_IN_1_GGA1(x4)
IF_DIV_3_IN_1_GGA4(x1, x2, x3, x4)  =  IF_DIV_3_IN_1_GGA1(x4)
IF_DIV_S_3_IN_1_GGA3(x1, x2, x3)  =  IF_DIV_S_3_IN_1_GGA1(x3)
DIV_S_3_IN_GGA3(x1, x2, x3)  =  DIV_S_3_IN_GGA2(x1, x2)
LSS_2_IN_GG2(x1, x2)  =  LSS_2_IN_GG2(x1, x2)
SUB_3_IN_GGA3(x1, x2, x3)  =  SUB_3_IN_GGA2(x1, x2)
IF_DIV_S_3_IN_2_GGA4(x1, x2, x3, x4)  =  IF_DIV_S_3_IN_2_GGA2(x2, x4)

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

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP

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

SUB_3_IN_GGA3(s_11(X), s_11(Y), Z) -> SUB_3_IN_GGA3(X, Y, Z)

The TRS R consists of the following rules:

div_3_in_gga3(X, s_11(Y), Z) -> if_div_3_in_1_gga4(X, Y, Z, div_s_3_in_gga3(X, Y, Z))
div_s_3_in_gga3(0_0, Y, 0_0) -> div_s_3_out_gga3(0_0, Y, 0_0)
div_s_3_in_gga3(s_11(X), Y, 0_0) -> if_div_s_3_in_1_gga3(X, Y, lss_2_in_gg2(X, Y))
lss_2_in_gg2(s_11(X), s_11(Y)) -> if_lss_2_in_1_gg3(X, Y, lss_2_in_gg2(X, Y))
lss_2_in_gg2(0_0, s_11(Y)) -> lss_2_out_gg2(0_0, s_11(Y))
if_lss_2_in_1_gg3(X, Y, lss_2_out_gg2(X, Y)) -> lss_2_out_gg2(s_11(X), s_11(Y))
if_div_s_3_in_1_gga3(X, Y, lss_2_out_gg2(X, Y)) -> div_s_3_out_gga3(s_11(X), Y, 0_0)
div_s_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_div_s_3_in_2_gga4(X, Y, Z, sub_3_in_gga3(X, Y, R))
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_div_s_3_in_2_gga4(X, Y, Z, sub_3_out_gga3(X, Y, R)) -> if_div_s_3_in_3_gga5(X, Y, Z, R, div_s_3_in_gga3(R, Y, Z))
if_div_s_3_in_3_gga5(X, Y, Z, R, div_s_3_out_gga3(R, Y, Z)) -> div_s_3_out_gga3(s_11(X), Y, s_11(Z))
if_div_3_in_1_gga4(X, Y, Z, div_s_3_out_gga3(X, Y, Z)) -> div_3_out_gga3(X, s_11(Y), Z)

The argument filtering Pi contains the following mapping:
div_3_in_gga3(x1, x2, x3)  =  div_3_in_gga2(x1, x2)
s_11(x1)  =  s_11(x1)
0_0  =  0_0
if_div_3_in_1_gga4(x1, x2, x3, x4)  =  if_div_3_in_1_gga1(x4)
div_s_3_in_gga3(x1, x2, x3)  =  div_s_3_in_gga2(x1, x2)
div_s_3_out_gga3(x1, x2, x3)  =  div_s_3_out_gga1(x3)
if_div_s_3_in_1_gga3(x1, x2, x3)  =  if_div_s_3_in_1_gga1(x3)
lss_2_in_gg2(x1, x2)  =  lss_2_in_gg2(x1, x2)
if_lss_2_in_1_gg3(x1, x2, x3)  =  if_lss_2_in_1_gg1(x3)
lss_2_out_gg2(x1, x2)  =  lss_2_out_gg
if_div_s_3_in_2_gga4(x1, x2, x3, x4)  =  if_div_s_3_in_2_gga2(x2, x4)
sub_3_in_gga3(x1, x2, x3)  =  sub_3_in_gga2(x1, x2)
if_sub_3_in_1_gga4(x1, x2, x3, x4)  =  if_sub_3_in_1_gga1(x4)
sub_3_out_gga3(x1, x2, x3)  =  sub_3_out_gga1(x3)
if_div_s_3_in_3_gga5(x1, x2, x3, x4, x5)  =  if_div_s_3_in_3_gga1(x5)
div_3_out_gga3(x1, x2, x3)  =  div_3_out_gga1(x3)
SUB_3_IN_GGA3(x1, x2, x3)  =  SUB_3_IN_GGA2(x1, x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting we can delete all non-usable rules from R.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP

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

SUB_3_IN_GGA3(s_11(X), s_11(Y), Z) -> SUB_3_IN_GGA3(X, Y, Z)

R is empty.
The argument filtering Pi contains the following mapping:
s_11(x1)  =  s_11(x1)
SUB_3_IN_GGA3(x1, x2, x3)  =  SUB_3_IN_GGA2(x1, x2)

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

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
              ↳ PiDP

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

SUB_3_IN_GGA2(s_11(X), s_11(Y)) -> SUB_3_IN_GGA2(X, Y)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {SUB_3_IN_GGA2}.
By using the subterm criterion together with the size-change analysis we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP

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

LSS_2_IN_GG2(s_11(X), s_11(Y)) -> LSS_2_IN_GG2(X, Y)

The TRS R consists of the following rules:

div_3_in_gga3(X, s_11(Y), Z) -> if_div_3_in_1_gga4(X, Y, Z, div_s_3_in_gga3(X, Y, Z))
div_s_3_in_gga3(0_0, Y, 0_0) -> div_s_3_out_gga3(0_0, Y, 0_0)
div_s_3_in_gga3(s_11(X), Y, 0_0) -> if_div_s_3_in_1_gga3(X, Y, lss_2_in_gg2(X, Y))
lss_2_in_gg2(s_11(X), s_11(Y)) -> if_lss_2_in_1_gg3(X, Y, lss_2_in_gg2(X, Y))
lss_2_in_gg2(0_0, s_11(Y)) -> lss_2_out_gg2(0_0, s_11(Y))
if_lss_2_in_1_gg3(X, Y, lss_2_out_gg2(X, Y)) -> lss_2_out_gg2(s_11(X), s_11(Y))
if_div_s_3_in_1_gga3(X, Y, lss_2_out_gg2(X, Y)) -> div_s_3_out_gga3(s_11(X), Y, 0_0)
div_s_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_div_s_3_in_2_gga4(X, Y, Z, sub_3_in_gga3(X, Y, R))
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_div_s_3_in_2_gga4(X, Y, Z, sub_3_out_gga3(X, Y, R)) -> if_div_s_3_in_3_gga5(X, Y, Z, R, div_s_3_in_gga3(R, Y, Z))
if_div_s_3_in_3_gga5(X, Y, Z, R, div_s_3_out_gga3(R, Y, Z)) -> div_s_3_out_gga3(s_11(X), Y, s_11(Z))
if_div_3_in_1_gga4(X, Y, Z, div_s_3_out_gga3(X, Y, Z)) -> div_3_out_gga3(X, s_11(Y), Z)

The argument filtering Pi contains the following mapping:
div_3_in_gga3(x1, x2, x3)  =  div_3_in_gga2(x1, x2)
s_11(x1)  =  s_11(x1)
0_0  =  0_0
if_div_3_in_1_gga4(x1, x2, x3, x4)  =  if_div_3_in_1_gga1(x4)
div_s_3_in_gga3(x1, x2, x3)  =  div_s_3_in_gga2(x1, x2)
div_s_3_out_gga3(x1, x2, x3)  =  div_s_3_out_gga1(x3)
if_div_s_3_in_1_gga3(x1, x2, x3)  =  if_div_s_3_in_1_gga1(x3)
lss_2_in_gg2(x1, x2)  =  lss_2_in_gg2(x1, x2)
if_lss_2_in_1_gg3(x1, x2, x3)  =  if_lss_2_in_1_gg1(x3)
lss_2_out_gg2(x1, x2)  =  lss_2_out_gg
if_div_s_3_in_2_gga4(x1, x2, x3, x4)  =  if_div_s_3_in_2_gga2(x2, x4)
sub_3_in_gga3(x1, x2, x3)  =  sub_3_in_gga2(x1, x2)
if_sub_3_in_1_gga4(x1, x2, x3, x4)  =  if_sub_3_in_1_gga1(x4)
sub_3_out_gga3(x1, x2, x3)  =  sub_3_out_gga1(x3)
if_div_s_3_in_3_gga5(x1, x2, x3, x4, x5)  =  if_div_s_3_in_3_gga1(x5)
div_3_out_gga3(x1, x2, x3)  =  div_3_out_gga1(x3)
LSS_2_IN_GG2(x1, x2)  =  LSS_2_IN_GG2(x1, x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting we can delete all non-usable rules from R.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP

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

LSS_2_IN_GG2(s_11(X), s_11(Y)) -> LSS_2_IN_GG2(X, Y)

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

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP

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

LSS_2_IN_GG2(s_11(X), s_11(Y)) -> LSS_2_IN_GG2(X, Y)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {LSS_2_IN_GG2}.
By using the subterm criterion together with the size-change analysis we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof

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

DIV_S_3_IN_GGA3(s_11(X), Y, s_11(Z)) -> IF_DIV_S_3_IN_2_GGA4(X, Y, Z, sub_3_in_gga3(X, Y, R))
IF_DIV_S_3_IN_2_GGA4(X, Y, Z, sub_3_out_gga3(X, Y, R)) -> DIV_S_3_IN_GGA3(R, Y, Z)

The TRS R consists of the following rules:

div_3_in_gga3(X, s_11(Y), Z) -> if_div_3_in_1_gga4(X, Y, Z, div_s_3_in_gga3(X, Y, Z))
div_s_3_in_gga3(0_0, Y, 0_0) -> div_s_3_out_gga3(0_0, Y, 0_0)
div_s_3_in_gga3(s_11(X), Y, 0_0) -> if_div_s_3_in_1_gga3(X, Y, lss_2_in_gg2(X, Y))
lss_2_in_gg2(s_11(X), s_11(Y)) -> if_lss_2_in_1_gg3(X, Y, lss_2_in_gg2(X, Y))
lss_2_in_gg2(0_0, s_11(Y)) -> lss_2_out_gg2(0_0, s_11(Y))
if_lss_2_in_1_gg3(X, Y, lss_2_out_gg2(X, Y)) -> lss_2_out_gg2(s_11(X), s_11(Y))
if_div_s_3_in_1_gga3(X, Y, lss_2_out_gg2(X, Y)) -> div_s_3_out_gga3(s_11(X), Y, 0_0)
div_s_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_div_s_3_in_2_gga4(X, Y, Z, sub_3_in_gga3(X, Y, R))
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_div_s_3_in_2_gga4(X, Y, Z, sub_3_out_gga3(X, Y, R)) -> if_div_s_3_in_3_gga5(X, Y, Z, R, div_s_3_in_gga3(R, Y, Z))
if_div_s_3_in_3_gga5(X, Y, Z, R, div_s_3_out_gga3(R, Y, Z)) -> div_s_3_out_gga3(s_11(X), Y, s_11(Z))
if_div_3_in_1_gga4(X, Y, Z, div_s_3_out_gga3(X, Y, Z)) -> div_3_out_gga3(X, s_11(Y), Z)

The argument filtering Pi contains the following mapping:
div_3_in_gga3(x1, x2, x3)  =  div_3_in_gga2(x1, x2)
s_11(x1)  =  s_11(x1)
0_0  =  0_0
if_div_3_in_1_gga4(x1, x2, x3, x4)  =  if_div_3_in_1_gga1(x4)
div_s_3_in_gga3(x1, x2, x3)  =  div_s_3_in_gga2(x1, x2)
div_s_3_out_gga3(x1, x2, x3)  =  div_s_3_out_gga1(x3)
if_div_s_3_in_1_gga3(x1, x2, x3)  =  if_div_s_3_in_1_gga1(x3)
lss_2_in_gg2(x1, x2)  =  lss_2_in_gg2(x1, x2)
if_lss_2_in_1_gg3(x1, x2, x3)  =  if_lss_2_in_1_gg1(x3)
lss_2_out_gg2(x1, x2)  =  lss_2_out_gg
if_div_s_3_in_2_gga4(x1, x2, x3, x4)  =  if_div_s_3_in_2_gga2(x2, x4)
sub_3_in_gga3(x1, x2, x3)  =  sub_3_in_gga2(x1, x2)
if_sub_3_in_1_gga4(x1, x2, x3, x4)  =  if_sub_3_in_1_gga1(x4)
sub_3_out_gga3(x1, x2, x3)  =  sub_3_out_gga1(x3)
if_div_s_3_in_3_gga5(x1, x2, x3, x4, x5)  =  if_div_s_3_in_3_gga1(x5)
div_3_out_gga3(x1, x2, x3)  =  div_3_out_gga1(x3)
DIV_S_3_IN_GGA3(x1, x2, x3)  =  DIV_S_3_IN_GGA2(x1, x2)
IF_DIV_S_3_IN_2_GGA4(x1, x2, x3, x4)  =  IF_DIV_S_3_IN_2_GGA2(x2, x4)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting we can delete all non-usable rules from R.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof

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

DIV_S_3_IN_GGA3(s_11(X), Y, s_11(Z)) -> IF_DIV_S_3_IN_2_GGA4(X, Y, Z, sub_3_in_gga3(X, Y, R))
IF_DIV_S_3_IN_2_GGA4(X, Y, Z, sub_3_out_gga3(X, Y, R)) -> DIV_S_3_IN_GGA3(R, Y, Z)

The TRS R consists of the following rules:

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)

The argument filtering Pi contains the following mapping:
s_11(x1)  =  s_11(x1)
0_0  =  0_0
sub_3_in_gga3(x1, x2, x3)  =  sub_3_in_gga2(x1, x2)
if_sub_3_in_1_gga4(x1, x2, x3, x4)  =  if_sub_3_in_1_gga1(x4)
sub_3_out_gga3(x1, x2, x3)  =  sub_3_out_gga1(x3)
DIV_S_3_IN_GGA3(x1, x2, x3)  =  DIV_S_3_IN_GGA2(x1, x2)
IF_DIV_S_3_IN_2_GGA4(x1, x2, x3, x4)  =  IF_DIV_S_3_IN_2_GGA2(x2, x4)

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

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof

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

DIV_S_3_IN_GGA2(s_11(X), Y) -> IF_DIV_S_3_IN_2_GGA2(Y, sub_3_in_gga2(X, Y))
IF_DIV_S_3_IN_2_GGA2(Y, sub_3_out_gga1(R)) -> DIV_S_3_IN_GGA2(R, Y)

The TRS R consists of the following rules:

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)

The set Q consists of the following terms:

sub_3_in_gga2(x0, x1)
if_sub_3_in_1_gga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {IF_DIV_S_3_IN_2_GGA2, DIV_S_3_IN_GGA2}.
We used the following order together with the size-change analysis to show that there are no infinite chains for this DP problem.

Order:Polynomial interpretation:


POL(0_0) = 0   
POL(if_sub_3_in_1_gga1(x1)) = x1   
POL(sub_3_out_gga1(x1)) = x1   
POL(sub_3_in_gga2(x1, x2)) = x1   
POL(s_11(x1)) = 1 + x1   

From the DPs we obtained the following set of size-change graphs:

We oriented the following set of usable rules.


sub_3_in_gga2(X, 0_0) -> sub_3_out_gga1(X)
sub_3_in_gga2(s_11(X), s_11(Y)) -> if_sub_3_in_1_gga1(sub_3_in_gga2(X, Y))
if_sub_3_in_1_gga1(sub_3_out_gga1(Z)) -> sub_3_out_gga1(Z)