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



↳ PROLOG
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof

le3(00, Y, true0).
le3(s1(X), 00, false0).
le3(s1(X), s1(Y), B) :- le3(X, Y, B).
minus3(X, 00, X).
minus3(s1(X), s1(Y), Z) :- minus3(X, Y, Z).
div3(X, s1(Y), Z) :- le3(s1(Y), X, B), if4(B, X, s1(Y), Z).
if4(false0, X, s1(Y), 00).
if4(true0, X, s1(Y), s1(Z)) :- minus3(X, Y, U), div3(U, s1(Y), Z).


With regard to the inferred argument filtering the predicates were used in the following modes:
div3: (b,b,f)
le3: (b,b,f)
if4: (b,b,b,f)
minus3: (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, le_3_in_gga3(s_11(Y), X, B))
le_3_in_gga3(0_0, Y, true_0) -> le_3_out_gga3(0_0, Y, true_0)
le_3_in_gga3(s_11(X), 0_0, false_0) -> le_3_out_gga3(s_11(X), 0_0, false_0)
le_3_in_gga3(s_11(X), s_11(Y), B) -> if_le_3_in_1_gga4(X, Y, B, le_3_in_gga3(X, Y, B))
if_le_3_in_1_gga4(X, Y, B, le_3_out_gga3(X, Y, B)) -> le_3_out_gga3(s_11(X), s_11(Y), B)
if_div_3_in_1_gga4(X, Y, Z, le_3_out_gga3(s_11(Y), X, B)) -> if_div_3_in_2_gga5(X, Y, Z, B, if_4_in_ggga4(B, X, s_11(Y), Z))
if_4_in_ggga4(false_0, X, s_11(Y), 0_0) -> if_4_out_ggga4(false_0, X, s_11(Y), 0_0)
if_4_in_ggga4(true_0, X, s_11(Y), s_11(Z)) -> if_if_4_in_1_ggga4(X, Y, Z, minus_3_in_gga3(X, Y, U))
minus_3_in_gga3(X, 0_0, X) -> minus_3_out_gga3(X, 0_0, X)
minus_3_in_gga3(s_11(X), s_11(Y), Z) -> if_minus_3_in_1_gga4(X, Y, Z, minus_3_in_gga3(X, Y, Z))
if_minus_3_in_1_gga4(X, Y, Z, minus_3_out_gga3(X, Y, Z)) -> minus_3_out_gga3(s_11(X), s_11(Y), Z)
if_if_4_in_1_ggga4(X, Y, Z, minus_3_out_gga3(X, Y, U)) -> if_if_4_in_2_ggga5(X, Y, Z, U, div_3_in_gga3(U, s_11(Y), Z))
if_if_4_in_2_ggga5(X, Y, Z, U, div_3_out_gga3(U, s_11(Y), Z)) -> if_4_out_ggga4(true_0, X, s_11(Y), s_11(Z))
if_div_3_in_2_gga5(X, Y, Z, B, if_4_out_ggga4(B, X, s_11(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)
0_0  =  0_0
true_0  =  true_0
s_11(x1)  =  s_11(x1)
false_0  =  false_0
if_div_3_in_1_gga4(x1, x2, x3, x4)  =  if_div_3_in_1_gga3(x1, x2, x4)
le_3_in_gga3(x1, x2, x3)  =  le_3_in_gga2(x1, x2)
le_3_out_gga3(x1, x2, x3)  =  le_3_out_gga1(x3)
if_le_3_in_1_gga4(x1, x2, x3, x4)  =  if_le_3_in_1_gga1(x4)
if_div_3_in_2_gga5(x1, x2, x3, x4, x5)  =  if_div_3_in_2_gga1(x5)
if_4_in_ggga4(x1, x2, x3, x4)  =  if_4_in_ggga3(x1, x2, x3)
if_4_out_ggga4(x1, x2, x3, x4)  =  if_4_out_ggga1(x4)
if_if_4_in_1_ggga4(x1, x2, x3, x4)  =  if_if_4_in_1_ggga2(x2, x4)
minus_3_in_gga3(x1, x2, x3)  =  minus_3_in_gga2(x1, x2)
minus_3_out_gga3(x1, x2, x3)  =  minus_3_out_gga1(x3)
if_minus_3_in_1_gga4(x1, x2, x3, x4)  =  if_minus_3_in_1_gga1(x4)
if_if_4_in_2_ggga5(x1, x2, x3, x4, x5)  =  if_if_4_in_2_ggga1(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
  ↳ PrologToPiTRSProof

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, le_3_in_gga3(s_11(Y), X, B))
le_3_in_gga3(0_0, Y, true_0) -> le_3_out_gga3(0_0, Y, true_0)
le_3_in_gga3(s_11(X), 0_0, false_0) -> le_3_out_gga3(s_11(X), 0_0, false_0)
le_3_in_gga3(s_11(X), s_11(Y), B) -> if_le_3_in_1_gga4(X, Y, B, le_3_in_gga3(X, Y, B))
if_le_3_in_1_gga4(X, Y, B, le_3_out_gga3(X, Y, B)) -> le_3_out_gga3(s_11(X), s_11(Y), B)
if_div_3_in_1_gga4(X, Y, Z, le_3_out_gga3(s_11(Y), X, B)) -> if_div_3_in_2_gga5(X, Y, Z, B, if_4_in_ggga4(B, X, s_11(Y), Z))
if_4_in_ggga4(false_0, X, s_11(Y), 0_0) -> if_4_out_ggga4(false_0, X, s_11(Y), 0_0)
if_4_in_ggga4(true_0, X, s_11(Y), s_11(Z)) -> if_if_4_in_1_ggga4(X, Y, Z, minus_3_in_gga3(X, Y, U))
minus_3_in_gga3(X, 0_0, X) -> minus_3_out_gga3(X, 0_0, X)
minus_3_in_gga3(s_11(X), s_11(Y), Z) -> if_minus_3_in_1_gga4(X, Y, Z, minus_3_in_gga3(X, Y, Z))
if_minus_3_in_1_gga4(X, Y, Z, minus_3_out_gga3(X, Y, Z)) -> minus_3_out_gga3(s_11(X), s_11(Y), Z)
if_if_4_in_1_ggga4(X, Y, Z, minus_3_out_gga3(X, Y, U)) -> if_if_4_in_2_ggga5(X, Y, Z, U, div_3_in_gga3(U, s_11(Y), Z))
if_if_4_in_2_ggga5(X, Y, Z, U, div_3_out_gga3(U, s_11(Y), Z)) -> if_4_out_ggga4(true_0, X, s_11(Y), s_11(Z))
if_div_3_in_2_gga5(X, Y, Z, B, if_4_out_ggga4(B, X, s_11(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)
0_0  =  0_0
true_0  =  true_0
s_11(x1)  =  s_11(x1)
false_0  =  false_0
if_div_3_in_1_gga4(x1, x2, x3, x4)  =  if_div_3_in_1_gga3(x1, x2, x4)
le_3_in_gga3(x1, x2, x3)  =  le_3_in_gga2(x1, x2)
le_3_out_gga3(x1, x2, x3)  =  le_3_out_gga1(x3)
if_le_3_in_1_gga4(x1, x2, x3, x4)  =  if_le_3_in_1_gga1(x4)
if_div_3_in_2_gga5(x1, x2, x3, x4, x5)  =  if_div_3_in_2_gga1(x5)
if_4_in_ggga4(x1, x2, x3, x4)  =  if_4_in_ggga3(x1, x2, x3)
if_4_out_ggga4(x1, x2, x3, x4)  =  if_4_out_ggga1(x4)
if_if_4_in_1_ggga4(x1, x2, x3, x4)  =  if_if_4_in_1_ggga2(x2, x4)
minus_3_in_gga3(x1, x2, x3)  =  minus_3_in_gga2(x1, x2)
minus_3_out_gga3(x1, x2, x3)  =  minus_3_out_gga1(x3)
if_minus_3_in_1_gga4(x1, x2, x3, x4)  =  if_minus_3_in_1_gga1(x4)
if_if_4_in_2_ggga5(x1, x2, x3, x4, x5)  =  if_if_4_in_2_ggga1(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, le_3_in_gga3(s_11(Y), X, B))
DIV_3_IN_GGA3(X, s_11(Y), Z) -> LE_3_IN_GGA3(s_11(Y), X, B)
LE_3_IN_GGA3(s_11(X), s_11(Y), B) -> IF_LE_3_IN_1_GGA4(X, Y, B, le_3_in_gga3(X, Y, B))
LE_3_IN_GGA3(s_11(X), s_11(Y), B) -> LE_3_IN_GGA3(X, Y, B)
IF_DIV_3_IN_1_GGA4(X, Y, Z, le_3_out_gga3(s_11(Y), X, B)) -> IF_DIV_3_IN_2_GGA5(X, Y, Z, B, if_4_in_ggga4(B, X, s_11(Y), Z))
IF_DIV_3_IN_1_GGA4(X, Y, Z, le_3_out_gga3(s_11(Y), X, B)) -> IF_4_IN_GGGA4(B, X, s_11(Y), Z)
IF_4_IN_GGGA4(true_0, X, s_11(Y), s_11(Z)) -> IF_IF_4_IN_1_GGGA4(X, Y, Z, minus_3_in_gga3(X, Y, U))
IF_4_IN_GGGA4(true_0, X, s_11(Y), s_11(Z)) -> MINUS_3_IN_GGA3(X, Y, U)
MINUS_3_IN_GGA3(s_11(X), s_11(Y), Z) -> IF_MINUS_3_IN_1_GGA4(X, Y, Z, minus_3_in_gga3(X, Y, Z))
MINUS_3_IN_GGA3(s_11(X), s_11(Y), Z) -> MINUS_3_IN_GGA3(X, Y, Z)
IF_IF_4_IN_1_GGGA4(X, Y, Z, minus_3_out_gga3(X, Y, U)) -> IF_IF_4_IN_2_GGGA5(X, Y, Z, U, div_3_in_gga3(U, s_11(Y), Z))
IF_IF_4_IN_1_GGGA4(X, Y, Z, minus_3_out_gga3(X, Y, U)) -> DIV_3_IN_GGA3(U, s_11(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, le_3_in_gga3(s_11(Y), X, B))
le_3_in_gga3(0_0, Y, true_0) -> le_3_out_gga3(0_0, Y, true_0)
le_3_in_gga3(s_11(X), 0_0, false_0) -> le_3_out_gga3(s_11(X), 0_0, false_0)
le_3_in_gga3(s_11(X), s_11(Y), B) -> if_le_3_in_1_gga4(X, Y, B, le_3_in_gga3(X, Y, B))
if_le_3_in_1_gga4(X, Y, B, le_3_out_gga3(X, Y, B)) -> le_3_out_gga3(s_11(X), s_11(Y), B)
if_div_3_in_1_gga4(X, Y, Z, le_3_out_gga3(s_11(Y), X, B)) -> if_div_3_in_2_gga5(X, Y, Z, B, if_4_in_ggga4(B, X, s_11(Y), Z))
if_4_in_ggga4(false_0, X, s_11(Y), 0_0) -> if_4_out_ggga4(false_0, X, s_11(Y), 0_0)
if_4_in_ggga4(true_0, X, s_11(Y), s_11(Z)) -> if_if_4_in_1_ggga4(X, Y, Z, minus_3_in_gga3(X, Y, U))
minus_3_in_gga3(X, 0_0, X) -> minus_3_out_gga3(X, 0_0, X)
minus_3_in_gga3(s_11(X), s_11(Y), Z) -> if_minus_3_in_1_gga4(X, Y, Z, minus_3_in_gga3(X, Y, Z))
if_minus_3_in_1_gga4(X, Y, Z, minus_3_out_gga3(X, Y, Z)) -> minus_3_out_gga3(s_11(X), s_11(Y), Z)
if_if_4_in_1_ggga4(X, Y, Z, minus_3_out_gga3(X, Y, U)) -> if_if_4_in_2_ggga5(X, Y, Z, U, div_3_in_gga3(U, s_11(Y), Z))
if_if_4_in_2_ggga5(X, Y, Z, U, div_3_out_gga3(U, s_11(Y), Z)) -> if_4_out_ggga4(true_0, X, s_11(Y), s_11(Z))
if_div_3_in_2_gga5(X, Y, Z, B, if_4_out_ggga4(B, X, s_11(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)
0_0  =  0_0
true_0  =  true_0
s_11(x1)  =  s_11(x1)
false_0  =  false_0
if_div_3_in_1_gga4(x1, x2, x3, x4)  =  if_div_3_in_1_gga3(x1, x2, x4)
le_3_in_gga3(x1, x2, x3)  =  le_3_in_gga2(x1, x2)
le_3_out_gga3(x1, x2, x3)  =  le_3_out_gga1(x3)
if_le_3_in_1_gga4(x1, x2, x3, x4)  =  if_le_3_in_1_gga1(x4)
if_div_3_in_2_gga5(x1, x2, x3, x4, x5)  =  if_div_3_in_2_gga1(x5)
if_4_in_ggga4(x1, x2, x3, x4)  =  if_4_in_ggga3(x1, x2, x3)
if_4_out_ggga4(x1, x2, x3, x4)  =  if_4_out_ggga1(x4)
if_if_4_in_1_ggga4(x1, x2, x3, x4)  =  if_if_4_in_1_ggga2(x2, x4)
minus_3_in_gga3(x1, x2, x3)  =  minus_3_in_gga2(x1, x2)
minus_3_out_gga3(x1, x2, x3)  =  minus_3_out_gga1(x3)
if_minus_3_in_1_gga4(x1, x2, x3, x4)  =  if_minus_3_in_1_gga1(x4)
if_if_4_in_2_ggga5(x1, x2, x3, x4, x5)  =  if_if_4_in_2_ggga1(x5)
div_3_out_gga3(x1, x2, x3)  =  div_3_out_gga1(x3)
IF_IF_4_IN_2_GGGA5(x1, x2, x3, x4, x5)  =  IF_IF_4_IN_2_GGGA1(x5)
DIV_3_IN_GGA3(x1, x2, x3)  =  DIV_3_IN_GGA2(x1, x2)
IF_4_IN_GGGA4(x1, x2, x3, x4)  =  IF_4_IN_GGGA3(x1, x2, x3)
IF_DIV_3_IN_1_GGA4(x1, x2, x3, x4)  =  IF_DIV_3_IN_1_GGA3(x1, x2, x4)
MINUS_3_IN_GGA3(x1, x2, x3)  =  MINUS_3_IN_GGA2(x1, x2)
IF_DIV_3_IN_2_GGA5(x1, x2, x3, x4, x5)  =  IF_DIV_3_IN_2_GGA1(x5)
IF_MINUS_3_IN_1_GGA4(x1, x2, x3, x4)  =  IF_MINUS_3_IN_1_GGA1(x4)
LE_3_IN_GGA3(x1, x2, x3)  =  LE_3_IN_GGA2(x1, x2)
IF_LE_3_IN_1_GGA4(x1, x2, x3, x4)  =  IF_LE_3_IN_1_GGA1(x4)
IF_IF_4_IN_1_GGGA4(x1, x2, x3, x4)  =  IF_IF_4_IN_1_GGGA2(x2, x4)

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

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

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, le_3_in_gga3(s_11(Y), X, B))
DIV_3_IN_GGA3(X, s_11(Y), Z) -> LE_3_IN_GGA3(s_11(Y), X, B)
LE_3_IN_GGA3(s_11(X), s_11(Y), B) -> IF_LE_3_IN_1_GGA4(X, Y, B, le_3_in_gga3(X, Y, B))
LE_3_IN_GGA3(s_11(X), s_11(Y), B) -> LE_3_IN_GGA3(X, Y, B)
IF_DIV_3_IN_1_GGA4(X, Y, Z, le_3_out_gga3(s_11(Y), X, B)) -> IF_DIV_3_IN_2_GGA5(X, Y, Z, B, if_4_in_ggga4(B, X, s_11(Y), Z))
IF_DIV_3_IN_1_GGA4(X, Y, Z, le_3_out_gga3(s_11(Y), X, B)) -> IF_4_IN_GGGA4(B, X, s_11(Y), Z)
IF_4_IN_GGGA4(true_0, X, s_11(Y), s_11(Z)) -> IF_IF_4_IN_1_GGGA4(X, Y, Z, minus_3_in_gga3(X, Y, U))
IF_4_IN_GGGA4(true_0, X, s_11(Y), s_11(Z)) -> MINUS_3_IN_GGA3(X, Y, U)
MINUS_3_IN_GGA3(s_11(X), s_11(Y), Z) -> IF_MINUS_3_IN_1_GGA4(X, Y, Z, minus_3_in_gga3(X, Y, Z))
MINUS_3_IN_GGA3(s_11(X), s_11(Y), Z) -> MINUS_3_IN_GGA3(X, Y, Z)
IF_IF_4_IN_1_GGGA4(X, Y, Z, minus_3_out_gga3(X, Y, U)) -> IF_IF_4_IN_2_GGGA5(X, Y, Z, U, div_3_in_gga3(U, s_11(Y), Z))
IF_IF_4_IN_1_GGGA4(X, Y, Z, minus_3_out_gga3(X, Y, U)) -> DIV_3_IN_GGA3(U, s_11(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, le_3_in_gga3(s_11(Y), X, B))
le_3_in_gga3(0_0, Y, true_0) -> le_3_out_gga3(0_0, Y, true_0)
le_3_in_gga3(s_11(X), 0_0, false_0) -> le_3_out_gga3(s_11(X), 0_0, false_0)
le_3_in_gga3(s_11(X), s_11(Y), B) -> if_le_3_in_1_gga4(X, Y, B, le_3_in_gga3(X, Y, B))
if_le_3_in_1_gga4(X, Y, B, le_3_out_gga3(X, Y, B)) -> le_3_out_gga3(s_11(X), s_11(Y), B)
if_div_3_in_1_gga4(X, Y, Z, le_3_out_gga3(s_11(Y), X, B)) -> if_div_3_in_2_gga5(X, Y, Z, B, if_4_in_ggga4(B, X, s_11(Y), Z))
if_4_in_ggga4(false_0, X, s_11(Y), 0_0) -> if_4_out_ggga4(false_0, X, s_11(Y), 0_0)
if_4_in_ggga4(true_0, X, s_11(Y), s_11(Z)) -> if_if_4_in_1_ggga4(X, Y, Z, minus_3_in_gga3(X, Y, U))
minus_3_in_gga3(X, 0_0, X) -> minus_3_out_gga3(X, 0_0, X)
minus_3_in_gga3(s_11(X), s_11(Y), Z) -> if_minus_3_in_1_gga4(X, Y, Z, minus_3_in_gga3(X, Y, Z))
if_minus_3_in_1_gga4(X, Y, Z, minus_3_out_gga3(X, Y, Z)) -> minus_3_out_gga3(s_11(X), s_11(Y), Z)
if_if_4_in_1_ggga4(X, Y, Z, minus_3_out_gga3(X, Y, U)) -> if_if_4_in_2_ggga5(X, Y, Z, U, div_3_in_gga3(U, s_11(Y), Z))
if_if_4_in_2_ggga5(X, Y, Z, U, div_3_out_gga3(U, s_11(Y), Z)) -> if_4_out_ggga4(true_0, X, s_11(Y), s_11(Z))
if_div_3_in_2_gga5(X, Y, Z, B, if_4_out_ggga4(B, X, s_11(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)
0_0  =  0_0
true_0  =  true_0
s_11(x1)  =  s_11(x1)
false_0  =  false_0
if_div_3_in_1_gga4(x1, x2, x3, x4)  =  if_div_3_in_1_gga3(x1, x2, x4)
le_3_in_gga3(x1, x2, x3)  =  le_3_in_gga2(x1, x2)
le_3_out_gga3(x1, x2, x3)  =  le_3_out_gga1(x3)
if_le_3_in_1_gga4(x1, x2, x3, x4)  =  if_le_3_in_1_gga1(x4)
if_div_3_in_2_gga5(x1, x2, x3, x4, x5)  =  if_div_3_in_2_gga1(x5)
if_4_in_ggga4(x1, x2, x3, x4)  =  if_4_in_ggga3(x1, x2, x3)
if_4_out_ggga4(x1, x2, x3, x4)  =  if_4_out_ggga1(x4)
if_if_4_in_1_ggga4(x1, x2, x3, x4)  =  if_if_4_in_1_ggga2(x2, x4)
minus_3_in_gga3(x1, x2, x3)  =  minus_3_in_gga2(x1, x2)
minus_3_out_gga3(x1, x2, x3)  =  minus_3_out_gga1(x3)
if_minus_3_in_1_gga4(x1, x2, x3, x4)  =  if_minus_3_in_1_gga1(x4)
if_if_4_in_2_ggga5(x1, x2, x3, x4, x5)  =  if_if_4_in_2_ggga1(x5)
div_3_out_gga3(x1, x2, x3)  =  div_3_out_gga1(x3)
IF_IF_4_IN_2_GGGA5(x1, x2, x3, x4, x5)  =  IF_IF_4_IN_2_GGGA1(x5)
DIV_3_IN_GGA3(x1, x2, x3)  =  DIV_3_IN_GGA2(x1, x2)
IF_4_IN_GGGA4(x1, x2, x3, x4)  =  IF_4_IN_GGGA3(x1, x2, x3)
IF_DIV_3_IN_1_GGA4(x1, x2, x3, x4)  =  IF_DIV_3_IN_1_GGA3(x1, x2, x4)
MINUS_3_IN_GGA3(x1, x2, x3)  =  MINUS_3_IN_GGA2(x1, x2)
IF_DIV_3_IN_2_GGA5(x1, x2, x3, x4, x5)  =  IF_DIV_3_IN_2_GGA1(x5)
IF_MINUS_3_IN_1_GGA4(x1, x2, x3, x4)  =  IF_MINUS_3_IN_1_GGA1(x4)
LE_3_IN_GGA3(x1, x2, x3)  =  LE_3_IN_GGA2(x1, x2)
IF_LE_3_IN_1_GGA4(x1, x2, x3, x4)  =  IF_LE_3_IN_1_GGA1(x4)
IF_IF_4_IN_1_GGGA4(x1, x2, x3, x4)  =  IF_IF_4_IN_1_GGGA2(x2, x4)

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

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

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

MINUS_3_IN_GGA3(s_11(X), s_11(Y), Z) -> MINUS_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, le_3_in_gga3(s_11(Y), X, B))
le_3_in_gga3(0_0, Y, true_0) -> le_3_out_gga3(0_0, Y, true_0)
le_3_in_gga3(s_11(X), 0_0, false_0) -> le_3_out_gga3(s_11(X), 0_0, false_0)
le_3_in_gga3(s_11(X), s_11(Y), B) -> if_le_3_in_1_gga4(X, Y, B, le_3_in_gga3(X, Y, B))
if_le_3_in_1_gga4(X, Y, B, le_3_out_gga3(X, Y, B)) -> le_3_out_gga3(s_11(X), s_11(Y), B)
if_div_3_in_1_gga4(X, Y, Z, le_3_out_gga3(s_11(Y), X, B)) -> if_div_3_in_2_gga5(X, Y, Z, B, if_4_in_ggga4(B, X, s_11(Y), Z))
if_4_in_ggga4(false_0, X, s_11(Y), 0_0) -> if_4_out_ggga4(false_0, X, s_11(Y), 0_0)
if_4_in_ggga4(true_0, X, s_11(Y), s_11(Z)) -> if_if_4_in_1_ggga4(X, Y, Z, minus_3_in_gga3(X, Y, U))
minus_3_in_gga3(X, 0_0, X) -> minus_3_out_gga3(X, 0_0, X)
minus_3_in_gga3(s_11(X), s_11(Y), Z) -> if_minus_3_in_1_gga4(X, Y, Z, minus_3_in_gga3(X, Y, Z))
if_minus_3_in_1_gga4(X, Y, Z, minus_3_out_gga3(X, Y, Z)) -> minus_3_out_gga3(s_11(X), s_11(Y), Z)
if_if_4_in_1_ggga4(X, Y, Z, minus_3_out_gga3(X, Y, U)) -> if_if_4_in_2_ggga5(X, Y, Z, U, div_3_in_gga3(U, s_11(Y), Z))
if_if_4_in_2_ggga5(X, Y, Z, U, div_3_out_gga3(U, s_11(Y), Z)) -> if_4_out_ggga4(true_0, X, s_11(Y), s_11(Z))
if_div_3_in_2_gga5(X, Y, Z, B, if_4_out_ggga4(B, X, s_11(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)
0_0  =  0_0
true_0  =  true_0
s_11(x1)  =  s_11(x1)
false_0  =  false_0
if_div_3_in_1_gga4(x1, x2, x3, x4)  =  if_div_3_in_1_gga3(x1, x2, x4)
le_3_in_gga3(x1, x2, x3)  =  le_3_in_gga2(x1, x2)
le_3_out_gga3(x1, x2, x3)  =  le_3_out_gga1(x3)
if_le_3_in_1_gga4(x1, x2, x3, x4)  =  if_le_3_in_1_gga1(x4)
if_div_3_in_2_gga5(x1, x2, x3, x4, x5)  =  if_div_3_in_2_gga1(x5)
if_4_in_ggga4(x1, x2, x3, x4)  =  if_4_in_ggga3(x1, x2, x3)
if_4_out_ggga4(x1, x2, x3, x4)  =  if_4_out_ggga1(x4)
if_if_4_in_1_ggga4(x1, x2, x3, x4)  =  if_if_4_in_1_ggga2(x2, x4)
minus_3_in_gga3(x1, x2, x3)  =  minus_3_in_gga2(x1, x2)
minus_3_out_gga3(x1, x2, x3)  =  minus_3_out_gga1(x3)
if_minus_3_in_1_gga4(x1, x2, x3, x4)  =  if_minus_3_in_1_gga1(x4)
if_if_4_in_2_ggga5(x1, x2, x3, x4, x5)  =  if_if_4_in_2_ggga1(x5)
div_3_out_gga3(x1, x2, x3)  =  div_3_out_gga1(x3)
MINUS_3_IN_GGA3(x1, x2, x3)  =  MINUS_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
  ↳ PrologToPiTRSProof

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

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

R is empty.
The argument filtering Pi contains the following mapping:
s_11(x1)  =  s_11(x1)
MINUS_3_IN_GGA3(x1, x2, x3)  =  MINUS_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
  ↳ PrologToPiTRSProof

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

MINUS_3_IN_GGA2(s_11(X), s_11(Y)) -> MINUS_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 {MINUS_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
  ↳ PrologToPiTRSProof

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

LE_3_IN_GGA3(s_11(X), s_11(Y), B) -> LE_3_IN_GGA3(X, Y, B)

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, le_3_in_gga3(s_11(Y), X, B))
le_3_in_gga3(0_0, Y, true_0) -> le_3_out_gga3(0_0, Y, true_0)
le_3_in_gga3(s_11(X), 0_0, false_0) -> le_3_out_gga3(s_11(X), 0_0, false_0)
le_3_in_gga3(s_11(X), s_11(Y), B) -> if_le_3_in_1_gga4(X, Y, B, le_3_in_gga3(X, Y, B))
if_le_3_in_1_gga4(X, Y, B, le_3_out_gga3(X, Y, B)) -> le_3_out_gga3(s_11(X), s_11(Y), B)
if_div_3_in_1_gga4(X, Y, Z, le_3_out_gga3(s_11(Y), X, B)) -> if_div_3_in_2_gga5(X, Y, Z, B, if_4_in_ggga4(B, X, s_11(Y), Z))
if_4_in_ggga4(false_0, X, s_11(Y), 0_0) -> if_4_out_ggga4(false_0, X, s_11(Y), 0_0)
if_4_in_ggga4(true_0, X, s_11(Y), s_11(Z)) -> if_if_4_in_1_ggga4(X, Y, Z, minus_3_in_gga3(X, Y, U))
minus_3_in_gga3(X, 0_0, X) -> minus_3_out_gga3(X, 0_0, X)
minus_3_in_gga3(s_11(X), s_11(Y), Z) -> if_minus_3_in_1_gga4(X, Y, Z, minus_3_in_gga3(X, Y, Z))
if_minus_3_in_1_gga4(X, Y, Z, minus_3_out_gga3(X, Y, Z)) -> minus_3_out_gga3(s_11(X), s_11(Y), Z)
if_if_4_in_1_ggga4(X, Y, Z, minus_3_out_gga3(X, Y, U)) -> if_if_4_in_2_ggga5(X, Y, Z, U, div_3_in_gga3(U, s_11(Y), Z))
if_if_4_in_2_ggga5(X, Y, Z, U, div_3_out_gga3(U, s_11(Y), Z)) -> if_4_out_ggga4(true_0, X, s_11(Y), s_11(Z))
if_div_3_in_2_gga5(X, Y, Z, B, if_4_out_ggga4(B, X, s_11(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)
0_0  =  0_0
true_0  =  true_0
s_11(x1)  =  s_11(x1)
false_0  =  false_0
if_div_3_in_1_gga4(x1, x2, x3, x4)  =  if_div_3_in_1_gga3(x1, x2, x4)
le_3_in_gga3(x1, x2, x3)  =  le_3_in_gga2(x1, x2)
le_3_out_gga3(x1, x2, x3)  =  le_3_out_gga1(x3)
if_le_3_in_1_gga4(x1, x2, x3, x4)  =  if_le_3_in_1_gga1(x4)
if_div_3_in_2_gga5(x1, x2, x3, x4, x5)  =  if_div_3_in_2_gga1(x5)
if_4_in_ggga4(x1, x2, x3, x4)  =  if_4_in_ggga3(x1, x2, x3)
if_4_out_ggga4(x1, x2, x3, x4)  =  if_4_out_ggga1(x4)
if_if_4_in_1_ggga4(x1, x2, x3, x4)  =  if_if_4_in_1_ggga2(x2, x4)
minus_3_in_gga3(x1, x2, x3)  =  minus_3_in_gga2(x1, x2)
minus_3_out_gga3(x1, x2, x3)  =  minus_3_out_gga1(x3)
if_minus_3_in_1_gga4(x1, x2, x3, x4)  =  if_minus_3_in_1_gga1(x4)
if_if_4_in_2_ggga5(x1, x2, x3, x4, x5)  =  if_if_4_in_2_ggga1(x5)
div_3_out_gga3(x1, x2, x3)  =  div_3_out_gga1(x3)
LE_3_IN_GGA3(x1, x2, x3)  =  LE_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
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
  ↳ PrologToPiTRSProof

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

LE_3_IN_GGA3(s_11(X), s_11(Y), B) -> LE_3_IN_GGA3(X, Y, B)

R is empty.
The argument filtering Pi contains the following mapping:
s_11(x1)  =  s_11(x1)
LE_3_IN_GGA3(x1, x2, x3)  =  LE_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
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
  ↳ PrologToPiTRSProof

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

LE_3_IN_GGA2(s_11(X), s_11(Y)) -> LE_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 {LE_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
              ↳ PiDP
                ↳ UsableRulesProof
  ↳ PrologToPiTRSProof

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

IF_IF_4_IN_1_GGGA4(X, Y, Z, minus_3_out_gga3(X, Y, U)) -> DIV_3_IN_GGA3(U, s_11(Y), Z)
DIV_3_IN_GGA3(X, s_11(Y), Z) -> IF_DIV_3_IN_1_GGA4(X, Y, Z, le_3_in_gga3(s_11(Y), X, B))
IF_4_IN_GGGA4(true_0, X, s_11(Y), s_11(Z)) -> IF_IF_4_IN_1_GGGA4(X, Y, Z, minus_3_in_gga3(X, Y, U))
IF_DIV_3_IN_1_GGA4(X, Y, Z, le_3_out_gga3(s_11(Y), X, B)) -> IF_4_IN_GGGA4(B, X, s_11(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, le_3_in_gga3(s_11(Y), X, B))
le_3_in_gga3(0_0, Y, true_0) -> le_3_out_gga3(0_0, Y, true_0)
le_3_in_gga3(s_11(X), 0_0, false_0) -> le_3_out_gga3(s_11(X), 0_0, false_0)
le_3_in_gga3(s_11(X), s_11(Y), B) -> if_le_3_in_1_gga4(X, Y, B, le_3_in_gga3(X, Y, B))
if_le_3_in_1_gga4(X, Y, B, le_3_out_gga3(X, Y, B)) -> le_3_out_gga3(s_11(X), s_11(Y), B)
if_div_3_in_1_gga4(X, Y, Z, le_3_out_gga3(s_11(Y), X, B)) -> if_div_3_in_2_gga5(X, Y, Z, B, if_4_in_ggga4(B, X, s_11(Y), Z))
if_4_in_ggga4(false_0, X, s_11(Y), 0_0) -> if_4_out_ggga4(false_0, X, s_11(Y), 0_0)
if_4_in_ggga4(true_0, X, s_11(Y), s_11(Z)) -> if_if_4_in_1_ggga4(X, Y, Z, minus_3_in_gga3(X, Y, U))
minus_3_in_gga3(X, 0_0, X) -> minus_3_out_gga3(X, 0_0, X)
minus_3_in_gga3(s_11(X), s_11(Y), Z) -> if_minus_3_in_1_gga4(X, Y, Z, minus_3_in_gga3(X, Y, Z))
if_minus_3_in_1_gga4(X, Y, Z, minus_3_out_gga3(X, Y, Z)) -> minus_3_out_gga3(s_11(X), s_11(Y), Z)
if_if_4_in_1_ggga4(X, Y, Z, minus_3_out_gga3(X, Y, U)) -> if_if_4_in_2_ggga5(X, Y, Z, U, div_3_in_gga3(U, s_11(Y), Z))
if_if_4_in_2_ggga5(X, Y, Z, U, div_3_out_gga3(U, s_11(Y), Z)) -> if_4_out_ggga4(true_0, X, s_11(Y), s_11(Z))
if_div_3_in_2_gga5(X, Y, Z, B, if_4_out_ggga4(B, X, s_11(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)
0_0  =  0_0
true_0  =  true_0
s_11(x1)  =  s_11(x1)
false_0  =  false_0
if_div_3_in_1_gga4(x1, x2, x3, x4)  =  if_div_3_in_1_gga3(x1, x2, x4)
le_3_in_gga3(x1, x2, x3)  =  le_3_in_gga2(x1, x2)
le_3_out_gga3(x1, x2, x3)  =  le_3_out_gga1(x3)
if_le_3_in_1_gga4(x1, x2, x3, x4)  =  if_le_3_in_1_gga1(x4)
if_div_3_in_2_gga5(x1, x2, x3, x4, x5)  =  if_div_3_in_2_gga1(x5)
if_4_in_ggga4(x1, x2, x3, x4)  =  if_4_in_ggga3(x1, x2, x3)
if_4_out_ggga4(x1, x2, x3, x4)  =  if_4_out_ggga1(x4)
if_if_4_in_1_ggga4(x1, x2, x3, x4)  =  if_if_4_in_1_ggga2(x2, x4)
minus_3_in_gga3(x1, x2, x3)  =  minus_3_in_gga2(x1, x2)
minus_3_out_gga3(x1, x2, x3)  =  minus_3_out_gga1(x3)
if_minus_3_in_1_gga4(x1, x2, x3, x4)  =  if_minus_3_in_1_gga1(x4)
if_if_4_in_2_ggga5(x1, x2, x3, x4, x5)  =  if_if_4_in_2_ggga1(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_4_IN_GGGA4(x1, x2, x3, x4)  =  IF_4_IN_GGGA3(x1, x2, x3)
IF_DIV_3_IN_1_GGA4(x1, x2, x3, x4)  =  IF_DIV_3_IN_1_GGA3(x1, x2, x4)
IF_IF_4_IN_1_GGGA4(x1, x2, x3, x4)  =  IF_IF_4_IN_1_GGGA2(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
  ↳ PrologToPiTRSProof

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

IF_IF_4_IN_1_GGGA4(X, Y, Z, minus_3_out_gga3(X, Y, U)) -> DIV_3_IN_GGA3(U, s_11(Y), Z)
DIV_3_IN_GGA3(X, s_11(Y), Z) -> IF_DIV_3_IN_1_GGA4(X, Y, Z, le_3_in_gga3(s_11(Y), X, B))
IF_4_IN_GGGA4(true_0, X, s_11(Y), s_11(Z)) -> IF_IF_4_IN_1_GGGA4(X, Y, Z, minus_3_in_gga3(X, Y, U))
IF_DIV_3_IN_1_GGA4(X, Y, Z, le_3_out_gga3(s_11(Y), X, B)) -> IF_4_IN_GGGA4(B, X, s_11(Y), Z)

The TRS R consists of the following rules:

le_3_in_gga3(s_11(X), 0_0, false_0) -> le_3_out_gga3(s_11(X), 0_0, false_0)
le_3_in_gga3(s_11(X), s_11(Y), B) -> if_le_3_in_1_gga4(X, Y, B, le_3_in_gga3(X, Y, B))
minus_3_in_gga3(X, 0_0, X) -> minus_3_out_gga3(X, 0_0, X)
minus_3_in_gga3(s_11(X), s_11(Y), Z) -> if_minus_3_in_1_gga4(X, Y, Z, minus_3_in_gga3(X, Y, Z))
if_le_3_in_1_gga4(X, Y, B, le_3_out_gga3(X, Y, B)) -> le_3_out_gga3(s_11(X), s_11(Y), B)
if_minus_3_in_1_gga4(X, Y, Z, minus_3_out_gga3(X, Y, Z)) -> minus_3_out_gga3(s_11(X), s_11(Y), Z)
le_3_in_gga3(0_0, Y, true_0) -> le_3_out_gga3(0_0, Y, true_0)

The argument filtering Pi contains the following mapping:
0_0  =  0_0
true_0  =  true_0
s_11(x1)  =  s_11(x1)
false_0  =  false_0
le_3_in_gga3(x1, x2, x3)  =  le_3_in_gga2(x1, x2)
le_3_out_gga3(x1, x2, x3)  =  le_3_out_gga1(x3)
if_le_3_in_1_gga4(x1, x2, x3, x4)  =  if_le_3_in_1_gga1(x4)
minus_3_in_gga3(x1, x2, x3)  =  minus_3_in_gga2(x1, x2)
minus_3_out_gga3(x1, x2, x3)  =  minus_3_out_gga1(x3)
if_minus_3_in_1_gga4(x1, x2, x3, x4)  =  if_minus_3_in_1_gga1(x4)
DIV_3_IN_GGA3(x1, x2, x3)  =  DIV_3_IN_GGA2(x1, x2)
IF_4_IN_GGGA4(x1, x2, x3, x4)  =  IF_4_IN_GGGA3(x1, x2, x3)
IF_DIV_3_IN_1_GGA4(x1, x2, x3, x4)  =  IF_DIV_3_IN_1_GGA3(x1, x2, x4)
IF_IF_4_IN_1_GGGA4(x1, x2, x3, x4)  =  IF_IF_4_IN_1_GGGA2(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
  ↳ PrologToPiTRSProof

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

IF_IF_4_IN_1_GGGA2(Y, minus_3_out_gga1(U)) -> DIV_3_IN_GGA2(U, s_11(Y))
DIV_3_IN_GGA2(X, s_11(Y)) -> IF_DIV_3_IN_1_GGA3(X, Y, le_3_in_gga2(s_11(Y), X))
IF_4_IN_GGGA3(true_0, X, s_11(Y)) -> IF_IF_4_IN_1_GGGA2(Y, minus_3_in_gga2(X, Y))
IF_DIV_3_IN_1_GGA3(X, Y, le_3_out_gga1(B)) -> IF_4_IN_GGGA3(B, X, s_11(Y))

The TRS R consists of the following rules:

le_3_in_gga2(s_11(X), 0_0) -> le_3_out_gga1(false_0)
le_3_in_gga2(s_11(X), s_11(Y)) -> if_le_3_in_1_gga1(le_3_in_gga2(X, Y))
minus_3_in_gga2(X, 0_0) -> minus_3_out_gga1(X)
minus_3_in_gga2(s_11(X), s_11(Y)) -> if_minus_3_in_1_gga1(minus_3_in_gga2(X, Y))
if_le_3_in_1_gga1(le_3_out_gga1(B)) -> le_3_out_gga1(B)
if_minus_3_in_1_gga1(minus_3_out_gga1(Z)) -> minus_3_out_gga1(Z)
le_3_in_gga2(0_0, Y) -> le_3_out_gga1(true_0)

The set Q consists of the following terms:

le_3_in_gga2(x0, x1)
minus_3_in_gga2(x0, x1)
if_le_3_in_1_gga1(x0)
if_minus_3_in_1_gga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {DIV_3_IN_GGA2, IF_IF_4_IN_1_GGGA2, IF_DIV_3_IN_1_GGA3, IF_4_IN_GGGA3}.
With regard to the inferred argument filtering the predicates were used in the following modes:
div3: (b,b,f)
le3: (b,b,f)
if4: (b,b,b,f)
minus3: (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, le_3_in_gga3(s_11(Y), X, B))
le_3_in_gga3(0_0, Y, true_0) -> le_3_out_gga3(0_0, Y, true_0)
le_3_in_gga3(s_11(X), 0_0, false_0) -> le_3_out_gga3(s_11(X), 0_0, false_0)
le_3_in_gga3(s_11(X), s_11(Y), B) -> if_le_3_in_1_gga4(X, Y, B, le_3_in_gga3(X, Y, B))
if_le_3_in_1_gga4(X, Y, B, le_3_out_gga3(X, Y, B)) -> le_3_out_gga3(s_11(X), s_11(Y), B)
if_div_3_in_1_gga4(X, Y, Z, le_3_out_gga3(s_11(Y), X, B)) -> if_div_3_in_2_gga5(X, Y, Z, B, if_4_in_ggga4(B, X, s_11(Y), Z))
if_4_in_ggga4(false_0, X, s_11(Y), 0_0) -> if_4_out_ggga4(false_0, X, s_11(Y), 0_0)
if_4_in_ggga4(true_0, X, s_11(Y), s_11(Z)) -> if_if_4_in_1_ggga4(X, Y, Z, minus_3_in_gga3(X, Y, U))
minus_3_in_gga3(X, 0_0, X) -> minus_3_out_gga3(X, 0_0, X)
minus_3_in_gga3(s_11(X), s_11(Y), Z) -> if_minus_3_in_1_gga4(X, Y, Z, minus_3_in_gga3(X, Y, Z))
if_minus_3_in_1_gga4(X, Y, Z, minus_3_out_gga3(X, Y, Z)) -> minus_3_out_gga3(s_11(X), s_11(Y), Z)
if_if_4_in_1_ggga4(X, Y, Z, minus_3_out_gga3(X, Y, U)) -> if_if_4_in_2_ggga5(X, Y, Z, U, div_3_in_gga3(U, s_11(Y), Z))
if_if_4_in_2_ggga5(X, Y, Z, U, div_3_out_gga3(U, s_11(Y), Z)) -> if_4_out_ggga4(true_0, X, s_11(Y), s_11(Z))
if_div_3_in_2_gga5(X, Y, Z, B, if_4_out_ggga4(B, X, s_11(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)
0_0  =  0_0
true_0  =  true_0
s_11(x1)  =  s_11(x1)
false_0  =  false_0
if_div_3_in_1_gga4(x1, x2, x3, x4)  =  if_div_3_in_1_gga3(x1, x2, x4)
le_3_in_gga3(x1, x2, x3)  =  le_3_in_gga2(x1, x2)
le_3_out_gga3(x1, x2, x3)  =  le_3_out_gga3(x1, x2, x3)
if_le_3_in_1_gga4(x1, x2, x3, x4)  =  if_le_3_in_1_gga3(x1, x2, x4)
if_div_3_in_2_gga5(x1, x2, x3, x4, x5)  =  if_div_3_in_2_gga3(x1, x2, x5)
if_4_in_ggga4(x1, x2, x3, x4)  =  if_4_in_ggga3(x1, x2, x3)
if_4_out_ggga4(x1, x2, x3, x4)  =  if_4_out_ggga4(x1, x2, x3, x4)
if_if_4_in_1_ggga4(x1, x2, x3, x4)  =  if_if_4_in_1_ggga3(x1, x2, x4)
minus_3_in_gga3(x1, x2, x3)  =  minus_3_in_gga2(x1, x2)
minus_3_out_gga3(x1, x2, x3)  =  minus_3_out_gga3(x1, x2, x3)
if_minus_3_in_1_gga4(x1, x2, x3, x4)  =  if_minus_3_in_1_gga3(x1, x2, x4)
if_if_4_in_2_ggga5(x1, x2, x3, x4, x5)  =  if_if_4_in_2_ggga3(x1, x2, x5)
div_3_out_gga3(x1, x2, x3)  =  div_3_out_gga3(x1, x2, x3)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG



↳ PROLOG
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS

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, le_3_in_gga3(s_11(Y), X, B))
le_3_in_gga3(0_0, Y, true_0) -> le_3_out_gga3(0_0, Y, true_0)
le_3_in_gga3(s_11(X), 0_0, false_0) -> le_3_out_gga3(s_11(X), 0_0, false_0)
le_3_in_gga3(s_11(X), s_11(Y), B) -> if_le_3_in_1_gga4(X, Y, B, le_3_in_gga3(X, Y, B))
if_le_3_in_1_gga4(X, Y, B, le_3_out_gga3(X, Y, B)) -> le_3_out_gga3(s_11(X), s_11(Y), B)
if_div_3_in_1_gga4(X, Y, Z, le_3_out_gga3(s_11(Y), X, B)) -> if_div_3_in_2_gga5(X, Y, Z, B, if_4_in_ggga4(B, X, s_11(Y), Z))
if_4_in_ggga4(false_0, X, s_11(Y), 0_0) -> if_4_out_ggga4(false_0, X, s_11(Y), 0_0)
if_4_in_ggga4(true_0, X, s_11(Y), s_11(Z)) -> if_if_4_in_1_ggga4(X, Y, Z, minus_3_in_gga3(X, Y, U))
minus_3_in_gga3(X, 0_0, X) -> minus_3_out_gga3(X, 0_0, X)
minus_3_in_gga3(s_11(X), s_11(Y), Z) -> if_minus_3_in_1_gga4(X, Y, Z, minus_3_in_gga3(X, Y, Z))
if_minus_3_in_1_gga4(X, Y, Z, minus_3_out_gga3(X, Y, Z)) -> minus_3_out_gga3(s_11(X), s_11(Y), Z)
if_if_4_in_1_ggga4(X, Y, Z, minus_3_out_gga3(X, Y, U)) -> if_if_4_in_2_ggga5(X, Y, Z, U, div_3_in_gga3(U, s_11(Y), Z))
if_if_4_in_2_ggga5(X, Y, Z, U, div_3_out_gga3(U, s_11(Y), Z)) -> if_4_out_ggga4(true_0, X, s_11(Y), s_11(Z))
if_div_3_in_2_gga5(X, Y, Z, B, if_4_out_ggga4(B, X, s_11(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)
0_0  =  0_0
true_0  =  true_0
s_11(x1)  =  s_11(x1)
false_0  =  false_0
if_div_3_in_1_gga4(x1, x2, x3, x4)  =  if_div_3_in_1_gga3(x1, x2, x4)
le_3_in_gga3(x1, x2, x3)  =  le_3_in_gga2(x1, x2)
le_3_out_gga3(x1, x2, x3)  =  le_3_out_gga3(x1, x2, x3)
if_le_3_in_1_gga4(x1, x2, x3, x4)  =  if_le_3_in_1_gga3(x1, x2, x4)
if_div_3_in_2_gga5(x1, x2, x3, x4, x5)  =  if_div_3_in_2_gga3(x1, x2, x5)
if_4_in_ggga4(x1, x2, x3, x4)  =  if_4_in_ggga3(x1, x2, x3)
if_4_out_ggga4(x1, x2, x3, x4)  =  if_4_out_ggga4(x1, x2, x3, x4)
if_if_4_in_1_ggga4(x1, x2, x3, x4)  =  if_if_4_in_1_ggga3(x1, x2, x4)
minus_3_in_gga3(x1, x2, x3)  =  minus_3_in_gga2(x1, x2)
minus_3_out_gga3(x1, x2, x3)  =  minus_3_out_gga3(x1, x2, x3)
if_minus_3_in_1_gga4(x1, x2, x3, x4)  =  if_minus_3_in_1_gga3(x1, x2, x4)
if_if_4_in_2_ggga5(x1, x2, x3, x4, x5)  =  if_if_4_in_2_ggga3(x1, x2, x5)
div_3_out_gga3(x1, x2, x3)  =  div_3_out_gga3(x1, x2, x3)