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



↳ PROLOG
  ↳ PrologToPiTRSProof

factor2(.2(X, {}0), X).
factor2(.2(X, .2(Y, Xs)), T) :- times3(X, Y, Z), factor2(.2(Z, Xs), T).
times3(00, X, 00).
times3(s1(X), Y, Z) :- times3(X, Y, XY), plus3(XY, Y, Z).
plus3(00, X, X).
plus3(s1(X), Y, s1(Z)) :- plus3(X, Y, Z).


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


factor_2_in_ga2(._22(X, []_0), X) -> factor_2_out_ga2(._22(X, []_0), X)
factor_2_in_ga2(._22(X, ._22(Y, Xs)), T) -> if_factor_2_in_1_ga5(X, Y, Xs, T, times_3_in_gga3(X, Y, Z))
times_3_in_gga3(0_0, X_, 0_0) -> times_3_out_gga3(0_0, X_, 0_0)
times_3_in_gga3(s_11(X), Y, Z) -> if_times_3_in_1_gga4(X, Y, Z, times_3_in_gga3(X, Y, XY))
if_times_3_in_1_gga4(X, Y, Z, times_3_out_gga3(X, Y, XY)) -> if_times_3_in_2_gga5(X, Y, Z, XY, plus_3_in_gga3(XY, Y, Z))
plus_3_in_gga3(0_0, X, X) -> plus_3_out_gga3(0_0, X, X)
plus_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_plus_3_in_1_gga4(X, Y, Z, plus_3_in_gga3(X, Y, Z))
if_plus_3_in_1_gga4(X, Y, Z, plus_3_out_gga3(X, Y, Z)) -> plus_3_out_gga3(s_11(X), Y, s_11(Z))
if_times_3_in_2_gga5(X, Y, Z, XY, plus_3_out_gga3(XY, Y, Z)) -> times_3_out_gga3(s_11(X), Y, Z)
if_factor_2_in_1_ga5(X, Y, Xs, T, times_3_out_gga3(X, Y, Z)) -> if_factor_2_in_2_ga6(X, Y, Xs, T, Z, factor_2_in_ga2(._22(Z, Xs), T))
if_factor_2_in_2_ga6(X, Y, Xs, T, Z, factor_2_out_ga2(._22(Z, Xs), T)) -> factor_2_out_ga2(._22(X, ._22(Y, Xs)), T)

The argument filtering Pi contains the following mapping:
factor_2_in_ga2(x1, x2)  =  factor_2_in_ga1(x1)
._22(x1, x2)  =  ._22(x1, x2)
[]_0  =  []_0
0_0  =  0_0
s_11(x1)  =  s_11(x1)
factor_2_out_ga2(x1, x2)  =  factor_2_out_ga1(x2)
if_factor_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_factor_2_in_1_ga2(x3, x5)
times_3_in_gga3(x1, x2, x3)  =  times_3_in_gga2(x1, x2)
times_3_out_gga3(x1, x2, x3)  =  times_3_out_gga1(x3)
if_times_3_in_1_gga4(x1, x2, x3, x4)  =  if_times_3_in_1_gga2(x2, x4)
if_times_3_in_2_gga5(x1, x2, x3, x4, x5)  =  if_times_3_in_2_gga1(x5)
plus_3_in_gga3(x1, x2, x3)  =  plus_3_in_gga2(x1, x2)
plus_3_out_gga3(x1, x2, x3)  =  plus_3_out_gga1(x3)
if_plus_3_in_1_gga4(x1, x2, x3, x4)  =  if_plus_3_in_1_gga1(x4)
if_factor_2_in_2_ga6(x1, x2, x3, x4, x5, x6)  =  if_factor_2_in_2_ga1(x6)

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:

factor_2_in_ga2(._22(X, []_0), X) -> factor_2_out_ga2(._22(X, []_0), X)
factor_2_in_ga2(._22(X, ._22(Y, Xs)), T) -> if_factor_2_in_1_ga5(X, Y, Xs, T, times_3_in_gga3(X, Y, Z))
times_3_in_gga3(0_0, X_, 0_0) -> times_3_out_gga3(0_0, X_, 0_0)
times_3_in_gga3(s_11(X), Y, Z) -> if_times_3_in_1_gga4(X, Y, Z, times_3_in_gga3(X, Y, XY))
if_times_3_in_1_gga4(X, Y, Z, times_3_out_gga3(X, Y, XY)) -> if_times_3_in_2_gga5(X, Y, Z, XY, plus_3_in_gga3(XY, Y, Z))
plus_3_in_gga3(0_0, X, X) -> plus_3_out_gga3(0_0, X, X)
plus_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_plus_3_in_1_gga4(X, Y, Z, plus_3_in_gga3(X, Y, Z))
if_plus_3_in_1_gga4(X, Y, Z, plus_3_out_gga3(X, Y, Z)) -> plus_3_out_gga3(s_11(X), Y, s_11(Z))
if_times_3_in_2_gga5(X, Y, Z, XY, plus_3_out_gga3(XY, Y, Z)) -> times_3_out_gga3(s_11(X), Y, Z)
if_factor_2_in_1_ga5(X, Y, Xs, T, times_3_out_gga3(X, Y, Z)) -> if_factor_2_in_2_ga6(X, Y, Xs, T, Z, factor_2_in_ga2(._22(Z, Xs), T))
if_factor_2_in_2_ga6(X, Y, Xs, T, Z, factor_2_out_ga2(._22(Z, Xs), T)) -> factor_2_out_ga2(._22(X, ._22(Y, Xs)), T)

The argument filtering Pi contains the following mapping:
factor_2_in_ga2(x1, x2)  =  factor_2_in_ga1(x1)
._22(x1, x2)  =  ._22(x1, x2)
[]_0  =  []_0
0_0  =  0_0
s_11(x1)  =  s_11(x1)
factor_2_out_ga2(x1, x2)  =  factor_2_out_ga1(x2)
if_factor_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_factor_2_in_1_ga2(x3, x5)
times_3_in_gga3(x1, x2, x3)  =  times_3_in_gga2(x1, x2)
times_3_out_gga3(x1, x2, x3)  =  times_3_out_gga1(x3)
if_times_3_in_1_gga4(x1, x2, x3, x4)  =  if_times_3_in_1_gga2(x2, x4)
if_times_3_in_2_gga5(x1, x2, x3, x4, x5)  =  if_times_3_in_2_gga1(x5)
plus_3_in_gga3(x1, x2, x3)  =  plus_3_in_gga2(x1, x2)
plus_3_out_gga3(x1, x2, x3)  =  plus_3_out_gga1(x3)
if_plus_3_in_1_gga4(x1, x2, x3, x4)  =  if_plus_3_in_1_gga1(x4)
if_factor_2_in_2_ga6(x1, x2, x3, x4, x5, x6)  =  if_factor_2_in_2_ga1(x6)


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

FACTOR_2_IN_GA2(._22(X, ._22(Y, Xs)), T) -> IF_FACTOR_2_IN_1_GA5(X, Y, Xs, T, times_3_in_gga3(X, Y, Z))
FACTOR_2_IN_GA2(._22(X, ._22(Y, Xs)), T) -> TIMES_3_IN_GGA3(X, Y, Z)
TIMES_3_IN_GGA3(s_11(X), Y, Z) -> IF_TIMES_3_IN_1_GGA4(X, Y, Z, times_3_in_gga3(X, Y, XY))
TIMES_3_IN_GGA3(s_11(X), Y, Z) -> TIMES_3_IN_GGA3(X, Y, XY)
IF_TIMES_3_IN_1_GGA4(X, Y, Z, times_3_out_gga3(X, Y, XY)) -> IF_TIMES_3_IN_2_GGA5(X, Y, Z, XY, plus_3_in_gga3(XY, Y, Z))
IF_TIMES_3_IN_1_GGA4(X, Y, Z, times_3_out_gga3(X, Y, XY)) -> PLUS_3_IN_GGA3(XY, Y, Z)
PLUS_3_IN_GGA3(s_11(X), Y, s_11(Z)) -> IF_PLUS_3_IN_1_GGA4(X, Y, Z, plus_3_in_gga3(X, Y, Z))
PLUS_3_IN_GGA3(s_11(X), Y, s_11(Z)) -> PLUS_3_IN_GGA3(X, Y, Z)
IF_FACTOR_2_IN_1_GA5(X, Y, Xs, T, times_3_out_gga3(X, Y, Z)) -> IF_FACTOR_2_IN_2_GA6(X, Y, Xs, T, Z, factor_2_in_ga2(._22(Z, Xs), T))
IF_FACTOR_2_IN_1_GA5(X, Y, Xs, T, times_3_out_gga3(X, Y, Z)) -> FACTOR_2_IN_GA2(._22(Z, Xs), T)

The TRS R consists of the following rules:

factor_2_in_ga2(._22(X, []_0), X) -> factor_2_out_ga2(._22(X, []_0), X)
factor_2_in_ga2(._22(X, ._22(Y, Xs)), T) -> if_factor_2_in_1_ga5(X, Y, Xs, T, times_3_in_gga3(X, Y, Z))
times_3_in_gga3(0_0, X_, 0_0) -> times_3_out_gga3(0_0, X_, 0_0)
times_3_in_gga3(s_11(X), Y, Z) -> if_times_3_in_1_gga4(X, Y, Z, times_3_in_gga3(X, Y, XY))
if_times_3_in_1_gga4(X, Y, Z, times_3_out_gga3(X, Y, XY)) -> if_times_3_in_2_gga5(X, Y, Z, XY, plus_3_in_gga3(XY, Y, Z))
plus_3_in_gga3(0_0, X, X) -> plus_3_out_gga3(0_0, X, X)
plus_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_plus_3_in_1_gga4(X, Y, Z, plus_3_in_gga3(X, Y, Z))
if_plus_3_in_1_gga4(X, Y, Z, plus_3_out_gga3(X, Y, Z)) -> plus_3_out_gga3(s_11(X), Y, s_11(Z))
if_times_3_in_2_gga5(X, Y, Z, XY, plus_3_out_gga3(XY, Y, Z)) -> times_3_out_gga3(s_11(X), Y, Z)
if_factor_2_in_1_ga5(X, Y, Xs, T, times_3_out_gga3(X, Y, Z)) -> if_factor_2_in_2_ga6(X, Y, Xs, T, Z, factor_2_in_ga2(._22(Z, Xs), T))
if_factor_2_in_2_ga6(X, Y, Xs, T, Z, factor_2_out_ga2(._22(Z, Xs), T)) -> factor_2_out_ga2(._22(X, ._22(Y, Xs)), T)

The argument filtering Pi contains the following mapping:
factor_2_in_ga2(x1, x2)  =  factor_2_in_ga1(x1)
._22(x1, x2)  =  ._22(x1, x2)
[]_0  =  []_0
0_0  =  0_0
s_11(x1)  =  s_11(x1)
factor_2_out_ga2(x1, x2)  =  factor_2_out_ga1(x2)
if_factor_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_factor_2_in_1_ga2(x3, x5)
times_3_in_gga3(x1, x2, x3)  =  times_3_in_gga2(x1, x2)
times_3_out_gga3(x1, x2, x3)  =  times_3_out_gga1(x3)
if_times_3_in_1_gga4(x1, x2, x3, x4)  =  if_times_3_in_1_gga2(x2, x4)
if_times_3_in_2_gga5(x1, x2, x3, x4, x5)  =  if_times_3_in_2_gga1(x5)
plus_3_in_gga3(x1, x2, x3)  =  plus_3_in_gga2(x1, x2)
plus_3_out_gga3(x1, x2, x3)  =  plus_3_out_gga1(x3)
if_plus_3_in_1_gga4(x1, x2, x3, x4)  =  if_plus_3_in_1_gga1(x4)
if_factor_2_in_2_ga6(x1, x2, x3, x4, x5, x6)  =  if_factor_2_in_2_ga1(x6)
IF_TIMES_3_IN_1_GGA4(x1, x2, x3, x4)  =  IF_TIMES_3_IN_1_GGA2(x2, x4)
IF_TIMES_3_IN_2_GGA5(x1, x2, x3, x4, x5)  =  IF_TIMES_3_IN_2_GGA1(x5)
FACTOR_2_IN_GA2(x1, x2)  =  FACTOR_2_IN_GA1(x1)
IF_PLUS_3_IN_1_GGA4(x1, x2, x3, x4)  =  IF_PLUS_3_IN_1_GGA1(x4)
PLUS_3_IN_GGA3(x1, x2, x3)  =  PLUS_3_IN_GGA2(x1, x2)
IF_FACTOR_2_IN_2_GA6(x1, x2, x3, x4, x5, x6)  =  IF_FACTOR_2_IN_2_GA1(x6)
TIMES_3_IN_GGA3(x1, x2, x3)  =  TIMES_3_IN_GGA2(x1, x2)
IF_FACTOR_2_IN_1_GA5(x1, x2, x3, x4, x5)  =  IF_FACTOR_2_IN_1_GA2(x3, x5)

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:

FACTOR_2_IN_GA2(._22(X, ._22(Y, Xs)), T) -> IF_FACTOR_2_IN_1_GA5(X, Y, Xs, T, times_3_in_gga3(X, Y, Z))
FACTOR_2_IN_GA2(._22(X, ._22(Y, Xs)), T) -> TIMES_3_IN_GGA3(X, Y, Z)
TIMES_3_IN_GGA3(s_11(X), Y, Z) -> IF_TIMES_3_IN_1_GGA4(X, Y, Z, times_3_in_gga3(X, Y, XY))
TIMES_3_IN_GGA3(s_11(X), Y, Z) -> TIMES_3_IN_GGA3(X, Y, XY)
IF_TIMES_3_IN_1_GGA4(X, Y, Z, times_3_out_gga3(X, Y, XY)) -> IF_TIMES_3_IN_2_GGA5(X, Y, Z, XY, plus_3_in_gga3(XY, Y, Z))
IF_TIMES_3_IN_1_GGA4(X, Y, Z, times_3_out_gga3(X, Y, XY)) -> PLUS_3_IN_GGA3(XY, Y, Z)
PLUS_3_IN_GGA3(s_11(X), Y, s_11(Z)) -> IF_PLUS_3_IN_1_GGA4(X, Y, Z, plus_3_in_gga3(X, Y, Z))
PLUS_3_IN_GGA3(s_11(X), Y, s_11(Z)) -> PLUS_3_IN_GGA3(X, Y, Z)
IF_FACTOR_2_IN_1_GA5(X, Y, Xs, T, times_3_out_gga3(X, Y, Z)) -> IF_FACTOR_2_IN_2_GA6(X, Y, Xs, T, Z, factor_2_in_ga2(._22(Z, Xs), T))
IF_FACTOR_2_IN_1_GA5(X, Y, Xs, T, times_3_out_gga3(X, Y, Z)) -> FACTOR_2_IN_GA2(._22(Z, Xs), T)

The TRS R consists of the following rules:

factor_2_in_ga2(._22(X, []_0), X) -> factor_2_out_ga2(._22(X, []_0), X)
factor_2_in_ga2(._22(X, ._22(Y, Xs)), T) -> if_factor_2_in_1_ga5(X, Y, Xs, T, times_3_in_gga3(X, Y, Z))
times_3_in_gga3(0_0, X_, 0_0) -> times_3_out_gga3(0_0, X_, 0_0)
times_3_in_gga3(s_11(X), Y, Z) -> if_times_3_in_1_gga4(X, Y, Z, times_3_in_gga3(X, Y, XY))
if_times_3_in_1_gga4(X, Y, Z, times_3_out_gga3(X, Y, XY)) -> if_times_3_in_2_gga5(X, Y, Z, XY, plus_3_in_gga3(XY, Y, Z))
plus_3_in_gga3(0_0, X, X) -> plus_3_out_gga3(0_0, X, X)
plus_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_plus_3_in_1_gga4(X, Y, Z, plus_3_in_gga3(X, Y, Z))
if_plus_3_in_1_gga4(X, Y, Z, plus_3_out_gga3(X, Y, Z)) -> plus_3_out_gga3(s_11(X), Y, s_11(Z))
if_times_3_in_2_gga5(X, Y, Z, XY, plus_3_out_gga3(XY, Y, Z)) -> times_3_out_gga3(s_11(X), Y, Z)
if_factor_2_in_1_ga5(X, Y, Xs, T, times_3_out_gga3(X, Y, Z)) -> if_factor_2_in_2_ga6(X, Y, Xs, T, Z, factor_2_in_ga2(._22(Z, Xs), T))
if_factor_2_in_2_ga6(X, Y, Xs, T, Z, factor_2_out_ga2(._22(Z, Xs), T)) -> factor_2_out_ga2(._22(X, ._22(Y, Xs)), T)

The argument filtering Pi contains the following mapping:
factor_2_in_ga2(x1, x2)  =  factor_2_in_ga1(x1)
._22(x1, x2)  =  ._22(x1, x2)
[]_0  =  []_0
0_0  =  0_0
s_11(x1)  =  s_11(x1)
factor_2_out_ga2(x1, x2)  =  factor_2_out_ga1(x2)
if_factor_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_factor_2_in_1_ga2(x3, x5)
times_3_in_gga3(x1, x2, x3)  =  times_3_in_gga2(x1, x2)
times_3_out_gga3(x1, x2, x3)  =  times_3_out_gga1(x3)
if_times_3_in_1_gga4(x1, x2, x3, x4)  =  if_times_3_in_1_gga2(x2, x4)
if_times_3_in_2_gga5(x1, x2, x3, x4, x5)  =  if_times_3_in_2_gga1(x5)
plus_3_in_gga3(x1, x2, x3)  =  plus_3_in_gga2(x1, x2)
plus_3_out_gga3(x1, x2, x3)  =  plus_3_out_gga1(x3)
if_plus_3_in_1_gga4(x1, x2, x3, x4)  =  if_plus_3_in_1_gga1(x4)
if_factor_2_in_2_ga6(x1, x2, x3, x4, x5, x6)  =  if_factor_2_in_2_ga1(x6)
IF_TIMES_3_IN_1_GGA4(x1, x2, x3, x4)  =  IF_TIMES_3_IN_1_GGA2(x2, x4)
IF_TIMES_3_IN_2_GGA5(x1, x2, x3, x4, x5)  =  IF_TIMES_3_IN_2_GGA1(x5)
FACTOR_2_IN_GA2(x1, x2)  =  FACTOR_2_IN_GA1(x1)
IF_PLUS_3_IN_1_GGA4(x1, x2, x3, x4)  =  IF_PLUS_3_IN_1_GGA1(x4)
PLUS_3_IN_GGA3(x1, x2, x3)  =  PLUS_3_IN_GGA2(x1, x2)
IF_FACTOR_2_IN_2_GA6(x1, x2, x3, x4, x5, x6)  =  IF_FACTOR_2_IN_2_GA1(x6)
TIMES_3_IN_GGA3(x1, x2, x3)  =  TIMES_3_IN_GGA2(x1, x2)
IF_FACTOR_2_IN_1_GA5(x1, x2, x3, x4, x5)  =  IF_FACTOR_2_IN_1_GA2(x3, x5)

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

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

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

The TRS R consists of the following rules:

factor_2_in_ga2(._22(X, []_0), X) -> factor_2_out_ga2(._22(X, []_0), X)
factor_2_in_ga2(._22(X, ._22(Y, Xs)), T) -> if_factor_2_in_1_ga5(X, Y, Xs, T, times_3_in_gga3(X, Y, Z))
times_3_in_gga3(0_0, X_, 0_0) -> times_3_out_gga3(0_0, X_, 0_0)
times_3_in_gga3(s_11(X), Y, Z) -> if_times_3_in_1_gga4(X, Y, Z, times_3_in_gga3(X, Y, XY))
if_times_3_in_1_gga4(X, Y, Z, times_3_out_gga3(X, Y, XY)) -> if_times_3_in_2_gga5(X, Y, Z, XY, plus_3_in_gga3(XY, Y, Z))
plus_3_in_gga3(0_0, X, X) -> plus_3_out_gga3(0_0, X, X)
plus_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_plus_3_in_1_gga4(X, Y, Z, plus_3_in_gga3(X, Y, Z))
if_plus_3_in_1_gga4(X, Y, Z, plus_3_out_gga3(X, Y, Z)) -> plus_3_out_gga3(s_11(X), Y, s_11(Z))
if_times_3_in_2_gga5(X, Y, Z, XY, plus_3_out_gga3(XY, Y, Z)) -> times_3_out_gga3(s_11(X), Y, Z)
if_factor_2_in_1_ga5(X, Y, Xs, T, times_3_out_gga3(X, Y, Z)) -> if_factor_2_in_2_ga6(X, Y, Xs, T, Z, factor_2_in_ga2(._22(Z, Xs), T))
if_factor_2_in_2_ga6(X, Y, Xs, T, Z, factor_2_out_ga2(._22(Z, Xs), T)) -> factor_2_out_ga2(._22(X, ._22(Y, Xs)), T)

The argument filtering Pi contains the following mapping:
factor_2_in_ga2(x1, x2)  =  factor_2_in_ga1(x1)
._22(x1, x2)  =  ._22(x1, x2)
[]_0  =  []_0
0_0  =  0_0
s_11(x1)  =  s_11(x1)
factor_2_out_ga2(x1, x2)  =  factor_2_out_ga1(x2)
if_factor_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_factor_2_in_1_ga2(x3, x5)
times_3_in_gga3(x1, x2, x3)  =  times_3_in_gga2(x1, x2)
times_3_out_gga3(x1, x2, x3)  =  times_3_out_gga1(x3)
if_times_3_in_1_gga4(x1, x2, x3, x4)  =  if_times_3_in_1_gga2(x2, x4)
if_times_3_in_2_gga5(x1, x2, x3, x4, x5)  =  if_times_3_in_2_gga1(x5)
plus_3_in_gga3(x1, x2, x3)  =  plus_3_in_gga2(x1, x2)
plus_3_out_gga3(x1, x2, x3)  =  plus_3_out_gga1(x3)
if_plus_3_in_1_gga4(x1, x2, x3, x4)  =  if_plus_3_in_1_gga1(x4)
if_factor_2_in_2_ga6(x1, x2, x3, x4, x5, x6)  =  if_factor_2_in_2_ga1(x6)
PLUS_3_IN_GGA3(x1, x2, x3)  =  PLUS_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:

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

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

PLUS_3_IN_GGA2(s_11(X), Y) -> PLUS_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 {PLUS_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:

TIMES_3_IN_GGA3(s_11(X), Y, Z) -> TIMES_3_IN_GGA3(X, Y, XY)

The TRS R consists of the following rules:

factor_2_in_ga2(._22(X, []_0), X) -> factor_2_out_ga2(._22(X, []_0), X)
factor_2_in_ga2(._22(X, ._22(Y, Xs)), T) -> if_factor_2_in_1_ga5(X, Y, Xs, T, times_3_in_gga3(X, Y, Z))
times_3_in_gga3(0_0, X_, 0_0) -> times_3_out_gga3(0_0, X_, 0_0)
times_3_in_gga3(s_11(X), Y, Z) -> if_times_3_in_1_gga4(X, Y, Z, times_3_in_gga3(X, Y, XY))
if_times_3_in_1_gga4(X, Y, Z, times_3_out_gga3(X, Y, XY)) -> if_times_3_in_2_gga5(X, Y, Z, XY, plus_3_in_gga3(XY, Y, Z))
plus_3_in_gga3(0_0, X, X) -> plus_3_out_gga3(0_0, X, X)
plus_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_plus_3_in_1_gga4(X, Y, Z, plus_3_in_gga3(X, Y, Z))
if_plus_3_in_1_gga4(X, Y, Z, plus_3_out_gga3(X, Y, Z)) -> plus_3_out_gga3(s_11(X), Y, s_11(Z))
if_times_3_in_2_gga5(X, Y, Z, XY, plus_3_out_gga3(XY, Y, Z)) -> times_3_out_gga3(s_11(X), Y, Z)
if_factor_2_in_1_ga5(X, Y, Xs, T, times_3_out_gga3(X, Y, Z)) -> if_factor_2_in_2_ga6(X, Y, Xs, T, Z, factor_2_in_ga2(._22(Z, Xs), T))
if_factor_2_in_2_ga6(X, Y, Xs, T, Z, factor_2_out_ga2(._22(Z, Xs), T)) -> factor_2_out_ga2(._22(X, ._22(Y, Xs)), T)

The argument filtering Pi contains the following mapping:
factor_2_in_ga2(x1, x2)  =  factor_2_in_ga1(x1)
._22(x1, x2)  =  ._22(x1, x2)
[]_0  =  []_0
0_0  =  0_0
s_11(x1)  =  s_11(x1)
factor_2_out_ga2(x1, x2)  =  factor_2_out_ga1(x2)
if_factor_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_factor_2_in_1_ga2(x3, x5)
times_3_in_gga3(x1, x2, x3)  =  times_3_in_gga2(x1, x2)
times_3_out_gga3(x1, x2, x3)  =  times_3_out_gga1(x3)
if_times_3_in_1_gga4(x1, x2, x3, x4)  =  if_times_3_in_1_gga2(x2, x4)
if_times_3_in_2_gga5(x1, x2, x3, x4, x5)  =  if_times_3_in_2_gga1(x5)
plus_3_in_gga3(x1, x2, x3)  =  plus_3_in_gga2(x1, x2)
plus_3_out_gga3(x1, x2, x3)  =  plus_3_out_gga1(x3)
if_plus_3_in_1_gga4(x1, x2, x3, x4)  =  if_plus_3_in_1_gga1(x4)
if_factor_2_in_2_ga6(x1, x2, x3, x4, x5, x6)  =  if_factor_2_in_2_ga1(x6)
TIMES_3_IN_GGA3(x1, x2, x3)  =  TIMES_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

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

TIMES_3_IN_GGA3(s_11(X), Y, Z) -> TIMES_3_IN_GGA3(X, Y, XY)

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

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

TIMES_3_IN_GGA2(s_11(X), Y) -> TIMES_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 {TIMES_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

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

IF_FACTOR_2_IN_1_GA5(X, Y, Xs, T, times_3_out_gga3(X, Y, Z)) -> FACTOR_2_IN_GA2(._22(Z, Xs), T)
FACTOR_2_IN_GA2(._22(X, ._22(Y, Xs)), T) -> IF_FACTOR_2_IN_1_GA5(X, Y, Xs, T, times_3_in_gga3(X, Y, Z))

The TRS R consists of the following rules:

factor_2_in_ga2(._22(X, []_0), X) -> factor_2_out_ga2(._22(X, []_0), X)
factor_2_in_ga2(._22(X, ._22(Y, Xs)), T) -> if_factor_2_in_1_ga5(X, Y, Xs, T, times_3_in_gga3(X, Y, Z))
times_3_in_gga3(0_0, X_, 0_0) -> times_3_out_gga3(0_0, X_, 0_0)
times_3_in_gga3(s_11(X), Y, Z) -> if_times_3_in_1_gga4(X, Y, Z, times_3_in_gga3(X, Y, XY))
if_times_3_in_1_gga4(X, Y, Z, times_3_out_gga3(X, Y, XY)) -> if_times_3_in_2_gga5(X, Y, Z, XY, plus_3_in_gga3(XY, Y, Z))
plus_3_in_gga3(0_0, X, X) -> plus_3_out_gga3(0_0, X, X)
plus_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_plus_3_in_1_gga4(X, Y, Z, plus_3_in_gga3(X, Y, Z))
if_plus_3_in_1_gga4(X, Y, Z, plus_3_out_gga3(X, Y, Z)) -> plus_3_out_gga3(s_11(X), Y, s_11(Z))
if_times_3_in_2_gga5(X, Y, Z, XY, plus_3_out_gga3(XY, Y, Z)) -> times_3_out_gga3(s_11(X), Y, Z)
if_factor_2_in_1_ga5(X, Y, Xs, T, times_3_out_gga3(X, Y, Z)) -> if_factor_2_in_2_ga6(X, Y, Xs, T, Z, factor_2_in_ga2(._22(Z, Xs), T))
if_factor_2_in_2_ga6(X, Y, Xs, T, Z, factor_2_out_ga2(._22(Z, Xs), T)) -> factor_2_out_ga2(._22(X, ._22(Y, Xs)), T)

The argument filtering Pi contains the following mapping:
factor_2_in_ga2(x1, x2)  =  factor_2_in_ga1(x1)
._22(x1, x2)  =  ._22(x1, x2)
[]_0  =  []_0
0_0  =  0_0
s_11(x1)  =  s_11(x1)
factor_2_out_ga2(x1, x2)  =  factor_2_out_ga1(x2)
if_factor_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_factor_2_in_1_ga2(x3, x5)
times_3_in_gga3(x1, x2, x3)  =  times_3_in_gga2(x1, x2)
times_3_out_gga3(x1, x2, x3)  =  times_3_out_gga1(x3)
if_times_3_in_1_gga4(x1, x2, x3, x4)  =  if_times_3_in_1_gga2(x2, x4)
if_times_3_in_2_gga5(x1, x2, x3, x4, x5)  =  if_times_3_in_2_gga1(x5)
plus_3_in_gga3(x1, x2, x3)  =  plus_3_in_gga2(x1, x2)
plus_3_out_gga3(x1, x2, x3)  =  plus_3_out_gga1(x3)
if_plus_3_in_1_gga4(x1, x2, x3, x4)  =  if_plus_3_in_1_gga1(x4)
if_factor_2_in_2_ga6(x1, x2, x3, x4, x5, x6)  =  if_factor_2_in_2_ga1(x6)
FACTOR_2_IN_GA2(x1, x2)  =  FACTOR_2_IN_GA1(x1)
IF_FACTOR_2_IN_1_GA5(x1, x2, x3, x4, x5)  =  IF_FACTOR_2_IN_1_GA2(x3, x5)

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:

IF_FACTOR_2_IN_1_GA5(X, Y, Xs, T, times_3_out_gga3(X, Y, Z)) -> FACTOR_2_IN_GA2(._22(Z, Xs), T)
FACTOR_2_IN_GA2(._22(X, ._22(Y, Xs)), T) -> IF_FACTOR_2_IN_1_GA5(X, Y, Xs, T, times_3_in_gga3(X, Y, Z))

The TRS R consists of the following rules:

times_3_in_gga3(0_0, X_, 0_0) -> times_3_out_gga3(0_0, X_, 0_0)
times_3_in_gga3(s_11(X), Y, Z) -> if_times_3_in_1_gga4(X, Y, Z, times_3_in_gga3(X, Y, XY))
if_times_3_in_1_gga4(X, Y, Z, times_3_out_gga3(X, Y, XY)) -> if_times_3_in_2_gga5(X, Y, Z, XY, plus_3_in_gga3(XY, Y, Z))
if_times_3_in_2_gga5(X, Y, Z, XY, plus_3_out_gga3(XY, Y, Z)) -> times_3_out_gga3(s_11(X), Y, Z)
plus_3_in_gga3(0_0, X, X) -> plus_3_out_gga3(0_0, X, X)
plus_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_plus_3_in_1_gga4(X, Y, Z, plus_3_in_gga3(X, Y, Z))
if_plus_3_in_1_gga4(X, Y, Z, plus_3_out_gga3(X, Y, Z)) -> plus_3_out_gga3(s_11(X), Y, s_11(Z))

The argument filtering Pi contains the following mapping:
._22(x1, x2)  =  ._22(x1, x2)
0_0  =  0_0
s_11(x1)  =  s_11(x1)
times_3_in_gga3(x1, x2, x3)  =  times_3_in_gga2(x1, x2)
times_3_out_gga3(x1, x2, x3)  =  times_3_out_gga1(x3)
if_times_3_in_1_gga4(x1, x2, x3, x4)  =  if_times_3_in_1_gga2(x2, x4)
if_times_3_in_2_gga5(x1, x2, x3, x4, x5)  =  if_times_3_in_2_gga1(x5)
plus_3_in_gga3(x1, x2, x3)  =  plus_3_in_gga2(x1, x2)
plus_3_out_gga3(x1, x2, x3)  =  plus_3_out_gga1(x3)
if_plus_3_in_1_gga4(x1, x2, x3, x4)  =  if_plus_3_in_1_gga1(x4)
FACTOR_2_IN_GA2(x1, x2)  =  FACTOR_2_IN_GA1(x1)
IF_FACTOR_2_IN_1_GA5(x1, x2, x3, x4, x5)  =  IF_FACTOR_2_IN_1_GA2(x3, x5)

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

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

IF_FACTOR_2_IN_1_GA2(Xs, times_3_out_gga1(Z)) -> FACTOR_2_IN_GA1(._22(Z, Xs))
FACTOR_2_IN_GA1(._22(X, ._22(Y, Xs))) -> IF_FACTOR_2_IN_1_GA2(Xs, times_3_in_gga2(X, Y))

The TRS R consists of the following rules:

times_3_in_gga2(0_0, X_) -> times_3_out_gga1(0_0)
times_3_in_gga2(s_11(X), Y) -> if_times_3_in_1_gga2(Y, times_3_in_gga2(X, Y))
if_times_3_in_1_gga2(Y, times_3_out_gga1(XY)) -> if_times_3_in_2_gga1(plus_3_in_gga2(XY, Y))
if_times_3_in_2_gga1(plus_3_out_gga1(Z)) -> times_3_out_gga1(Z)
plus_3_in_gga2(0_0, X) -> plus_3_out_gga1(X)
plus_3_in_gga2(s_11(X), Y) -> if_plus_3_in_1_gga1(plus_3_in_gga2(X, Y))
if_plus_3_in_1_gga1(plus_3_out_gga1(Z)) -> plus_3_out_gga1(s_11(Z))

The set Q consists of the following terms:

times_3_in_gga2(x0, x1)
if_times_3_in_1_gga2(x0, x1)
if_times_3_in_2_gga1(x0)
plus_3_in_gga2(x0, x1)
if_plus_3_in_1_gga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {FACTOR_2_IN_GA1, IF_FACTOR_2_IN_1_GA2}.
By using a polynomial ordering, the following set of Dependency Pairs of this DP problem can be strictly oriented.

FACTOR_2_IN_GA1(._22(X, ._22(Y, Xs))) -> IF_FACTOR_2_IN_1_GA2(Xs, times_3_in_gga2(X, Y))
The remaining Dependency Pairs were at least non-strictly be oriented.

IF_FACTOR_2_IN_1_GA2(Xs, times_3_out_gga1(Z)) -> FACTOR_2_IN_GA1(._22(Z, Xs))
With the implicit AFS there is no usable rule.

Used ordering: POLO with Polynomial interpretation:


POL(0_0) = 0   
POL(if_plus_3_in_1_gga1(x1)) = 0   
POL(._22(x1, x2)) = 1 + x2   
POL(if_times_3_in_2_gga1(x1)) = 0   
POL(if_times_3_in_1_gga2(x1, x2)) = 0   
POL(plus_3_out_gga1(x1)) = 0   
POL(FACTOR_2_IN_GA1(x1)) = x1   
POL(times_3_in_gga2(x1, x2)) = 0   
POL(s_11(x1)) = 0   
POL(IF_FACTOR_2_IN_1_GA2(x1, x2)) = 1 + x1   
POL(times_3_out_gga1(x1)) = 0   
POL(plus_3_in_gga2(x1, x2)) = 0   



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

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

IF_FACTOR_2_IN_1_GA2(Xs, times_3_out_gga1(Z)) -> FACTOR_2_IN_GA1(._22(Z, Xs))

The TRS R consists of the following rules:

times_3_in_gga2(0_0, X_) -> times_3_out_gga1(0_0)
times_3_in_gga2(s_11(X), Y) -> if_times_3_in_1_gga2(Y, times_3_in_gga2(X, Y))
if_times_3_in_1_gga2(Y, times_3_out_gga1(XY)) -> if_times_3_in_2_gga1(plus_3_in_gga2(XY, Y))
if_times_3_in_2_gga1(plus_3_out_gga1(Z)) -> times_3_out_gga1(Z)
plus_3_in_gga2(0_0, X) -> plus_3_out_gga1(X)
plus_3_in_gga2(s_11(X), Y) -> if_plus_3_in_1_gga1(plus_3_in_gga2(X, Y))
if_plus_3_in_1_gga1(plus_3_out_gga1(Z)) -> plus_3_out_gga1(s_11(Z))

The set Q consists of the following terms:

times_3_in_gga2(x0, x1)
if_times_3_in_1_gga2(x0, x1)
if_times_3_in_2_gga1(x0)
plus_3_in_gga2(x0, x1)
if_plus_3_in_1_gga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {FACTOR_2_IN_GA1, IF_FACTOR_2_IN_1_GA2}.
The approximation of the Dependency Graph contains 0 SCCs with 1 less node.