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



↳ PROLOG
  ↳ PrologToPiTRSProof

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


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


minus_3_in_gaa3(X, Y, Z) -> if_minus_3_in_1_gaa4(X, Y, Z, le_3_in_gaa3(X, Y, B))
le_3_in_gaa3(0_0, Y, true_0) -> le_3_out_gaa3(0_0, Y, true_0)
le_3_in_gaa3(s_11(X), 0_0, false_0) -> le_3_out_gaa3(s_11(X), 0_0, false_0)
le_3_in_gaa3(s_11(X), s_11(Y), B) -> if_le_3_in_1_gaa4(X, Y, B, le_3_in_gaa3(X, Y, B))
if_le_3_in_1_gaa4(X, Y, B, le_3_out_gaa3(X, Y, B)) -> le_3_out_gaa3(s_11(X), s_11(Y), B)
if_minus_3_in_1_gaa4(X, Y, Z, le_3_out_gaa3(X, Y, B)) -> if_minus_3_in_2_gaa5(X, Y, Z, B, if_4_in_ggaa4(B, X, Y, Z))
if_4_in_ggaa4(true_0, X, Y, 0_0) -> if_4_out_ggaa4(true_0, X, Y, 0_0)
if_4_in_ggaa4(false_0, X, Y, s_11(Z)) -> if_if_4_in_1_ggaa4(X, Y, Z, p_2_in_ga2(X, X1))
p_2_in_ga2(0_0, 0_0) -> p_2_out_ga2(0_0, 0_0)
p_2_in_ga2(s_11(X), X) -> p_2_out_ga2(s_11(X), X)
if_if_4_in_1_ggaa4(X, Y, Z, p_2_out_ga2(X, X1)) -> if_if_4_in_2_ggaa5(X, Y, Z, X1, minus_3_in_gaa3(X1, Y, Z))
if_if_4_in_2_ggaa5(X, Y, Z, X1, minus_3_out_gaa3(X1, Y, Z)) -> if_4_out_ggaa4(false_0, X, Y, s_11(Z))
if_minus_3_in_2_gaa5(X, Y, Z, B, if_4_out_ggaa4(B, X, Y, Z)) -> minus_3_out_gaa3(X, Y, Z)

The argument filtering Pi contains the following mapping:
minus_3_in_gaa3(x1, x2, x3)  =  minus_3_in_gaa1(x1)
0_0  =  0_0
s_11(x1)  =  s_11(x1)
true_0  =  true_0
false_0  =  false_0
if_minus_3_in_1_gaa4(x1, x2, x3, x4)  =  if_minus_3_in_1_gaa2(x1, x4)
le_3_in_gaa3(x1, x2, x3)  =  le_3_in_gaa1(x1)
le_3_out_gaa3(x1, x2, x3)  =  le_3_out_gaa1(x3)
if_le_3_in_1_gaa4(x1, x2, x3, x4)  =  if_le_3_in_1_gaa1(x4)
if_minus_3_in_2_gaa5(x1, x2, x3, x4, x5)  =  if_minus_3_in_2_gaa1(x5)
if_4_in_ggaa4(x1, x2, x3, x4)  =  if_4_in_ggaa2(x1, x2)
if_4_out_ggaa4(x1, x2, x3, x4)  =  if_4_out_ggaa1(x4)
if_if_4_in_1_ggaa4(x1, x2, x3, x4)  =  if_if_4_in_1_ggaa1(x4)
p_2_in_ga2(x1, x2)  =  p_2_in_ga1(x1)
p_2_out_ga2(x1, x2)  =  p_2_out_ga1(x2)
if_if_4_in_2_ggaa5(x1, x2, x3, x4, x5)  =  if_if_4_in_2_ggaa1(x5)
minus_3_out_gaa3(x1, x2, x3)  =  minus_3_out_gaa1(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:

minus_3_in_gaa3(X, Y, Z) -> if_minus_3_in_1_gaa4(X, Y, Z, le_3_in_gaa3(X, Y, B))
le_3_in_gaa3(0_0, Y, true_0) -> le_3_out_gaa3(0_0, Y, true_0)
le_3_in_gaa3(s_11(X), 0_0, false_0) -> le_3_out_gaa3(s_11(X), 0_0, false_0)
le_3_in_gaa3(s_11(X), s_11(Y), B) -> if_le_3_in_1_gaa4(X, Y, B, le_3_in_gaa3(X, Y, B))
if_le_3_in_1_gaa4(X, Y, B, le_3_out_gaa3(X, Y, B)) -> le_3_out_gaa3(s_11(X), s_11(Y), B)
if_minus_3_in_1_gaa4(X, Y, Z, le_3_out_gaa3(X, Y, B)) -> if_minus_3_in_2_gaa5(X, Y, Z, B, if_4_in_ggaa4(B, X, Y, Z))
if_4_in_ggaa4(true_0, X, Y, 0_0) -> if_4_out_ggaa4(true_0, X, Y, 0_0)
if_4_in_ggaa4(false_0, X, Y, s_11(Z)) -> if_if_4_in_1_ggaa4(X, Y, Z, p_2_in_ga2(X, X1))
p_2_in_ga2(0_0, 0_0) -> p_2_out_ga2(0_0, 0_0)
p_2_in_ga2(s_11(X), X) -> p_2_out_ga2(s_11(X), X)
if_if_4_in_1_ggaa4(X, Y, Z, p_2_out_ga2(X, X1)) -> if_if_4_in_2_ggaa5(X, Y, Z, X1, minus_3_in_gaa3(X1, Y, Z))
if_if_4_in_2_ggaa5(X, Y, Z, X1, minus_3_out_gaa3(X1, Y, Z)) -> if_4_out_ggaa4(false_0, X, Y, s_11(Z))
if_minus_3_in_2_gaa5(X, Y, Z, B, if_4_out_ggaa4(B, X, Y, Z)) -> minus_3_out_gaa3(X, Y, Z)

The argument filtering Pi contains the following mapping:
minus_3_in_gaa3(x1, x2, x3)  =  minus_3_in_gaa1(x1)
0_0  =  0_0
s_11(x1)  =  s_11(x1)
true_0  =  true_0
false_0  =  false_0
if_minus_3_in_1_gaa4(x1, x2, x3, x4)  =  if_minus_3_in_1_gaa2(x1, x4)
le_3_in_gaa3(x1, x2, x3)  =  le_3_in_gaa1(x1)
le_3_out_gaa3(x1, x2, x3)  =  le_3_out_gaa1(x3)
if_le_3_in_1_gaa4(x1, x2, x3, x4)  =  if_le_3_in_1_gaa1(x4)
if_minus_3_in_2_gaa5(x1, x2, x3, x4, x5)  =  if_minus_3_in_2_gaa1(x5)
if_4_in_ggaa4(x1, x2, x3, x4)  =  if_4_in_ggaa2(x1, x2)
if_4_out_ggaa4(x1, x2, x3, x4)  =  if_4_out_ggaa1(x4)
if_if_4_in_1_ggaa4(x1, x2, x3, x4)  =  if_if_4_in_1_ggaa1(x4)
p_2_in_ga2(x1, x2)  =  p_2_in_ga1(x1)
p_2_out_ga2(x1, x2)  =  p_2_out_ga1(x2)
if_if_4_in_2_ggaa5(x1, x2, x3, x4, x5)  =  if_if_4_in_2_ggaa1(x5)
minus_3_out_gaa3(x1, x2, x3)  =  minus_3_out_gaa1(x3)


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

MINUS_3_IN_GAA3(X, Y, Z) -> IF_MINUS_3_IN_1_GAA4(X, Y, Z, le_3_in_gaa3(X, Y, B))
MINUS_3_IN_GAA3(X, Y, Z) -> LE_3_IN_GAA3(X, Y, B)
LE_3_IN_GAA3(s_11(X), s_11(Y), B) -> IF_LE_3_IN_1_GAA4(X, Y, B, le_3_in_gaa3(X, Y, B))
LE_3_IN_GAA3(s_11(X), s_11(Y), B) -> LE_3_IN_GAA3(X, Y, B)
IF_MINUS_3_IN_1_GAA4(X, Y, Z, le_3_out_gaa3(X, Y, B)) -> IF_MINUS_3_IN_2_GAA5(X, Y, Z, B, if_4_in_ggaa4(B, X, Y, Z))
IF_MINUS_3_IN_1_GAA4(X, Y, Z, le_3_out_gaa3(X, Y, B)) -> IF_4_IN_GGAA4(B, X, Y, Z)
IF_4_IN_GGAA4(false_0, X, Y, s_11(Z)) -> IF_IF_4_IN_1_GGAA4(X, Y, Z, p_2_in_ga2(X, X1))
IF_4_IN_GGAA4(false_0, X, Y, s_11(Z)) -> P_2_IN_GA2(X, X1)
IF_IF_4_IN_1_GGAA4(X, Y, Z, p_2_out_ga2(X, X1)) -> IF_IF_4_IN_2_GGAA5(X, Y, Z, X1, minus_3_in_gaa3(X1, Y, Z))
IF_IF_4_IN_1_GGAA4(X, Y, Z, p_2_out_ga2(X, X1)) -> MINUS_3_IN_GAA3(X1, Y, Z)

The TRS R consists of the following rules:

minus_3_in_gaa3(X, Y, Z) -> if_minus_3_in_1_gaa4(X, Y, Z, le_3_in_gaa3(X, Y, B))
le_3_in_gaa3(0_0, Y, true_0) -> le_3_out_gaa3(0_0, Y, true_0)
le_3_in_gaa3(s_11(X), 0_0, false_0) -> le_3_out_gaa3(s_11(X), 0_0, false_0)
le_3_in_gaa3(s_11(X), s_11(Y), B) -> if_le_3_in_1_gaa4(X, Y, B, le_3_in_gaa3(X, Y, B))
if_le_3_in_1_gaa4(X, Y, B, le_3_out_gaa3(X, Y, B)) -> le_3_out_gaa3(s_11(X), s_11(Y), B)
if_minus_3_in_1_gaa4(X, Y, Z, le_3_out_gaa3(X, Y, B)) -> if_minus_3_in_2_gaa5(X, Y, Z, B, if_4_in_ggaa4(B, X, Y, Z))
if_4_in_ggaa4(true_0, X, Y, 0_0) -> if_4_out_ggaa4(true_0, X, Y, 0_0)
if_4_in_ggaa4(false_0, X, Y, s_11(Z)) -> if_if_4_in_1_ggaa4(X, Y, Z, p_2_in_ga2(X, X1))
p_2_in_ga2(0_0, 0_0) -> p_2_out_ga2(0_0, 0_0)
p_2_in_ga2(s_11(X), X) -> p_2_out_ga2(s_11(X), X)
if_if_4_in_1_ggaa4(X, Y, Z, p_2_out_ga2(X, X1)) -> if_if_4_in_2_ggaa5(X, Y, Z, X1, minus_3_in_gaa3(X1, Y, Z))
if_if_4_in_2_ggaa5(X, Y, Z, X1, minus_3_out_gaa3(X1, Y, Z)) -> if_4_out_ggaa4(false_0, X, Y, s_11(Z))
if_minus_3_in_2_gaa5(X, Y, Z, B, if_4_out_ggaa4(B, X, Y, Z)) -> minus_3_out_gaa3(X, Y, Z)

The argument filtering Pi contains the following mapping:
minus_3_in_gaa3(x1, x2, x3)  =  minus_3_in_gaa1(x1)
0_0  =  0_0
s_11(x1)  =  s_11(x1)
true_0  =  true_0
false_0  =  false_0
if_minus_3_in_1_gaa4(x1, x2, x3, x4)  =  if_minus_3_in_1_gaa2(x1, x4)
le_3_in_gaa3(x1, x2, x3)  =  le_3_in_gaa1(x1)
le_3_out_gaa3(x1, x2, x3)  =  le_3_out_gaa1(x3)
if_le_3_in_1_gaa4(x1, x2, x3, x4)  =  if_le_3_in_1_gaa1(x4)
if_minus_3_in_2_gaa5(x1, x2, x3, x4, x5)  =  if_minus_3_in_2_gaa1(x5)
if_4_in_ggaa4(x1, x2, x3, x4)  =  if_4_in_ggaa2(x1, x2)
if_4_out_ggaa4(x1, x2, x3, x4)  =  if_4_out_ggaa1(x4)
if_if_4_in_1_ggaa4(x1, x2, x3, x4)  =  if_if_4_in_1_ggaa1(x4)
p_2_in_ga2(x1, x2)  =  p_2_in_ga1(x1)
p_2_out_ga2(x1, x2)  =  p_2_out_ga1(x2)
if_if_4_in_2_ggaa5(x1, x2, x3, x4, x5)  =  if_if_4_in_2_ggaa1(x5)
minus_3_out_gaa3(x1, x2, x3)  =  minus_3_out_gaa1(x3)
IF_LE_3_IN_1_GAA4(x1, x2, x3, x4)  =  IF_LE_3_IN_1_GAA1(x4)
IF_MINUS_3_IN_1_GAA4(x1, x2, x3, x4)  =  IF_MINUS_3_IN_1_GAA2(x1, x4)
LE_3_IN_GAA3(x1, x2, x3)  =  LE_3_IN_GAA1(x1)
IF_IF_4_IN_2_GGAA5(x1, x2, x3, x4, x5)  =  IF_IF_4_IN_2_GGAA1(x5)
P_2_IN_GA2(x1, x2)  =  P_2_IN_GA1(x1)
IF_IF_4_IN_1_GGAA4(x1, x2, x3, x4)  =  IF_IF_4_IN_1_GGAA1(x4)
IF_4_IN_GGAA4(x1, x2, x3, x4)  =  IF_4_IN_GGAA2(x1, x2)
IF_MINUS_3_IN_2_GAA5(x1, x2, x3, x4, x5)  =  IF_MINUS_3_IN_2_GAA1(x5)
MINUS_3_IN_GAA3(x1, x2, x3)  =  MINUS_3_IN_GAA1(x1)

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:

MINUS_3_IN_GAA3(X, Y, Z) -> IF_MINUS_3_IN_1_GAA4(X, Y, Z, le_3_in_gaa3(X, Y, B))
MINUS_3_IN_GAA3(X, Y, Z) -> LE_3_IN_GAA3(X, Y, B)
LE_3_IN_GAA3(s_11(X), s_11(Y), B) -> IF_LE_3_IN_1_GAA4(X, Y, B, le_3_in_gaa3(X, Y, B))
LE_3_IN_GAA3(s_11(X), s_11(Y), B) -> LE_3_IN_GAA3(X, Y, B)
IF_MINUS_3_IN_1_GAA4(X, Y, Z, le_3_out_gaa3(X, Y, B)) -> IF_MINUS_3_IN_2_GAA5(X, Y, Z, B, if_4_in_ggaa4(B, X, Y, Z))
IF_MINUS_3_IN_1_GAA4(X, Y, Z, le_3_out_gaa3(X, Y, B)) -> IF_4_IN_GGAA4(B, X, Y, Z)
IF_4_IN_GGAA4(false_0, X, Y, s_11(Z)) -> IF_IF_4_IN_1_GGAA4(X, Y, Z, p_2_in_ga2(X, X1))
IF_4_IN_GGAA4(false_0, X, Y, s_11(Z)) -> P_2_IN_GA2(X, X1)
IF_IF_4_IN_1_GGAA4(X, Y, Z, p_2_out_ga2(X, X1)) -> IF_IF_4_IN_2_GGAA5(X, Y, Z, X1, minus_3_in_gaa3(X1, Y, Z))
IF_IF_4_IN_1_GGAA4(X, Y, Z, p_2_out_ga2(X, X1)) -> MINUS_3_IN_GAA3(X1, Y, Z)

The TRS R consists of the following rules:

minus_3_in_gaa3(X, Y, Z) -> if_minus_3_in_1_gaa4(X, Y, Z, le_3_in_gaa3(X, Y, B))
le_3_in_gaa3(0_0, Y, true_0) -> le_3_out_gaa3(0_0, Y, true_0)
le_3_in_gaa3(s_11(X), 0_0, false_0) -> le_3_out_gaa3(s_11(X), 0_0, false_0)
le_3_in_gaa3(s_11(X), s_11(Y), B) -> if_le_3_in_1_gaa4(X, Y, B, le_3_in_gaa3(X, Y, B))
if_le_3_in_1_gaa4(X, Y, B, le_3_out_gaa3(X, Y, B)) -> le_3_out_gaa3(s_11(X), s_11(Y), B)
if_minus_3_in_1_gaa4(X, Y, Z, le_3_out_gaa3(X, Y, B)) -> if_minus_3_in_2_gaa5(X, Y, Z, B, if_4_in_ggaa4(B, X, Y, Z))
if_4_in_ggaa4(true_0, X, Y, 0_0) -> if_4_out_ggaa4(true_0, X, Y, 0_0)
if_4_in_ggaa4(false_0, X, Y, s_11(Z)) -> if_if_4_in_1_ggaa4(X, Y, Z, p_2_in_ga2(X, X1))
p_2_in_ga2(0_0, 0_0) -> p_2_out_ga2(0_0, 0_0)
p_2_in_ga2(s_11(X), X) -> p_2_out_ga2(s_11(X), X)
if_if_4_in_1_ggaa4(X, Y, Z, p_2_out_ga2(X, X1)) -> if_if_4_in_2_ggaa5(X, Y, Z, X1, minus_3_in_gaa3(X1, Y, Z))
if_if_4_in_2_ggaa5(X, Y, Z, X1, minus_3_out_gaa3(X1, Y, Z)) -> if_4_out_ggaa4(false_0, X, Y, s_11(Z))
if_minus_3_in_2_gaa5(X, Y, Z, B, if_4_out_ggaa4(B, X, Y, Z)) -> minus_3_out_gaa3(X, Y, Z)

The argument filtering Pi contains the following mapping:
minus_3_in_gaa3(x1, x2, x3)  =  minus_3_in_gaa1(x1)
0_0  =  0_0
s_11(x1)  =  s_11(x1)
true_0  =  true_0
false_0  =  false_0
if_minus_3_in_1_gaa4(x1, x2, x3, x4)  =  if_minus_3_in_1_gaa2(x1, x4)
le_3_in_gaa3(x1, x2, x3)  =  le_3_in_gaa1(x1)
le_3_out_gaa3(x1, x2, x3)  =  le_3_out_gaa1(x3)
if_le_3_in_1_gaa4(x1, x2, x3, x4)  =  if_le_3_in_1_gaa1(x4)
if_minus_3_in_2_gaa5(x1, x2, x3, x4, x5)  =  if_minus_3_in_2_gaa1(x5)
if_4_in_ggaa4(x1, x2, x3, x4)  =  if_4_in_ggaa2(x1, x2)
if_4_out_ggaa4(x1, x2, x3, x4)  =  if_4_out_ggaa1(x4)
if_if_4_in_1_ggaa4(x1, x2, x3, x4)  =  if_if_4_in_1_ggaa1(x4)
p_2_in_ga2(x1, x2)  =  p_2_in_ga1(x1)
p_2_out_ga2(x1, x2)  =  p_2_out_ga1(x2)
if_if_4_in_2_ggaa5(x1, x2, x3, x4, x5)  =  if_if_4_in_2_ggaa1(x5)
minus_3_out_gaa3(x1, x2, x3)  =  minus_3_out_gaa1(x3)
IF_LE_3_IN_1_GAA4(x1, x2, x3, x4)  =  IF_LE_3_IN_1_GAA1(x4)
IF_MINUS_3_IN_1_GAA4(x1, x2, x3, x4)  =  IF_MINUS_3_IN_1_GAA2(x1, x4)
LE_3_IN_GAA3(x1, x2, x3)  =  LE_3_IN_GAA1(x1)
IF_IF_4_IN_2_GGAA5(x1, x2, x3, x4, x5)  =  IF_IF_4_IN_2_GGAA1(x5)
P_2_IN_GA2(x1, x2)  =  P_2_IN_GA1(x1)
IF_IF_4_IN_1_GGAA4(x1, x2, x3, x4)  =  IF_IF_4_IN_1_GGAA1(x4)
IF_4_IN_GGAA4(x1, x2, x3, x4)  =  IF_4_IN_GGAA2(x1, x2)
IF_MINUS_3_IN_2_GAA5(x1, x2, x3, x4, x5)  =  IF_MINUS_3_IN_2_GAA1(x5)
MINUS_3_IN_GAA3(x1, x2, x3)  =  MINUS_3_IN_GAA1(x1)

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

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

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

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

The TRS R consists of the following rules:

minus_3_in_gaa3(X, Y, Z) -> if_minus_3_in_1_gaa4(X, Y, Z, le_3_in_gaa3(X, Y, B))
le_3_in_gaa3(0_0, Y, true_0) -> le_3_out_gaa3(0_0, Y, true_0)
le_3_in_gaa3(s_11(X), 0_0, false_0) -> le_3_out_gaa3(s_11(X), 0_0, false_0)
le_3_in_gaa3(s_11(X), s_11(Y), B) -> if_le_3_in_1_gaa4(X, Y, B, le_3_in_gaa3(X, Y, B))
if_le_3_in_1_gaa4(X, Y, B, le_3_out_gaa3(X, Y, B)) -> le_3_out_gaa3(s_11(X), s_11(Y), B)
if_minus_3_in_1_gaa4(X, Y, Z, le_3_out_gaa3(X, Y, B)) -> if_minus_3_in_2_gaa5(X, Y, Z, B, if_4_in_ggaa4(B, X, Y, Z))
if_4_in_ggaa4(true_0, X, Y, 0_0) -> if_4_out_ggaa4(true_0, X, Y, 0_0)
if_4_in_ggaa4(false_0, X, Y, s_11(Z)) -> if_if_4_in_1_ggaa4(X, Y, Z, p_2_in_ga2(X, X1))
p_2_in_ga2(0_0, 0_0) -> p_2_out_ga2(0_0, 0_0)
p_2_in_ga2(s_11(X), X) -> p_2_out_ga2(s_11(X), X)
if_if_4_in_1_ggaa4(X, Y, Z, p_2_out_ga2(X, X1)) -> if_if_4_in_2_ggaa5(X, Y, Z, X1, minus_3_in_gaa3(X1, Y, Z))
if_if_4_in_2_ggaa5(X, Y, Z, X1, minus_3_out_gaa3(X1, Y, Z)) -> if_4_out_ggaa4(false_0, X, Y, s_11(Z))
if_minus_3_in_2_gaa5(X, Y, Z, B, if_4_out_ggaa4(B, X, Y, Z)) -> minus_3_out_gaa3(X, Y, Z)

The argument filtering Pi contains the following mapping:
minus_3_in_gaa3(x1, x2, x3)  =  minus_3_in_gaa1(x1)
0_0  =  0_0
s_11(x1)  =  s_11(x1)
true_0  =  true_0
false_0  =  false_0
if_minus_3_in_1_gaa4(x1, x2, x3, x4)  =  if_minus_3_in_1_gaa2(x1, x4)
le_3_in_gaa3(x1, x2, x3)  =  le_3_in_gaa1(x1)
le_3_out_gaa3(x1, x2, x3)  =  le_3_out_gaa1(x3)
if_le_3_in_1_gaa4(x1, x2, x3, x4)  =  if_le_3_in_1_gaa1(x4)
if_minus_3_in_2_gaa5(x1, x2, x3, x4, x5)  =  if_minus_3_in_2_gaa1(x5)
if_4_in_ggaa4(x1, x2, x3, x4)  =  if_4_in_ggaa2(x1, x2)
if_4_out_ggaa4(x1, x2, x3, x4)  =  if_4_out_ggaa1(x4)
if_if_4_in_1_ggaa4(x1, x2, x3, x4)  =  if_if_4_in_1_ggaa1(x4)
p_2_in_ga2(x1, x2)  =  p_2_in_ga1(x1)
p_2_out_ga2(x1, x2)  =  p_2_out_ga1(x2)
if_if_4_in_2_ggaa5(x1, x2, x3, x4, x5)  =  if_if_4_in_2_ggaa1(x5)
minus_3_out_gaa3(x1, x2, x3)  =  minus_3_out_gaa1(x3)
LE_3_IN_GAA3(x1, x2, x3)  =  LE_3_IN_GAA1(x1)

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

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

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

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

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

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

LE_3_IN_GAA1(s_11(X)) -> LE_3_IN_GAA1(X)

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_GAA1}.
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

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

IF_IF_4_IN_1_GGAA4(X, Y, Z, p_2_out_ga2(X, X1)) -> MINUS_3_IN_GAA3(X1, Y, Z)
IF_MINUS_3_IN_1_GAA4(X, Y, Z, le_3_out_gaa3(X, Y, B)) -> IF_4_IN_GGAA4(B, X, Y, Z)
MINUS_3_IN_GAA3(X, Y, Z) -> IF_MINUS_3_IN_1_GAA4(X, Y, Z, le_3_in_gaa3(X, Y, B))
IF_4_IN_GGAA4(false_0, X, Y, s_11(Z)) -> IF_IF_4_IN_1_GGAA4(X, Y, Z, p_2_in_ga2(X, X1))

The TRS R consists of the following rules:

minus_3_in_gaa3(X, Y, Z) -> if_minus_3_in_1_gaa4(X, Y, Z, le_3_in_gaa3(X, Y, B))
le_3_in_gaa3(0_0, Y, true_0) -> le_3_out_gaa3(0_0, Y, true_0)
le_3_in_gaa3(s_11(X), 0_0, false_0) -> le_3_out_gaa3(s_11(X), 0_0, false_0)
le_3_in_gaa3(s_11(X), s_11(Y), B) -> if_le_3_in_1_gaa4(X, Y, B, le_3_in_gaa3(X, Y, B))
if_le_3_in_1_gaa4(X, Y, B, le_3_out_gaa3(X, Y, B)) -> le_3_out_gaa3(s_11(X), s_11(Y), B)
if_minus_3_in_1_gaa4(X, Y, Z, le_3_out_gaa3(X, Y, B)) -> if_minus_3_in_2_gaa5(X, Y, Z, B, if_4_in_ggaa4(B, X, Y, Z))
if_4_in_ggaa4(true_0, X, Y, 0_0) -> if_4_out_ggaa4(true_0, X, Y, 0_0)
if_4_in_ggaa4(false_0, X, Y, s_11(Z)) -> if_if_4_in_1_ggaa4(X, Y, Z, p_2_in_ga2(X, X1))
p_2_in_ga2(0_0, 0_0) -> p_2_out_ga2(0_0, 0_0)
p_2_in_ga2(s_11(X), X) -> p_2_out_ga2(s_11(X), X)
if_if_4_in_1_ggaa4(X, Y, Z, p_2_out_ga2(X, X1)) -> if_if_4_in_2_ggaa5(X, Y, Z, X1, minus_3_in_gaa3(X1, Y, Z))
if_if_4_in_2_ggaa5(X, Y, Z, X1, minus_3_out_gaa3(X1, Y, Z)) -> if_4_out_ggaa4(false_0, X, Y, s_11(Z))
if_minus_3_in_2_gaa5(X, Y, Z, B, if_4_out_ggaa4(B, X, Y, Z)) -> minus_3_out_gaa3(X, Y, Z)

The argument filtering Pi contains the following mapping:
minus_3_in_gaa3(x1, x2, x3)  =  minus_3_in_gaa1(x1)
0_0  =  0_0
s_11(x1)  =  s_11(x1)
true_0  =  true_0
false_0  =  false_0
if_minus_3_in_1_gaa4(x1, x2, x3, x4)  =  if_minus_3_in_1_gaa2(x1, x4)
le_3_in_gaa3(x1, x2, x3)  =  le_3_in_gaa1(x1)
le_3_out_gaa3(x1, x2, x3)  =  le_3_out_gaa1(x3)
if_le_3_in_1_gaa4(x1, x2, x3, x4)  =  if_le_3_in_1_gaa1(x4)
if_minus_3_in_2_gaa5(x1, x2, x3, x4, x5)  =  if_minus_3_in_2_gaa1(x5)
if_4_in_ggaa4(x1, x2, x3, x4)  =  if_4_in_ggaa2(x1, x2)
if_4_out_ggaa4(x1, x2, x3, x4)  =  if_4_out_ggaa1(x4)
if_if_4_in_1_ggaa4(x1, x2, x3, x4)  =  if_if_4_in_1_ggaa1(x4)
p_2_in_ga2(x1, x2)  =  p_2_in_ga1(x1)
p_2_out_ga2(x1, x2)  =  p_2_out_ga1(x2)
if_if_4_in_2_ggaa5(x1, x2, x3, x4, x5)  =  if_if_4_in_2_ggaa1(x5)
minus_3_out_gaa3(x1, x2, x3)  =  minus_3_out_gaa1(x3)
IF_MINUS_3_IN_1_GAA4(x1, x2, x3, x4)  =  IF_MINUS_3_IN_1_GAA2(x1, x4)
IF_IF_4_IN_1_GGAA4(x1, x2, x3, x4)  =  IF_IF_4_IN_1_GGAA1(x4)
IF_4_IN_GGAA4(x1, x2, x3, x4)  =  IF_4_IN_GGAA2(x1, x2)
MINUS_3_IN_GAA3(x1, x2, x3)  =  MINUS_3_IN_GAA1(x1)

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

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

IF_IF_4_IN_1_GGAA4(X, Y, Z, p_2_out_ga2(X, X1)) -> MINUS_3_IN_GAA3(X1, Y, Z)
IF_MINUS_3_IN_1_GAA4(X, Y, Z, le_3_out_gaa3(X, Y, B)) -> IF_4_IN_GGAA4(B, X, Y, Z)
MINUS_3_IN_GAA3(X, Y, Z) -> IF_MINUS_3_IN_1_GAA4(X, Y, Z, le_3_in_gaa3(X, Y, B))
IF_4_IN_GGAA4(false_0, X, Y, s_11(Z)) -> IF_IF_4_IN_1_GGAA4(X, Y, Z, p_2_in_ga2(X, X1))

The TRS R consists of the following rules:

le_3_in_gaa3(0_0, Y, true_0) -> le_3_out_gaa3(0_0, Y, true_0)
le_3_in_gaa3(s_11(X), 0_0, false_0) -> le_3_out_gaa3(s_11(X), 0_0, false_0)
le_3_in_gaa3(s_11(X), s_11(Y), B) -> if_le_3_in_1_gaa4(X, Y, B, le_3_in_gaa3(X, Y, B))
p_2_in_ga2(0_0, 0_0) -> p_2_out_ga2(0_0, 0_0)
p_2_in_ga2(s_11(X), X) -> p_2_out_ga2(s_11(X), X)
if_le_3_in_1_gaa4(X, Y, B, le_3_out_gaa3(X, Y, B)) -> le_3_out_gaa3(s_11(X), s_11(Y), B)

The argument filtering Pi contains the following mapping:
0_0  =  0_0
s_11(x1)  =  s_11(x1)
true_0  =  true_0
false_0  =  false_0
le_3_in_gaa3(x1, x2, x3)  =  le_3_in_gaa1(x1)
le_3_out_gaa3(x1, x2, x3)  =  le_3_out_gaa1(x3)
if_le_3_in_1_gaa4(x1, x2, x3, x4)  =  if_le_3_in_1_gaa1(x4)
p_2_in_ga2(x1, x2)  =  p_2_in_ga1(x1)
p_2_out_ga2(x1, x2)  =  p_2_out_ga1(x2)
IF_MINUS_3_IN_1_GAA4(x1, x2, x3, x4)  =  IF_MINUS_3_IN_1_GAA2(x1, x4)
IF_IF_4_IN_1_GGAA4(x1, x2, x3, x4)  =  IF_IF_4_IN_1_GGAA1(x4)
IF_4_IN_GGAA4(x1, x2, x3, x4)  =  IF_4_IN_GGAA2(x1, x2)
MINUS_3_IN_GAA3(x1, x2, x3)  =  MINUS_3_IN_GAA1(x1)

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
                        ↳ RuleRemovalProof

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

IF_IF_4_IN_1_GGAA1(p_2_out_ga1(X1)) -> MINUS_3_IN_GAA1(X1)
IF_MINUS_3_IN_1_GAA2(X, le_3_out_gaa1(B)) -> IF_4_IN_GGAA2(B, X)
MINUS_3_IN_GAA1(X) -> IF_MINUS_3_IN_1_GAA2(X, le_3_in_gaa1(X))
IF_4_IN_GGAA2(false_0, X) -> IF_IF_4_IN_1_GGAA1(p_2_in_ga1(X))

The TRS R consists of the following rules:

le_3_in_gaa1(0_0) -> le_3_out_gaa1(true_0)
le_3_in_gaa1(s_11(X)) -> le_3_out_gaa1(false_0)
le_3_in_gaa1(s_11(X)) -> if_le_3_in_1_gaa1(le_3_in_gaa1(X))
p_2_in_ga1(0_0) -> p_2_out_ga1(0_0)
p_2_in_ga1(s_11(X)) -> p_2_out_ga1(X)
if_le_3_in_1_gaa1(le_3_out_gaa1(B)) -> le_3_out_gaa1(B)

The set Q consists of the following terms:

le_3_in_gaa1(x0)
p_2_in_ga1(x0)
if_le_3_in_1_gaa1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {MINUS_3_IN_GAA1, IF_IF_4_IN_1_GGAA1, IF_4_IN_GGAA2, IF_MINUS_3_IN_1_GAA2}.
By using a polynomial ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.

Strictly oriented rules of the TRS R:

le_3_in_gaa1(0_0) -> le_3_out_gaa1(true_0)
le_3_in_gaa1(s_11(X)) -> if_le_3_in_1_gaa1(le_3_in_gaa1(X))
p_2_in_ga1(s_11(X)) -> p_2_out_ga1(X)

Used ordering: POLO with Polynomial interpretation:

POL(0_0) = 2   
POL(p_2_out_ga1(x1)) = 2·x1   
POL(false_0) = 2   
POL(true_0) = 1   
POL(le_3_out_gaa1(x1)) = 1 + x1   
POL(IF_MINUS_3_IN_1_GAA2(x1, x2)) = x1 + x2   
POL(if_le_3_in_1_gaa1(x1)) = x1   
POL(MINUS_3_IN_GAA1(x1)) = 1 + 2·x1   
POL(le_3_in_gaa1(x1)) = 1 + x1   
POL(p_2_in_ga1(x1)) = 2 + x1   
POL(s_11(x1)) = 2 + 2·x1   
POL(IF_IF_4_IN_1_GGAA1(x1)) = 1 + x1   
POL(IF_4_IN_GGAA2(x1, x2)) = 1 + x1 + x2   



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

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

IF_IF_4_IN_1_GGAA1(p_2_out_ga1(X1)) -> MINUS_3_IN_GAA1(X1)
IF_MINUS_3_IN_1_GAA2(X, le_3_out_gaa1(B)) -> IF_4_IN_GGAA2(B, X)
MINUS_3_IN_GAA1(X) -> IF_MINUS_3_IN_1_GAA2(X, le_3_in_gaa1(X))
IF_4_IN_GGAA2(false_0, X) -> IF_IF_4_IN_1_GGAA1(p_2_in_ga1(X))

The TRS R consists of the following rules:

le_3_in_gaa1(s_11(X)) -> le_3_out_gaa1(false_0)
p_2_in_ga1(0_0) -> p_2_out_ga1(0_0)
if_le_3_in_1_gaa1(le_3_out_gaa1(B)) -> le_3_out_gaa1(B)

The set Q consists of the following terms:

le_3_in_gaa1(x0)
p_2_in_ga1(x0)
if_le_3_in_1_gaa1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {MINUS_3_IN_GAA1, IF_IF_4_IN_1_GGAA1, IF_4_IN_GGAA2, IF_MINUS_3_IN_1_GAA2}.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, we can delete all non-usable rules from R.

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

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

IF_IF_4_IN_1_GGAA1(p_2_out_ga1(X1)) -> MINUS_3_IN_GAA1(X1)
IF_MINUS_3_IN_1_GAA2(X, le_3_out_gaa1(B)) -> IF_4_IN_GGAA2(B, X)
MINUS_3_IN_GAA1(X) -> IF_MINUS_3_IN_1_GAA2(X, le_3_in_gaa1(X))
IF_4_IN_GGAA2(false_0, X) -> IF_IF_4_IN_1_GGAA1(p_2_in_ga1(X))

The TRS R consists of the following rules:

p_2_in_ga1(0_0) -> p_2_out_ga1(0_0)
le_3_in_gaa1(s_11(X)) -> le_3_out_gaa1(false_0)

The set Q consists of the following terms:

le_3_in_gaa1(x0)
p_2_in_ga1(x0)
if_le_3_in_1_gaa1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {MINUS_3_IN_GAA1, IF_IF_4_IN_1_GGAA1, IF_4_IN_GGAA2, IF_MINUS_3_IN_1_GAA2}.
By using a polynomial ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

IF_MINUS_3_IN_1_GAA2(X, le_3_out_gaa1(B)) -> IF_4_IN_GGAA2(B, X)

Strictly oriented rules of the TRS R:

le_3_in_gaa1(s_11(X)) -> le_3_out_gaa1(false_0)

Used ordering: POLO with Polynomial interpretation:

POL(0_0) = 0   
POL(p_2_out_ga1(x1)) = 2·x1   
POL(false_0) = 1   
POL(MINUS_3_IN_GAA1(x1)) = 1 + 2·x1   
POL(le_3_in_gaa1(x1)) = 1 + x1   
POL(p_2_in_ga1(x1)) = x1   
POL(s_11(x1)) = 2 + x1   
POL(le_3_out_gaa1(x1)) = 1 + x1   
POL(IF_IF_4_IN_1_GGAA1(x1)) = 1 + x1   
POL(IF_MINUS_3_IN_1_GAA2(x1, x2)) = x1 + x2   
POL(IF_4_IN_GGAA2(x1, x2)) = x1 + x2   



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

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

IF_IF_4_IN_1_GGAA1(p_2_out_ga1(X1)) -> MINUS_3_IN_GAA1(X1)
MINUS_3_IN_GAA1(X) -> IF_MINUS_3_IN_1_GAA2(X, le_3_in_gaa1(X))
IF_4_IN_GGAA2(false_0, X) -> IF_IF_4_IN_1_GGAA1(p_2_in_ga1(X))

The TRS R consists of the following rules:

p_2_in_ga1(0_0) -> p_2_out_ga1(0_0)

The set Q consists of the following terms:

le_3_in_gaa1(x0)
p_2_in_ga1(x0)
if_le_3_in_1_gaa1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {MINUS_3_IN_GAA1, IF_IF_4_IN_1_GGAA1, IF_MINUS_3_IN_1_GAA2, IF_4_IN_GGAA2}.
The approximation of the Dependency Graph contains 0 SCCs with 3 less nodes.