MAYBE Left Termination proof of ../tpdb/LP/SGST06/doublehalfpred.pl
Left Termination of the query pattern f_in_1(g) w.r.t. the given Prolog program could not be shown:



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof

Clauses:

pred(0, 0).
pred(s(0), 0).
pred(s(s(X)), s(Y)) :- pred(s(X), Y).
double(0, 0).
double(s(X), s(s(Y))) :- ','(pred(s(X), Z), double(Z, Y)).
half(0, 0).
half(s(s(X)), s(U)) :- ','(pred(s(s(X)), Y), ','(pred(Y, Z), half(Z, U))).
f(s(X)) :- ','(half(s(X), Y), ','(double(Y, Z), f(Z))).

Queries:

f(g).

We use the technique of [30]. With regard to the inferred argument filtering the predicates were used in the following modes:
f_in: (b)
half_in: (b,f)
pred_in: (b,f)
double_in: (b,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

f_in_g(s(X)) → U7_g(X, half_in_ga(s(X), Y))
half_in_ga(0, 0) → half_out_ga(0, 0)
half_in_ga(s(s(X)), s(U)) → U4_ga(X, U, pred_in_ga(s(s(X)), Y))
pred_in_ga(0, 0) → pred_out_ga(0, 0)
pred_in_ga(s(0), 0) → pred_out_ga(s(0), 0)
pred_in_ga(s(s(X)), s(Y)) → U1_ga(X, Y, pred_in_ga(s(X), Y))
U1_ga(X, Y, pred_out_ga(s(X), Y)) → pred_out_ga(s(s(X)), s(Y))
U4_ga(X, U, pred_out_ga(s(s(X)), Y)) → U5_ga(X, U, pred_in_ga(Y, Z))
U5_ga(X, U, pred_out_ga(Y, Z)) → U6_ga(X, U, half_in_ga(Z, U))
U6_ga(X, U, half_out_ga(Z, U)) → half_out_ga(s(s(X)), s(U))
U7_g(X, half_out_ga(s(X), Y)) → U8_g(X, double_in_ga(Y, Z))
double_in_ga(0, 0) → double_out_ga(0, 0)
double_in_ga(s(X), s(s(Y))) → U2_ga(X, Y, pred_in_ga(s(X), Z))
U2_ga(X, Y, pred_out_ga(s(X), Z)) → U3_ga(X, Y, double_in_ga(Z, Y))
U3_ga(X, Y, double_out_ga(Z, Y)) → double_out_ga(s(X), s(s(Y)))
U8_g(X, double_out_ga(Y, Z)) → U9_g(X, f_in_g(Z))
U9_g(X, f_out_g(Z)) → f_out_g(s(X))

The argument filtering Pi contains the following mapping:
f_in_g(x1)  =  f_in_g(x1)
s(x1)  =  s(x1)
U7_g(x1, x2)  =  U7_g(x2)
half_in_ga(x1, x2)  =  half_in_ga(x1)
0  =  0
half_out_ga(x1, x2)  =  half_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
pred_in_ga(x1, x2)  =  pred_in_ga(x1)
pred_out_ga(x1, x2)  =  pred_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U8_g(x1, x2)  =  U8_g(x2)
double_in_ga(x1, x2)  =  double_in_ga(x1)
double_out_ga(x1, x2)  =  double_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U9_g(x1, x2)  =  U9_g(x2)
f_out_g(x1)  =  f_out_g

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:

f_in_g(s(X)) → U7_g(X, half_in_ga(s(X), Y))
half_in_ga(0, 0) → half_out_ga(0, 0)
half_in_ga(s(s(X)), s(U)) → U4_ga(X, U, pred_in_ga(s(s(X)), Y))
pred_in_ga(0, 0) → pred_out_ga(0, 0)
pred_in_ga(s(0), 0) → pred_out_ga(s(0), 0)
pred_in_ga(s(s(X)), s(Y)) → U1_ga(X, Y, pred_in_ga(s(X), Y))
U1_ga(X, Y, pred_out_ga(s(X), Y)) → pred_out_ga(s(s(X)), s(Y))
U4_ga(X, U, pred_out_ga(s(s(X)), Y)) → U5_ga(X, U, pred_in_ga(Y, Z))
U5_ga(X, U, pred_out_ga(Y, Z)) → U6_ga(X, U, half_in_ga(Z, U))
U6_ga(X, U, half_out_ga(Z, U)) → half_out_ga(s(s(X)), s(U))
U7_g(X, half_out_ga(s(X), Y)) → U8_g(X, double_in_ga(Y, Z))
double_in_ga(0, 0) → double_out_ga(0, 0)
double_in_ga(s(X), s(s(Y))) → U2_ga(X, Y, pred_in_ga(s(X), Z))
U2_ga(X, Y, pred_out_ga(s(X), Z)) → U3_ga(X, Y, double_in_ga(Z, Y))
U3_ga(X, Y, double_out_ga(Z, Y)) → double_out_ga(s(X), s(s(Y)))
U8_g(X, double_out_ga(Y, Z)) → U9_g(X, f_in_g(Z))
U9_g(X, f_out_g(Z)) → f_out_g(s(X))

The argument filtering Pi contains the following mapping:
f_in_g(x1)  =  f_in_g(x1)
s(x1)  =  s(x1)
U7_g(x1, x2)  =  U7_g(x2)
half_in_ga(x1, x2)  =  half_in_ga(x1)
0  =  0
half_out_ga(x1, x2)  =  half_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
pred_in_ga(x1, x2)  =  pred_in_ga(x1)
pred_out_ga(x1, x2)  =  pred_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U8_g(x1, x2)  =  U8_g(x2)
double_in_ga(x1, x2)  =  double_in_ga(x1)
double_out_ga(x1, x2)  =  double_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U9_g(x1, x2)  =  U9_g(x2)
f_out_g(x1)  =  f_out_g


Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

F_IN_G(s(X)) → U7_G(X, half_in_ga(s(X), Y))
F_IN_G(s(X)) → HALF_IN_GA(s(X), Y)
HALF_IN_GA(s(s(X)), s(U)) → U4_GA(X, U, pred_in_ga(s(s(X)), Y))
HALF_IN_GA(s(s(X)), s(U)) → PRED_IN_GA(s(s(X)), Y)
PRED_IN_GA(s(s(X)), s(Y)) → U1_GA(X, Y, pred_in_ga(s(X), Y))
PRED_IN_GA(s(s(X)), s(Y)) → PRED_IN_GA(s(X), Y)
U4_GA(X, U, pred_out_ga(s(s(X)), Y)) → U5_GA(X, U, pred_in_ga(Y, Z))
U4_GA(X, U, pred_out_ga(s(s(X)), Y)) → PRED_IN_GA(Y, Z)
U5_GA(X, U, pred_out_ga(Y, Z)) → U6_GA(X, U, half_in_ga(Z, U))
U5_GA(X, U, pred_out_ga(Y, Z)) → HALF_IN_GA(Z, U)
U7_G(X, half_out_ga(s(X), Y)) → U8_G(X, double_in_ga(Y, Z))
U7_G(X, half_out_ga(s(X), Y)) → DOUBLE_IN_GA(Y, Z)
DOUBLE_IN_GA(s(X), s(s(Y))) → U2_GA(X, Y, pred_in_ga(s(X), Z))
DOUBLE_IN_GA(s(X), s(s(Y))) → PRED_IN_GA(s(X), Z)
U2_GA(X, Y, pred_out_ga(s(X), Z)) → U3_GA(X, Y, double_in_ga(Z, Y))
U2_GA(X, Y, pred_out_ga(s(X), Z)) → DOUBLE_IN_GA(Z, Y)
U8_G(X, double_out_ga(Y, Z)) → U9_G(X, f_in_g(Z))
U8_G(X, double_out_ga(Y, Z)) → F_IN_G(Z)

The TRS R consists of the following rules:

f_in_g(s(X)) → U7_g(X, half_in_ga(s(X), Y))
half_in_ga(0, 0) → half_out_ga(0, 0)
half_in_ga(s(s(X)), s(U)) → U4_ga(X, U, pred_in_ga(s(s(X)), Y))
pred_in_ga(0, 0) → pred_out_ga(0, 0)
pred_in_ga(s(0), 0) → pred_out_ga(s(0), 0)
pred_in_ga(s(s(X)), s(Y)) → U1_ga(X, Y, pred_in_ga(s(X), Y))
U1_ga(X, Y, pred_out_ga(s(X), Y)) → pred_out_ga(s(s(X)), s(Y))
U4_ga(X, U, pred_out_ga(s(s(X)), Y)) → U5_ga(X, U, pred_in_ga(Y, Z))
U5_ga(X, U, pred_out_ga(Y, Z)) → U6_ga(X, U, half_in_ga(Z, U))
U6_ga(X, U, half_out_ga(Z, U)) → half_out_ga(s(s(X)), s(U))
U7_g(X, half_out_ga(s(X), Y)) → U8_g(X, double_in_ga(Y, Z))
double_in_ga(0, 0) → double_out_ga(0, 0)
double_in_ga(s(X), s(s(Y))) → U2_ga(X, Y, pred_in_ga(s(X), Z))
U2_ga(X, Y, pred_out_ga(s(X), Z)) → U3_ga(X, Y, double_in_ga(Z, Y))
U3_ga(X, Y, double_out_ga(Z, Y)) → double_out_ga(s(X), s(s(Y)))
U8_g(X, double_out_ga(Y, Z)) → U9_g(X, f_in_g(Z))
U9_g(X, f_out_g(Z)) → f_out_g(s(X))

The argument filtering Pi contains the following mapping:
f_in_g(x1)  =  f_in_g(x1)
s(x1)  =  s(x1)
U7_g(x1, x2)  =  U7_g(x2)
half_in_ga(x1, x2)  =  half_in_ga(x1)
0  =  0
half_out_ga(x1, x2)  =  half_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
pred_in_ga(x1, x2)  =  pred_in_ga(x1)
pred_out_ga(x1, x2)  =  pred_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U8_g(x1, x2)  =  U8_g(x2)
double_in_ga(x1, x2)  =  double_in_ga(x1)
double_out_ga(x1, x2)  =  double_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U9_g(x1, x2)  =  U9_g(x2)
f_out_g(x1)  =  f_out_g
U5_GA(x1, x2, x3)  =  U5_GA(x3)
U4_GA(x1, x2, x3)  =  U4_GA(x3)
U6_GA(x1, x2, x3)  =  U6_GA(x3)
DOUBLE_IN_GA(x1, x2)  =  DOUBLE_IN_GA(x1)
F_IN_G(x1)  =  F_IN_G(x1)
HALF_IN_GA(x1, x2)  =  HALF_IN_GA(x1)
PRED_IN_GA(x1, x2)  =  PRED_IN_GA(x1)
U8_G(x1, x2)  =  U8_G(x2)
U3_GA(x1, x2, x3)  =  U3_GA(x3)
U1_GA(x1, x2, x3)  =  U1_GA(x3)
U2_GA(x1, x2, x3)  =  U2_GA(x3)
U9_G(x1, x2)  =  U9_G(x2)
U7_G(x1, x2)  =  U7_G(x2)

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:

F_IN_G(s(X)) → U7_G(X, half_in_ga(s(X), Y))
F_IN_G(s(X)) → HALF_IN_GA(s(X), Y)
HALF_IN_GA(s(s(X)), s(U)) → U4_GA(X, U, pred_in_ga(s(s(X)), Y))
HALF_IN_GA(s(s(X)), s(U)) → PRED_IN_GA(s(s(X)), Y)
PRED_IN_GA(s(s(X)), s(Y)) → U1_GA(X, Y, pred_in_ga(s(X), Y))
PRED_IN_GA(s(s(X)), s(Y)) → PRED_IN_GA(s(X), Y)
U4_GA(X, U, pred_out_ga(s(s(X)), Y)) → U5_GA(X, U, pred_in_ga(Y, Z))
U4_GA(X, U, pred_out_ga(s(s(X)), Y)) → PRED_IN_GA(Y, Z)
U5_GA(X, U, pred_out_ga(Y, Z)) → U6_GA(X, U, half_in_ga(Z, U))
U5_GA(X, U, pred_out_ga(Y, Z)) → HALF_IN_GA(Z, U)
U7_G(X, half_out_ga(s(X), Y)) → U8_G(X, double_in_ga(Y, Z))
U7_G(X, half_out_ga(s(X), Y)) → DOUBLE_IN_GA(Y, Z)
DOUBLE_IN_GA(s(X), s(s(Y))) → U2_GA(X, Y, pred_in_ga(s(X), Z))
DOUBLE_IN_GA(s(X), s(s(Y))) → PRED_IN_GA(s(X), Z)
U2_GA(X, Y, pred_out_ga(s(X), Z)) → U3_GA(X, Y, double_in_ga(Z, Y))
U2_GA(X, Y, pred_out_ga(s(X), Z)) → DOUBLE_IN_GA(Z, Y)
U8_G(X, double_out_ga(Y, Z)) → U9_G(X, f_in_g(Z))
U8_G(X, double_out_ga(Y, Z)) → F_IN_G(Z)

The TRS R consists of the following rules:

f_in_g(s(X)) → U7_g(X, half_in_ga(s(X), Y))
half_in_ga(0, 0) → half_out_ga(0, 0)
half_in_ga(s(s(X)), s(U)) → U4_ga(X, U, pred_in_ga(s(s(X)), Y))
pred_in_ga(0, 0) → pred_out_ga(0, 0)
pred_in_ga(s(0), 0) → pred_out_ga(s(0), 0)
pred_in_ga(s(s(X)), s(Y)) → U1_ga(X, Y, pred_in_ga(s(X), Y))
U1_ga(X, Y, pred_out_ga(s(X), Y)) → pred_out_ga(s(s(X)), s(Y))
U4_ga(X, U, pred_out_ga(s(s(X)), Y)) → U5_ga(X, U, pred_in_ga(Y, Z))
U5_ga(X, U, pred_out_ga(Y, Z)) → U6_ga(X, U, half_in_ga(Z, U))
U6_ga(X, U, half_out_ga(Z, U)) → half_out_ga(s(s(X)), s(U))
U7_g(X, half_out_ga(s(X), Y)) → U8_g(X, double_in_ga(Y, Z))
double_in_ga(0, 0) → double_out_ga(0, 0)
double_in_ga(s(X), s(s(Y))) → U2_ga(X, Y, pred_in_ga(s(X), Z))
U2_ga(X, Y, pred_out_ga(s(X), Z)) → U3_ga(X, Y, double_in_ga(Z, Y))
U3_ga(X, Y, double_out_ga(Z, Y)) → double_out_ga(s(X), s(s(Y)))
U8_g(X, double_out_ga(Y, Z)) → U9_g(X, f_in_g(Z))
U9_g(X, f_out_g(Z)) → f_out_g(s(X))

The argument filtering Pi contains the following mapping:
f_in_g(x1)  =  f_in_g(x1)
s(x1)  =  s(x1)
U7_g(x1, x2)  =  U7_g(x2)
half_in_ga(x1, x2)  =  half_in_ga(x1)
0  =  0
half_out_ga(x1, x2)  =  half_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
pred_in_ga(x1, x2)  =  pred_in_ga(x1)
pred_out_ga(x1, x2)  =  pred_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U8_g(x1, x2)  =  U8_g(x2)
double_in_ga(x1, x2)  =  double_in_ga(x1)
double_out_ga(x1, x2)  =  double_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U9_g(x1, x2)  =  U9_g(x2)
f_out_g(x1)  =  f_out_g
U5_GA(x1, x2, x3)  =  U5_GA(x3)
U4_GA(x1, x2, x3)  =  U4_GA(x3)
U6_GA(x1, x2, x3)  =  U6_GA(x3)
DOUBLE_IN_GA(x1, x2)  =  DOUBLE_IN_GA(x1)
F_IN_G(x1)  =  F_IN_G(x1)
HALF_IN_GA(x1, x2)  =  HALF_IN_GA(x1)
PRED_IN_GA(x1, x2)  =  PRED_IN_GA(x1)
U8_G(x1, x2)  =  U8_G(x2)
U3_GA(x1, x2, x3)  =  U3_GA(x3)
U1_GA(x1, x2, x3)  =  U1_GA(x3)
U2_GA(x1, x2, x3)  =  U2_GA(x3)
U9_G(x1, x2)  =  U9_G(x2)
U7_G(x1, x2)  =  U7_G(x2)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 4 SCCs with 9 less nodes.

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

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

PRED_IN_GA(s(s(X)), s(Y)) → PRED_IN_GA(s(X), Y)

The TRS R consists of the following rules:

f_in_g(s(X)) → U7_g(X, half_in_ga(s(X), Y))
half_in_ga(0, 0) → half_out_ga(0, 0)
half_in_ga(s(s(X)), s(U)) → U4_ga(X, U, pred_in_ga(s(s(X)), Y))
pred_in_ga(0, 0) → pred_out_ga(0, 0)
pred_in_ga(s(0), 0) → pred_out_ga(s(0), 0)
pred_in_ga(s(s(X)), s(Y)) → U1_ga(X, Y, pred_in_ga(s(X), Y))
U1_ga(X, Y, pred_out_ga(s(X), Y)) → pred_out_ga(s(s(X)), s(Y))
U4_ga(X, U, pred_out_ga(s(s(X)), Y)) → U5_ga(X, U, pred_in_ga(Y, Z))
U5_ga(X, U, pred_out_ga(Y, Z)) → U6_ga(X, U, half_in_ga(Z, U))
U6_ga(X, U, half_out_ga(Z, U)) → half_out_ga(s(s(X)), s(U))
U7_g(X, half_out_ga(s(X), Y)) → U8_g(X, double_in_ga(Y, Z))
double_in_ga(0, 0) → double_out_ga(0, 0)
double_in_ga(s(X), s(s(Y))) → U2_ga(X, Y, pred_in_ga(s(X), Z))
U2_ga(X, Y, pred_out_ga(s(X), Z)) → U3_ga(X, Y, double_in_ga(Z, Y))
U3_ga(X, Y, double_out_ga(Z, Y)) → double_out_ga(s(X), s(s(Y)))
U8_g(X, double_out_ga(Y, Z)) → U9_g(X, f_in_g(Z))
U9_g(X, f_out_g(Z)) → f_out_g(s(X))

The argument filtering Pi contains the following mapping:
f_in_g(x1)  =  f_in_g(x1)
s(x1)  =  s(x1)
U7_g(x1, x2)  =  U7_g(x2)
half_in_ga(x1, x2)  =  half_in_ga(x1)
0  =  0
half_out_ga(x1, x2)  =  half_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
pred_in_ga(x1, x2)  =  pred_in_ga(x1)
pred_out_ga(x1, x2)  =  pred_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U8_g(x1, x2)  =  U8_g(x2)
double_in_ga(x1, x2)  =  double_in_ga(x1)
double_out_ga(x1, x2)  =  double_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U9_g(x1, x2)  =  U9_g(x2)
f_out_g(x1)  =  f_out_g
PRED_IN_GA(x1, x2)  =  PRED_IN_GA(x1)

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

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

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

PRED_IN_GA(s(s(X)), s(Y)) → PRED_IN_GA(s(X), Y)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
PRED_IN_GA(x1, x2)  =  PRED_IN_GA(x1)

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

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

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

PRED_IN_GA(s(s(X))) → PRED_IN_GA(s(X))

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] 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
              ↳ PiDP
  ↳ PrologToPiTRSProof

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

U2_GA(X, Y, pred_out_ga(s(X), Z)) → DOUBLE_IN_GA(Z, Y)
DOUBLE_IN_GA(s(X), s(s(Y))) → U2_GA(X, Y, pred_in_ga(s(X), Z))

The TRS R consists of the following rules:

f_in_g(s(X)) → U7_g(X, half_in_ga(s(X), Y))
half_in_ga(0, 0) → half_out_ga(0, 0)
half_in_ga(s(s(X)), s(U)) → U4_ga(X, U, pred_in_ga(s(s(X)), Y))
pred_in_ga(0, 0) → pred_out_ga(0, 0)
pred_in_ga(s(0), 0) → pred_out_ga(s(0), 0)
pred_in_ga(s(s(X)), s(Y)) → U1_ga(X, Y, pred_in_ga(s(X), Y))
U1_ga(X, Y, pred_out_ga(s(X), Y)) → pred_out_ga(s(s(X)), s(Y))
U4_ga(X, U, pred_out_ga(s(s(X)), Y)) → U5_ga(X, U, pred_in_ga(Y, Z))
U5_ga(X, U, pred_out_ga(Y, Z)) → U6_ga(X, U, half_in_ga(Z, U))
U6_ga(X, U, half_out_ga(Z, U)) → half_out_ga(s(s(X)), s(U))
U7_g(X, half_out_ga(s(X), Y)) → U8_g(X, double_in_ga(Y, Z))
double_in_ga(0, 0) → double_out_ga(0, 0)
double_in_ga(s(X), s(s(Y))) → U2_ga(X, Y, pred_in_ga(s(X), Z))
U2_ga(X, Y, pred_out_ga(s(X), Z)) → U3_ga(X, Y, double_in_ga(Z, Y))
U3_ga(X, Y, double_out_ga(Z, Y)) → double_out_ga(s(X), s(s(Y)))
U8_g(X, double_out_ga(Y, Z)) → U9_g(X, f_in_g(Z))
U9_g(X, f_out_g(Z)) → f_out_g(s(X))

The argument filtering Pi contains the following mapping:
f_in_g(x1)  =  f_in_g(x1)
s(x1)  =  s(x1)
U7_g(x1, x2)  =  U7_g(x2)
half_in_ga(x1, x2)  =  half_in_ga(x1)
0  =  0
half_out_ga(x1, x2)  =  half_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
pred_in_ga(x1, x2)  =  pred_in_ga(x1)
pred_out_ga(x1, x2)  =  pred_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U8_g(x1, x2)  =  U8_g(x2)
double_in_ga(x1, x2)  =  double_in_ga(x1)
double_out_ga(x1, x2)  =  double_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U9_g(x1, x2)  =  U9_g(x2)
f_out_g(x1)  =  f_out_g
DOUBLE_IN_GA(x1, x2)  =  DOUBLE_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x3)

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

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

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

U2_GA(X, Y, pred_out_ga(s(X), Z)) → DOUBLE_IN_GA(Z, Y)
DOUBLE_IN_GA(s(X), s(s(Y))) → U2_GA(X, Y, pred_in_ga(s(X), Z))

The TRS R consists of the following rules:

pred_in_ga(s(0), 0) → pred_out_ga(s(0), 0)
pred_in_ga(s(s(X)), s(Y)) → U1_ga(X, Y, pred_in_ga(s(X), Y))
U1_ga(X, Y, pred_out_ga(s(X), Y)) → pred_out_ga(s(s(X)), s(Y))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
pred_in_ga(x1, x2)  =  pred_in_ga(x1)
pred_out_ga(x1, x2)  =  pred_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
DOUBLE_IN_GA(x1, x2)  =  DOUBLE_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x3)

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

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

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

U2_GA(pred_out_ga(Z)) → DOUBLE_IN_GA(Z)
DOUBLE_IN_GA(s(X)) → U2_GA(pred_in_ga(s(X)))

The TRS R consists of the following rules:

pred_in_ga(s(0)) → pred_out_ga(0)
pred_in_ga(s(s(X))) → U1_ga(pred_in_ga(s(X)))
U1_ga(pred_out_ga(Y)) → pred_out_ga(s(Y))

The set Q consists of the following terms:

pred_in_ga(x0)
U1_ga(x0)

We have to consider all (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

U2_GA(pred_out_ga(Z)) → DOUBLE_IN_GA(Z)
DOUBLE_IN_GA(s(X)) → U2_GA(pred_in_ga(s(X)))

Strictly oriented rules of the TRS R:

pred_in_ga(s(0)) → pred_out_ga(0)
U1_ga(pred_out_ga(Y)) → pred_out_ga(s(Y))

Used ordering: POLO with Polynomial interpretation [25]:

POL(0) = 2   
POL(DOUBLE_IN_GA(x1)) = 2 + 2·x1   
POL(U1_ga(x1)) = 2·x1   
POL(U2_GA(x1)) = 1 + 2·x1   
POL(pred_in_ga(x1)) = x1   
POL(pred_out_ga(x1)) = 1 + x1   
POL(s(x1)) = 2·x1   



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ RuleRemovalProof
                          ↳ QDP
                            ↳ PisEmptyProof
              ↳ PiDP
              ↳ PiDP
  ↳ PrologToPiTRSProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

pred_in_ga(s(s(X))) → U1_ga(pred_in_ga(s(X)))

The set Q consists of the following terms:

pred_in_ga(x0)
U1_ga(x0)

We have to consider all (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

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

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

HALF_IN_GA(s(s(X)), s(U)) → U4_GA(X, U, pred_in_ga(s(s(X)), Y))
U5_GA(X, U, pred_out_ga(Y, Z)) → HALF_IN_GA(Z, U)
U4_GA(X, U, pred_out_ga(s(s(X)), Y)) → U5_GA(X, U, pred_in_ga(Y, Z))

The TRS R consists of the following rules:

f_in_g(s(X)) → U7_g(X, half_in_ga(s(X), Y))
half_in_ga(0, 0) → half_out_ga(0, 0)
half_in_ga(s(s(X)), s(U)) → U4_ga(X, U, pred_in_ga(s(s(X)), Y))
pred_in_ga(0, 0) → pred_out_ga(0, 0)
pred_in_ga(s(0), 0) → pred_out_ga(s(0), 0)
pred_in_ga(s(s(X)), s(Y)) → U1_ga(X, Y, pred_in_ga(s(X), Y))
U1_ga(X, Y, pred_out_ga(s(X), Y)) → pred_out_ga(s(s(X)), s(Y))
U4_ga(X, U, pred_out_ga(s(s(X)), Y)) → U5_ga(X, U, pred_in_ga(Y, Z))
U5_ga(X, U, pred_out_ga(Y, Z)) → U6_ga(X, U, half_in_ga(Z, U))
U6_ga(X, U, half_out_ga(Z, U)) → half_out_ga(s(s(X)), s(U))
U7_g(X, half_out_ga(s(X), Y)) → U8_g(X, double_in_ga(Y, Z))
double_in_ga(0, 0) → double_out_ga(0, 0)
double_in_ga(s(X), s(s(Y))) → U2_ga(X, Y, pred_in_ga(s(X), Z))
U2_ga(X, Y, pred_out_ga(s(X), Z)) → U3_ga(X, Y, double_in_ga(Z, Y))
U3_ga(X, Y, double_out_ga(Z, Y)) → double_out_ga(s(X), s(s(Y)))
U8_g(X, double_out_ga(Y, Z)) → U9_g(X, f_in_g(Z))
U9_g(X, f_out_g(Z)) → f_out_g(s(X))

The argument filtering Pi contains the following mapping:
f_in_g(x1)  =  f_in_g(x1)
s(x1)  =  s(x1)
U7_g(x1, x2)  =  U7_g(x2)
half_in_ga(x1, x2)  =  half_in_ga(x1)
0  =  0
half_out_ga(x1, x2)  =  half_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
pred_in_ga(x1, x2)  =  pred_in_ga(x1)
pred_out_ga(x1, x2)  =  pred_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U8_g(x1, x2)  =  U8_g(x2)
double_in_ga(x1, x2)  =  double_in_ga(x1)
double_out_ga(x1, x2)  =  double_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U9_g(x1, x2)  =  U9_g(x2)
f_out_g(x1)  =  f_out_g
U5_GA(x1, x2, x3)  =  U5_GA(x3)
U4_GA(x1, x2, x3)  =  U4_GA(x3)
HALF_IN_GA(x1, x2)  =  HALF_IN_GA(x1)

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

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

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

HALF_IN_GA(s(s(X)), s(U)) → U4_GA(X, U, pred_in_ga(s(s(X)), Y))
U5_GA(X, U, pred_out_ga(Y, Z)) → HALF_IN_GA(Z, U)
U4_GA(X, U, pred_out_ga(s(s(X)), Y)) → U5_GA(X, U, pred_in_ga(Y, Z))

The TRS R consists of the following rules:

pred_in_ga(s(s(X)), s(Y)) → U1_ga(X, Y, pred_in_ga(s(X), Y))
pred_in_ga(0, 0) → pred_out_ga(0, 0)
pred_in_ga(s(0), 0) → pred_out_ga(s(0), 0)
U1_ga(X, Y, pred_out_ga(s(X), Y)) → pred_out_ga(s(s(X)), s(Y))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
pred_in_ga(x1, x2)  =  pred_in_ga(x1)
pred_out_ga(x1, x2)  =  pred_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U5_GA(x1, x2, x3)  =  U5_GA(x3)
U4_GA(x1, x2, x3)  =  U4_GA(x3)
HALF_IN_GA(x1, x2)  =  HALF_IN_GA(x1)

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

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

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

U4_GA(pred_out_ga(Y)) → U5_GA(pred_in_ga(Y))
U5_GA(pred_out_ga(Z)) → HALF_IN_GA(Z)
HALF_IN_GA(s(s(X))) → U4_GA(pred_in_ga(s(s(X))))

The TRS R consists of the following rules:

pred_in_ga(s(s(X))) → U1_ga(pred_in_ga(s(X)))
pred_in_ga(0) → pred_out_ga(0)
pred_in_ga(s(0)) → pred_out_ga(0)
U1_ga(pred_out_ga(Y)) → pred_out_ga(s(Y))

The set Q consists of the following terms:

pred_in_ga(x0)
U1_ga(x0)

We have to consider all (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], 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:

pred_in_ga(s(0)) → pred_out_ga(0)

Used ordering: POLO with Polynomial interpretation [25]:

POL(0) = 2   
POL(HALF_IN_GA(x1)) = 2·x1   
POL(U1_ga(x1)) = 2·x1   
POL(U4_GA(x1)) = 2·x1   
POL(U5_GA(x1)) = 2·x1   
POL(pred_in_ga(x1)) = x1   
POL(pred_out_ga(x1)) = x1   
POL(s(x1)) = 2·x1   



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ RuleRemovalProof
                          ↳ QDP
                            ↳ RFCMatchBoundsDPProof
              ↳ PiDP
  ↳ PrologToPiTRSProof

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

U4_GA(pred_out_ga(Y)) → U5_GA(pred_in_ga(Y))
HALF_IN_GA(s(s(X))) → U4_GA(pred_in_ga(s(s(X))))
U5_GA(pred_out_ga(Z)) → HALF_IN_GA(Z)

The TRS R consists of the following rules:

pred_in_ga(s(s(X))) → U1_ga(pred_in_ga(s(X)))
pred_in_ga(0) → pred_out_ga(0)
U1_ga(pred_out_ga(Y)) → pred_out_ga(s(Y))

The set Q consists of the following terms:

pred_in_ga(x0)
U1_ga(x0)

We have to consider all (P,Q,R)-chains.
Termination of the TRS P cup R can be shown by a matchbound [6,7] of 2. This implies finiteness of the given DP problem.
The following rules (P cup R) were used to construct the certificate:

pred_in_ga(s(s(X))) → U1_ga(pred_in_ga(s(X)))
pred_in_ga(0) → pred_out_ga(0)
U1_ga(pred_out_ga(Y)) → pred_out_ga(s(Y))
U4_GA(pred_out_ga(Y)) → U5_GA(pred_in_ga(Y))
HALF_IN_GA(s(s(X))) → U4_GA(pred_in_ga(s(s(X))))
U5_GA(pred_out_ga(Z)) → HALF_IN_GA(Z)

The certificate found is represented by the following graph.

The certificate consists of the following enumerated nodes:

211, 212, 213, 214, 215, 216, 217, 218, 219, 220, 221, 222, 223, 224, 225, 226, 227

Node 211 is start node and node 212 is final node.

Those nodes are connect through the following edges:




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

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

U7_G(X, half_out_ga(s(X), Y)) → U8_G(X, double_in_ga(Y, Z))
F_IN_G(s(X)) → U7_G(X, half_in_ga(s(X), Y))
U8_G(X, double_out_ga(Y, Z)) → F_IN_G(Z)

The TRS R consists of the following rules:

f_in_g(s(X)) → U7_g(X, half_in_ga(s(X), Y))
half_in_ga(0, 0) → half_out_ga(0, 0)
half_in_ga(s(s(X)), s(U)) → U4_ga(X, U, pred_in_ga(s(s(X)), Y))
pred_in_ga(0, 0) → pred_out_ga(0, 0)
pred_in_ga(s(0), 0) → pred_out_ga(s(0), 0)
pred_in_ga(s(s(X)), s(Y)) → U1_ga(X, Y, pred_in_ga(s(X), Y))
U1_ga(X, Y, pred_out_ga(s(X), Y)) → pred_out_ga(s(s(X)), s(Y))
U4_ga(X, U, pred_out_ga(s(s(X)), Y)) → U5_ga(X, U, pred_in_ga(Y, Z))
U5_ga(X, U, pred_out_ga(Y, Z)) → U6_ga(X, U, half_in_ga(Z, U))
U6_ga(X, U, half_out_ga(Z, U)) → half_out_ga(s(s(X)), s(U))
U7_g(X, half_out_ga(s(X), Y)) → U8_g(X, double_in_ga(Y, Z))
double_in_ga(0, 0) → double_out_ga(0, 0)
double_in_ga(s(X), s(s(Y))) → U2_ga(X, Y, pred_in_ga(s(X), Z))
U2_ga(X, Y, pred_out_ga(s(X), Z)) → U3_ga(X, Y, double_in_ga(Z, Y))
U3_ga(X, Y, double_out_ga(Z, Y)) → double_out_ga(s(X), s(s(Y)))
U8_g(X, double_out_ga(Y, Z)) → U9_g(X, f_in_g(Z))
U9_g(X, f_out_g(Z)) → f_out_g(s(X))

The argument filtering Pi contains the following mapping:
f_in_g(x1)  =  f_in_g(x1)
s(x1)  =  s(x1)
U7_g(x1, x2)  =  U7_g(x2)
half_in_ga(x1, x2)  =  half_in_ga(x1)
0  =  0
half_out_ga(x1, x2)  =  half_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
pred_in_ga(x1, x2)  =  pred_in_ga(x1)
pred_out_ga(x1, x2)  =  pred_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U8_g(x1, x2)  =  U8_g(x2)
double_in_ga(x1, x2)  =  double_in_ga(x1)
double_out_ga(x1, x2)  =  double_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U9_g(x1, x2)  =  U9_g(x2)
f_out_g(x1)  =  f_out_g
F_IN_G(x1)  =  F_IN_G(x1)
U8_G(x1, x2)  =  U8_G(x2)
U7_G(x1, x2)  =  U7_G(x2)

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

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

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

U7_G(X, half_out_ga(s(X), Y)) → U8_G(X, double_in_ga(Y, Z))
F_IN_G(s(X)) → U7_G(X, half_in_ga(s(X), Y))
U8_G(X, double_out_ga(Y, Z)) → F_IN_G(Z)

The TRS R consists of the following rules:

double_in_ga(0, 0) → double_out_ga(0, 0)
double_in_ga(s(X), s(s(Y))) → U2_ga(X, Y, pred_in_ga(s(X), Z))
half_in_ga(s(s(X)), s(U)) → U4_ga(X, U, pred_in_ga(s(s(X)), Y))
U2_ga(X, Y, pred_out_ga(s(X), Z)) → U3_ga(X, Y, double_in_ga(Z, Y))
U4_ga(X, U, pred_out_ga(s(s(X)), Y)) → U5_ga(X, U, pred_in_ga(Y, Z))
pred_in_ga(s(0), 0) → pred_out_ga(s(0), 0)
pred_in_ga(s(s(X)), s(Y)) → U1_ga(X, Y, pred_in_ga(s(X), Y))
U3_ga(X, Y, double_out_ga(Z, Y)) → double_out_ga(s(X), s(s(Y)))
U5_ga(X, U, pred_out_ga(Y, Z)) → U6_ga(X, U, half_in_ga(Z, U))
U1_ga(X, Y, pred_out_ga(s(X), Y)) → pred_out_ga(s(s(X)), s(Y))
pred_in_ga(0, 0) → pred_out_ga(0, 0)
U6_ga(X, U, half_out_ga(Z, U)) → half_out_ga(s(s(X)), s(U))
half_in_ga(0, 0) → half_out_ga(0, 0)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
half_in_ga(x1, x2)  =  half_in_ga(x1)
0  =  0
half_out_ga(x1, x2)  =  half_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
pred_in_ga(x1, x2)  =  pred_in_ga(x1)
pred_out_ga(x1, x2)  =  pred_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
double_in_ga(x1, x2)  =  double_in_ga(x1)
double_out_ga(x1, x2)  =  double_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
F_IN_G(x1)  =  F_IN_G(x1)
U8_G(x1, x2)  =  U8_G(x2)
U7_G(x1, x2)  =  U7_G(x2)

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

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Narrowing
  ↳ PrologToPiTRSProof

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

F_IN_G(s(X)) → U7_G(half_in_ga(s(X)))
U8_G(double_out_ga(Z)) → F_IN_G(Z)
U7_G(half_out_ga(Y)) → U8_G(double_in_ga(Y))

The TRS R consists of the following rules:

double_in_ga(0) → double_out_ga(0)
double_in_ga(s(X)) → U2_ga(pred_in_ga(s(X)))
half_in_ga(s(s(X))) → U4_ga(pred_in_ga(s(s(X))))
U2_ga(pred_out_ga(Z)) → U3_ga(double_in_ga(Z))
U4_ga(pred_out_ga(Y)) → U5_ga(pred_in_ga(Y))
pred_in_ga(s(0)) → pred_out_ga(0)
pred_in_ga(s(s(X))) → U1_ga(pred_in_ga(s(X)))
U3_ga(double_out_ga(Y)) → double_out_ga(s(s(Y)))
U5_ga(pred_out_ga(Z)) → U6_ga(half_in_ga(Z))
U1_ga(pred_out_ga(Y)) → pred_out_ga(s(Y))
pred_in_ga(0) → pred_out_ga(0)
U6_ga(half_out_ga(U)) → half_out_ga(s(U))
half_in_ga(0) → half_out_ga(0)

The set Q consists of the following terms:

double_in_ga(x0)
half_in_ga(x0)
U2_ga(x0)
U4_ga(x0)
pred_in_ga(x0)
U3_ga(x0)
U5_ga(x0)
U1_ga(x0)
U6_ga(x0)

We have to consider all (P,Q,R)-chains.
By narrowing [15] the rule U7_G(half_out_ga(Y)) → U8_G(double_in_ga(Y)) at position [0] we obtained the following new rules:

U7_G(half_out_ga(s(x0))) → U8_G(U2_ga(pred_in_ga(s(x0))))
U7_G(half_out_ga(0)) → U8_G(double_out_ga(0))



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
  ↳ PrologToPiTRSProof

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

U7_G(half_out_ga(s(x0))) → U8_G(U2_ga(pred_in_ga(s(x0))))
F_IN_G(s(X)) → U7_G(half_in_ga(s(X)))
U8_G(double_out_ga(Z)) → F_IN_G(Z)
U7_G(half_out_ga(0)) → U8_G(double_out_ga(0))

The TRS R consists of the following rules:

double_in_ga(0) → double_out_ga(0)
double_in_ga(s(X)) → U2_ga(pred_in_ga(s(X)))
half_in_ga(s(s(X))) → U4_ga(pred_in_ga(s(s(X))))
U2_ga(pred_out_ga(Z)) → U3_ga(double_in_ga(Z))
U4_ga(pred_out_ga(Y)) → U5_ga(pred_in_ga(Y))
pred_in_ga(s(0)) → pred_out_ga(0)
pred_in_ga(s(s(X))) → U1_ga(pred_in_ga(s(X)))
U3_ga(double_out_ga(Y)) → double_out_ga(s(s(Y)))
U5_ga(pred_out_ga(Z)) → U6_ga(half_in_ga(Z))
U1_ga(pred_out_ga(Y)) → pred_out_ga(s(Y))
pred_in_ga(0) → pred_out_ga(0)
U6_ga(half_out_ga(U)) → half_out_ga(s(U))
half_in_ga(0) → half_out_ga(0)

The set Q consists of the following terms:

double_in_ga(x0)
half_in_ga(x0)
U2_ga(x0)
U4_ga(x0)
pred_in_ga(x0)
U3_ga(x0)
U5_ga(x0)
U1_ga(x0)
U6_ga(x0)

We have to consider all (P,Q,R)-chains.
By narrowing [15] the rule F_IN_G(s(X)) → U7_G(half_in_ga(s(X))) at position [0] we obtained the following new rules:

F_IN_G(s(s(x0))) → U7_G(U4_ga(pred_in_ga(s(s(x0)))))



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Rewriting
  ↳ PrologToPiTRSProof

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

U7_G(half_out_ga(s(x0))) → U8_G(U2_ga(pred_in_ga(s(x0))))
U8_G(double_out_ga(Z)) → F_IN_G(Z)
F_IN_G(s(s(x0))) → U7_G(U4_ga(pred_in_ga(s(s(x0)))))
U7_G(half_out_ga(0)) → U8_G(double_out_ga(0))

The TRS R consists of the following rules:

double_in_ga(0) → double_out_ga(0)
double_in_ga(s(X)) → U2_ga(pred_in_ga(s(X)))
half_in_ga(s(s(X))) → U4_ga(pred_in_ga(s(s(X))))
U2_ga(pred_out_ga(Z)) → U3_ga(double_in_ga(Z))
U4_ga(pred_out_ga(Y)) → U5_ga(pred_in_ga(Y))
pred_in_ga(s(0)) → pred_out_ga(0)
pred_in_ga(s(s(X))) → U1_ga(pred_in_ga(s(X)))
U3_ga(double_out_ga(Y)) → double_out_ga(s(s(Y)))
U5_ga(pred_out_ga(Z)) → U6_ga(half_in_ga(Z))
U1_ga(pred_out_ga(Y)) → pred_out_ga(s(Y))
pred_in_ga(0) → pred_out_ga(0)
U6_ga(half_out_ga(U)) → half_out_ga(s(U))
half_in_ga(0) → half_out_ga(0)

The set Q consists of the following terms:

double_in_ga(x0)
half_in_ga(x0)
U2_ga(x0)
U4_ga(x0)
pred_in_ga(x0)
U3_ga(x0)
U5_ga(x0)
U1_ga(x0)
U6_ga(x0)

We have to consider all (P,Q,R)-chains.
By rewriting [15] the rule F_IN_G(s(s(x0))) → U7_G(U4_ga(pred_in_ga(s(s(x0))))) at position [0,0] we obtained the following new rules:

F_IN_G(s(s(x0))) → U7_G(U4_ga(U1_ga(pred_in_ga(s(x0)))))



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Rewriting
                                  ↳ QDP
                                    ↳ ForwardInstantiation
  ↳ PrologToPiTRSProof

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

U7_G(half_out_ga(s(x0))) → U8_G(U2_ga(pred_in_ga(s(x0))))
U8_G(double_out_ga(Z)) → F_IN_G(Z)
F_IN_G(s(s(x0))) → U7_G(U4_ga(U1_ga(pred_in_ga(s(x0)))))
U7_G(half_out_ga(0)) → U8_G(double_out_ga(0))

The TRS R consists of the following rules:

double_in_ga(0) → double_out_ga(0)
double_in_ga(s(X)) → U2_ga(pred_in_ga(s(X)))
half_in_ga(s(s(X))) → U4_ga(pred_in_ga(s(s(X))))
U2_ga(pred_out_ga(Z)) → U3_ga(double_in_ga(Z))
U4_ga(pred_out_ga(Y)) → U5_ga(pred_in_ga(Y))
pred_in_ga(s(0)) → pred_out_ga(0)
pred_in_ga(s(s(X))) → U1_ga(pred_in_ga(s(X)))
U3_ga(double_out_ga(Y)) → double_out_ga(s(s(Y)))
U5_ga(pred_out_ga(Z)) → U6_ga(half_in_ga(Z))
U1_ga(pred_out_ga(Y)) → pred_out_ga(s(Y))
pred_in_ga(0) → pred_out_ga(0)
U6_ga(half_out_ga(U)) → half_out_ga(s(U))
half_in_ga(0) → half_out_ga(0)

The set Q consists of the following terms:

double_in_ga(x0)
half_in_ga(x0)
U2_ga(x0)
U4_ga(x0)
pred_in_ga(x0)
U3_ga(x0)
U5_ga(x0)
U1_ga(x0)
U6_ga(x0)

We have to consider all (P,Q,R)-chains.
By forward instantiating [14] the rule U8_G(double_out_ga(Z)) → F_IN_G(Z) we obtained the following new rules:

U8_G(double_out_ga(s(s(y_0)))) → F_IN_G(s(s(y_0)))



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Rewriting
                                  ↳ QDP
                                    ↳ ForwardInstantiation
                                      ↳ QDP
                                        ↳ DependencyGraphProof
  ↳ PrologToPiTRSProof

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

U8_G(double_out_ga(s(s(y_0)))) → F_IN_G(s(s(y_0)))
U7_G(half_out_ga(s(x0))) → U8_G(U2_ga(pred_in_ga(s(x0))))
F_IN_G(s(s(x0))) → U7_G(U4_ga(U1_ga(pred_in_ga(s(x0)))))
U7_G(half_out_ga(0)) → U8_G(double_out_ga(0))

The TRS R consists of the following rules:

double_in_ga(0) → double_out_ga(0)
double_in_ga(s(X)) → U2_ga(pred_in_ga(s(X)))
half_in_ga(s(s(X))) → U4_ga(pred_in_ga(s(s(X))))
U2_ga(pred_out_ga(Z)) → U3_ga(double_in_ga(Z))
U4_ga(pred_out_ga(Y)) → U5_ga(pred_in_ga(Y))
pred_in_ga(s(0)) → pred_out_ga(0)
pred_in_ga(s(s(X))) → U1_ga(pred_in_ga(s(X)))
U3_ga(double_out_ga(Y)) → double_out_ga(s(s(Y)))
U5_ga(pred_out_ga(Z)) → U6_ga(half_in_ga(Z))
U1_ga(pred_out_ga(Y)) → pred_out_ga(s(Y))
pred_in_ga(0) → pred_out_ga(0)
U6_ga(half_out_ga(U)) → half_out_ga(s(U))
half_in_ga(0) → half_out_ga(0)

The set Q consists of the following terms:

double_in_ga(x0)
half_in_ga(x0)
U2_ga(x0)
U4_ga(x0)
pred_in_ga(x0)
U3_ga(x0)
U5_ga(x0)
U1_ga(x0)
U6_ga(x0)

We have to consider all (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Rewriting
                                  ↳ QDP
                                    ↳ ForwardInstantiation
                                      ↳ QDP
                                        ↳ DependencyGraphProof
                                          ↳ QDP
  ↳ PrologToPiTRSProof

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

U7_G(half_out_ga(s(x0))) → U8_G(U2_ga(pred_in_ga(s(x0))))
U8_G(double_out_ga(s(s(y_0)))) → F_IN_G(s(s(y_0)))
F_IN_G(s(s(x0))) → U7_G(U4_ga(U1_ga(pred_in_ga(s(x0)))))

The TRS R consists of the following rules:

double_in_ga(0) → double_out_ga(0)
double_in_ga(s(X)) → U2_ga(pred_in_ga(s(X)))
half_in_ga(s(s(X))) → U4_ga(pred_in_ga(s(s(X))))
U2_ga(pred_out_ga(Z)) → U3_ga(double_in_ga(Z))
U4_ga(pred_out_ga(Y)) → U5_ga(pred_in_ga(Y))
pred_in_ga(s(0)) → pred_out_ga(0)
pred_in_ga(s(s(X))) → U1_ga(pred_in_ga(s(X)))
U3_ga(double_out_ga(Y)) → double_out_ga(s(s(Y)))
U5_ga(pred_out_ga(Z)) → U6_ga(half_in_ga(Z))
U1_ga(pred_out_ga(Y)) → pred_out_ga(s(Y))
pred_in_ga(0) → pred_out_ga(0)
U6_ga(half_out_ga(U)) → half_out_ga(s(U))
half_in_ga(0) → half_out_ga(0)

The set Q consists of the following terms:

double_in_ga(x0)
half_in_ga(x0)
U2_ga(x0)
U4_ga(x0)
pred_in_ga(x0)
U3_ga(x0)
U5_ga(x0)
U1_ga(x0)
U6_ga(x0)

We have to consider all (P,Q,R)-chains.
We use the technique of [30]. With regard to the inferred argument filtering the predicates were used in the following modes:
f_in: (b)
half_in: (b,f)
pred_in: (b,f)
double_in: (b,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

f_in_g(s(X)) → U7_g(X, half_in_ga(s(X), Y))
half_in_ga(0, 0) → half_out_ga(0, 0)
half_in_ga(s(s(X)), s(U)) → U4_ga(X, U, pred_in_ga(s(s(X)), Y))
pred_in_ga(0, 0) → pred_out_ga(0, 0)
pred_in_ga(s(0), 0) → pred_out_ga(s(0), 0)
pred_in_ga(s(s(X)), s(Y)) → U1_ga(X, Y, pred_in_ga(s(X), Y))
U1_ga(X, Y, pred_out_ga(s(X), Y)) → pred_out_ga(s(s(X)), s(Y))
U4_ga(X, U, pred_out_ga(s(s(X)), Y)) → U5_ga(X, U, pred_in_ga(Y, Z))
U5_ga(X, U, pred_out_ga(Y, Z)) → U6_ga(X, U, half_in_ga(Z, U))
U6_ga(X, U, half_out_ga(Z, U)) → half_out_ga(s(s(X)), s(U))
U7_g(X, half_out_ga(s(X), Y)) → U8_g(X, double_in_ga(Y, Z))
double_in_ga(0, 0) → double_out_ga(0, 0)
double_in_ga(s(X), s(s(Y))) → U2_ga(X, Y, pred_in_ga(s(X), Z))
U2_ga(X, Y, pred_out_ga(s(X), Z)) → U3_ga(X, Y, double_in_ga(Z, Y))
U3_ga(X, Y, double_out_ga(Z, Y)) → double_out_ga(s(X), s(s(Y)))
U8_g(X, double_out_ga(Y, Z)) → U9_g(X, f_in_g(Z))
U9_g(X, f_out_g(Z)) → f_out_g(s(X))

The argument filtering Pi contains the following mapping:
f_in_g(x1)  =  f_in_g(x1)
s(x1)  =  s(x1)
U7_g(x1, x2)  =  U7_g(x1, x2)
half_in_ga(x1, x2)  =  half_in_ga(x1)
0  =  0
half_out_ga(x1, x2)  =  half_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
pred_in_ga(x1, x2)  =  pred_in_ga(x1)
pred_out_ga(x1, x2)  =  pred_out_ga(x1, x2)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
U6_ga(x1, x2, x3)  =  U6_ga(x1, x3)
U8_g(x1, x2)  =  U8_g(x1, x2)
double_in_ga(x1, x2)  =  double_in_ga(x1)
double_out_ga(x1, x2)  =  double_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
U9_g(x1, x2)  =  U9_g(x1, x2)
f_out_g(x1)  =  f_out_g(x1)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof

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

f_in_g(s(X)) → U7_g(X, half_in_ga(s(X), Y))
half_in_ga(0, 0) → half_out_ga(0, 0)
half_in_ga(s(s(X)), s(U)) → U4_ga(X, U, pred_in_ga(s(s(X)), Y))
pred_in_ga(0, 0) → pred_out_ga(0, 0)
pred_in_ga(s(0), 0) → pred_out_ga(s(0), 0)
pred_in_ga(s(s(X)), s(Y)) → U1_ga(X, Y, pred_in_ga(s(X), Y))
U1_ga(X, Y, pred_out_ga(s(X), Y)) → pred_out_ga(s(s(X)), s(Y))
U4_ga(X, U, pred_out_ga(s(s(X)), Y)) → U5_ga(X, U, pred_in_ga(Y, Z))
U5_ga(X, U, pred_out_ga(Y, Z)) → U6_ga(X, U, half_in_ga(Z, U))
U6_ga(X, U, half_out_ga(Z, U)) → half_out_ga(s(s(X)), s(U))
U7_g(X, half_out_ga(s(X), Y)) → U8_g(X, double_in_ga(Y, Z))
double_in_ga(0, 0) → double_out_ga(0, 0)
double_in_ga(s(X), s(s(Y))) → U2_ga(X, Y, pred_in_ga(s(X), Z))
U2_ga(X, Y, pred_out_ga(s(X), Z)) → U3_ga(X, Y, double_in_ga(Z, Y))
U3_ga(X, Y, double_out_ga(Z, Y)) → double_out_ga(s(X), s(s(Y)))
U8_g(X, double_out_ga(Y, Z)) → U9_g(X, f_in_g(Z))
U9_g(X, f_out_g(Z)) → f_out_g(s(X))

The argument filtering Pi contains the following mapping:
f_in_g(x1)  =  f_in_g(x1)
s(x1)  =  s(x1)
U7_g(x1, x2)  =  U7_g(x1, x2)
half_in_ga(x1, x2)  =  half_in_ga(x1)
0  =  0
half_out_ga(x1, x2)  =  half_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
pred_in_ga(x1, x2)  =  pred_in_ga(x1)
pred_out_ga(x1, x2)  =  pred_out_ga(x1, x2)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
U6_ga(x1, x2, x3)  =  U6_ga(x1, x3)
U8_g(x1, x2)  =  U8_g(x1, x2)
double_in_ga(x1, x2)  =  double_in_ga(x1)
double_out_ga(x1, x2)  =  double_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
U9_g(x1, x2)  =  U9_g(x1, x2)
f_out_g(x1)  =  f_out_g(x1)


Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

F_IN_G(s(X)) → U7_G(X, half_in_ga(s(X), Y))
F_IN_G(s(X)) → HALF_IN_GA(s(X), Y)
HALF_IN_GA(s(s(X)), s(U)) → U4_GA(X, U, pred_in_ga(s(s(X)), Y))
HALF_IN_GA(s(s(X)), s(U)) → PRED_IN_GA(s(s(X)), Y)
PRED_IN_GA(s(s(X)), s(Y)) → U1_GA(X, Y, pred_in_ga(s(X), Y))
PRED_IN_GA(s(s(X)), s(Y)) → PRED_IN_GA(s(X), Y)
U4_GA(X, U, pred_out_ga(s(s(X)), Y)) → U5_GA(X, U, pred_in_ga(Y, Z))
U4_GA(X, U, pred_out_ga(s(s(X)), Y)) → PRED_IN_GA(Y, Z)
U5_GA(X, U, pred_out_ga(Y, Z)) → U6_GA(X, U, half_in_ga(Z, U))
U5_GA(X, U, pred_out_ga(Y, Z)) → HALF_IN_GA(Z, U)
U7_G(X, half_out_ga(s(X), Y)) → U8_G(X, double_in_ga(Y, Z))
U7_G(X, half_out_ga(s(X), Y)) → DOUBLE_IN_GA(Y, Z)
DOUBLE_IN_GA(s(X), s(s(Y))) → U2_GA(X, Y, pred_in_ga(s(X), Z))
DOUBLE_IN_GA(s(X), s(s(Y))) → PRED_IN_GA(s(X), Z)
U2_GA(X, Y, pred_out_ga(s(X), Z)) → U3_GA(X, Y, double_in_ga(Z, Y))
U2_GA(X, Y, pred_out_ga(s(X), Z)) → DOUBLE_IN_GA(Z, Y)
U8_G(X, double_out_ga(Y, Z)) → U9_G(X, f_in_g(Z))
U8_G(X, double_out_ga(Y, Z)) → F_IN_G(Z)

The TRS R consists of the following rules:

f_in_g(s(X)) → U7_g(X, half_in_ga(s(X), Y))
half_in_ga(0, 0) → half_out_ga(0, 0)
half_in_ga(s(s(X)), s(U)) → U4_ga(X, U, pred_in_ga(s(s(X)), Y))
pred_in_ga(0, 0) → pred_out_ga(0, 0)
pred_in_ga(s(0), 0) → pred_out_ga(s(0), 0)
pred_in_ga(s(s(X)), s(Y)) → U1_ga(X, Y, pred_in_ga(s(X), Y))
U1_ga(X, Y, pred_out_ga(s(X), Y)) → pred_out_ga(s(s(X)), s(Y))
U4_ga(X, U, pred_out_ga(s(s(X)), Y)) → U5_ga(X, U, pred_in_ga(Y, Z))
U5_ga(X, U, pred_out_ga(Y, Z)) → U6_ga(X, U, half_in_ga(Z, U))
U6_ga(X, U, half_out_ga(Z, U)) → half_out_ga(s(s(X)), s(U))
U7_g(X, half_out_ga(s(X), Y)) → U8_g(X, double_in_ga(Y, Z))
double_in_ga(0, 0) → double_out_ga(0, 0)
double_in_ga(s(X), s(s(Y))) → U2_ga(X, Y, pred_in_ga(s(X), Z))
U2_ga(X, Y, pred_out_ga(s(X), Z)) → U3_ga(X, Y, double_in_ga(Z, Y))
U3_ga(X, Y, double_out_ga(Z, Y)) → double_out_ga(s(X), s(s(Y)))
U8_g(X, double_out_ga(Y, Z)) → U9_g(X, f_in_g(Z))
U9_g(X, f_out_g(Z)) → f_out_g(s(X))

The argument filtering Pi contains the following mapping:
f_in_g(x1)  =  f_in_g(x1)
s(x1)  =  s(x1)
U7_g(x1, x2)  =  U7_g(x1, x2)
half_in_ga(x1, x2)  =  half_in_ga(x1)
0  =  0
half_out_ga(x1, x2)  =  half_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
pred_in_ga(x1, x2)  =  pred_in_ga(x1)
pred_out_ga(x1, x2)  =  pred_out_ga(x1, x2)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
U6_ga(x1, x2, x3)  =  U6_ga(x1, x3)
U8_g(x1, x2)  =  U8_g(x1, x2)
double_in_ga(x1, x2)  =  double_in_ga(x1)
double_out_ga(x1, x2)  =  double_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
U9_g(x1, x2)  =  U9_g(x1, x2)
f_out_g(x1)  =  f_out_g(x1)
U5_GA(x1, x2, x3)  =  U5_GA(x1, x3)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
U6_GA(x1, x2, x3)  =  U6_GA(x1, x3)
DOUBLE_IN_GA(x1, x2)  =  DOUBLE_IN_GA(x1)
F_IN_G(x1)  =  F_IN_G(x1)
HALF_IN_GA(x1, x2)  =  HALF_IN_GA(x1)
PRED_IN_GA(x1, x2)  =  PRED_IN_GA(x1)
U8_G(x1, x2)  =  U8_G(x1, x2)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
U9_G(x1, x2)  =  U9_G(x1, x2)
U7_G(x1, x2)  =  U7_G(x1, x2)

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

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof

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

F_IN_G(s(X)) → U7_G(X, half_in_ga(s(X), Y))
F_IN_G(s(X)) → HALF_IN_GA(s(X), Y)
HALF_IN_GA(s(s(X)), s(U)) → U4_GA(X, U, pred_in_ga(s(s(X)), Y))
HALF_IN_GA(s(s(X)), s(U)) → PRED_IN_GA(s(s(X)), Y)
PRED_IN_GA(s(s(X)), s(Y)) → U1_GA(X, Y, pred_in_ga(s(X), Y))
PRED_IN_GA(s(s(X)), s(Y)) → PRED_IN_GA(s(X), Y)
U4_GA(X, U, pred_out_ga(s(s(X)), Y)) → U5_GA(X, U, pred_in_ga(Y, Z))
U4_GA(X, U, pred_out_ga(s(s(X)), Y)) → PRED_IN_GA(Y, Z)
U5_GA(X, U, pred_out_ga(Y, Z)) → U6_GA(X, U, half_in_ga(Z, U))
U5_GA(X, U, pred_out_ga(Y, Z)) → HALF_IN_GA(Z, U)
U7_G(X, half_out_ga(s(X), Y)) → U8_G(X, double_in_ga(Y, Z))
U7_G(X, half_out_ga(s(X), Y)) → DOUBLE_IN_GA(Y, Z)
DOUBLE_IN_GA(s(X), s(s(Y))) → U2_GA(X, Y, pred_in_ga(s(X), Z))
DOUBLE_IN_GA(s(X), s(s(Y))) → PRED_IN_GA(s(X), Z)
U2_GA(X, Y, pred_out_ga(s(X), Z)) → U3_GA(X, Y, double_in_ga(Z, Y))
U2_GA(X, Y, pred_out_ga(s(X), Z)) → DOUBLE_IN_GA(Z, Y)
U8_G(X, double_out_ga(Y, Z)) → U9_G(X, f_in_g(Z))
U8_G(X, double_out_ga(Y, Z)) → F_IN_G(Z)

The TRS R consists of the following rules:

f_in_g(s(X)) → U7_g(X, half_in_ga(s(X), Y))
half_in_ga(0, 0) → half_out_ga(0, 0)
half_in_ga(s(s(X)), s(U)) → U4_ga(X, U, pred_in_ga(s(s(X)), Y))
pred_in_ga(0, 0) → pred_out_ga(0, 0)
pred_in_ga(s(0), 0) → pred_out_ga(s(0), 0)
pred_in_ga(s(s(X)), s(Y)) → U1_ga(X, Y, pred_in_ga(s(X), Y))
U1_ga(X, Y, pred_out_ga(s(X), Y)) → pred_out_ga(s(s(X)), s(Y))
U4_ga(X, U, pred_out_ga(s(s(X)), Y)) → U5_ga(X, U, pred_in_ga(Y, Z))
U5_ga(X, U, pred_out_ga(Y, Z)) → U6_ga(X, U, half_in_ga(Z, U))
U6_ga(X, U, half_out_ga(Z, U)) → half_out_ga(s(s(X)), s(U))
U7_g(X, half_out_ga(s(X), Y)) → U8_g(X, double_in_ga(Y, Z))
double_in_ga(0, 0) → double_out_ga(0, 0)
double_in_ga(s(X), s(s(Y))) → U2_ga(X, Y, pred_in_ga(s(X), Z))
U2_ga(X, Y, pred_out_ga(s(X), Z)) → U3_ga(X, Y, double_in_ga(Z, Y))
U3_ga(X, Y, double_out_ga(Z, Y)) → double_out_ga(s(X), s(s(Y)))
U8_g(X, double_out_ga(Y, Z)) → U9_g(X, f_in_g(Z))
U9_g(X, f_out_g(Z)) → f_out_g(s(X))

The argument filtering Pi contains the following mapping:
f_in_g(x1)  =  f_in_g(x1)
s(x1)  =  s(x1)
U7_g(x1, x2)  =  U7_g(x1, x2)
half_in_ga(x1, x2)  =  half_in_ga(x1)
0  =  0
half_out_ga(x1, x2)  =  half_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
pred_in_ga(x1, x2)  =  pred_in_ga(x1)
pred_out_ga(x1, x2)  =  pred_out_ga(x1, x2)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
U6_ga(x1, x2, x3)  =  U6_ga(x1, x3)
U8_g(x1, x2)  =  U8_g(x1, x2)
double_in_ga(x1, x2)  =  double_in_ga(x1)
double_out_ga(x1, x2)  =  double_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
U9_g(x1, x2)  =  U9_g(x1, x2)
f_out_g(x1)  =  f_out_g(x1)
U5_GA(x1, x2, x3)  =  U5_GA(x1, x3)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
U6_GA(x1, x2, x3)  =  U6_GA(x1, x3)
DOUBLE_IN_GA(x1, x2)  =  DOUBLE_IN_GA(x1)
F_IN_G(x1)  =  F_IN_G(x1)
HALF_IN_GA(x1, x2)  =  HALF_IN_GA(x1)
PRED_IN_GA(x1, x2)  =  PRED_IN_GA(x1)
U8_G(x1, x2)  =  U8_G(x1, x2)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
U9_G(x1, x2)  =  U9_G(x1, x2)
U7_G(x1, x2)  =  U7_G(x1, x2)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 4 SCCs with 9 less nodes.

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

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

PRED_IN_GA(s(s(X)), s(Y)) → PRED_IN_GA(s(X), Y)

The TRS R consists of the following rules:

f_in_g(s(X)) → U7_g(X, half_in_ga(s(X), Y))
half_in_ga(0, 0) → half_out_ga(0, 0)
half_in_ga(s(s(X)), s(U)) → U4_ga(X, U, pred_in_ga(s(s(X)), Y))
pred_in_ga(0, 0) → pred_out_ga(0, 0)
pred_in_ga(s(0), 0) → pred_out_ga(s(0), 0)
pred_in_ga(s(s(X)), s(Y)) → U1_ga(X, Y, pred_in_ga(s(X), Y))
U1_ga(X, Y, pred_out_ga(s(X), Y)) → pred_out_ga(s(s(X)), s(Y))
U4_ga(X, U, pred_out_ga(s(s(X)), Y)) → U5_ga(X, U, pred_in_ga(Y, Z))
U5_ga(X, U, pred_out_ga(Y, Z)) → U6_ga(X, U, half_in_ga(Z, U))
U6_ga(X, U, half_out_ga(Z, U)) → half_out_ga(s(s(X)), s(U))
U7_g(X, half_out_ga(s(X), Y)) → U8_g(X, double_in_ga(Y, Z))
double_in_ga(0, 0) → double_out_ga(0, 0)
double_in_ga(s(X), s(s(Y))) → U2_ga(X, Y, pred_in_ga(s(X), Z))
U2_ga(X, Y, pred_out_ga(s(X), Z)) → U3_ga(X, Y, double_in_ga(Z, Y))
U3_ga(X, Y, double_out_ga(Z, Y)) → double_out_ga(s(X), s(s(Y)))
U8_g(X, double_out_ga(Y, Z)) → U9_g(X, f_in_g(Z))
U9_g(X, f_out_g(Z)) → f_out_g(s(X))

The argument filtering Pi contains the following mapping:
f_in_g(x1)  =  f_in_g(x1)
s(x1)  =  s(x1)
U7_g(x1, x2)  =  U7_g(x1, x2)
half_in_ga(x1, x2)  =  half_in_ga(x1)
0  =  0
half_out_ga(x1, x2)  =  half_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
pred_in_ga(x1, x2)  =  pred_in_ga(x1)
pred_out_ga(x1, x2)  =  pred_out_ga(x1, x2)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
U6_ga(x1, x2, x3)  =  U6_ga(x1, x3)
U8_g(x1, x2)  =  U8_g(x1, x2)
double_in_ga(x1, x2)  =  double_in_ga(x1)
double_out_ga(x1, x2)  =  double_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
U9_g(x1, x2)  =  U9_g(x1, x2)
f_out_g(x1)  =  f_out_g(x1)
PRED_IN_GA(x1, x2)  =  PRED_IN_GA(x1)

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

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

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

PRED_IN_GA(s(s(X)), s(Y)) → PRED_IN_GA(s(X), Y)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
PRED_IN_GA(x1, x2)  =  PRED_IN_GA(x1)

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

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

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

PRED_IN_GA(s(s(X))) → PRED_IN_GA(s(X))

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] 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
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP

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

U2_GA(X, Y, pred_out_ga(s(X), Z)) → DOUBLE_IN_GA(Z, Y)
DOUBLE_IN_GA(s(X), s(s(Y))) → U2_GA(X, Y, pred_in_ga(s(X), Z))

The TRS R consists of the following rules:

f_in_g(s(X)) → U7_g(X, half_in_ga(s(X), Y))
half_in_ga(0, 0) → half_out_ga(0, 0)
half_in_ga(s(s(X)), s(U)) → U4_ga(X, U, pred_in_ga(s(s(X)), Y))
pred_in_ga(0, 0) → pred_out_ga(0, 0)
pred_in_ga(s(0), 0) → pred_out_ga(s(0), 0)
pred_in_ga(s(s(X)), s(Y)) → U1_ga(X, Y, pred_in_ga(s(X), Y))
U1_ga(X, Y, pred_out_ga(s(X), Y)) → pred_out_ga(s(s(X)), s(Y))
U4_ga(X, U, pred_out_ga(s(s(X)), Y)) → U5_ga(X, U, pred_in_ga(Y, Z))
U5_ga(X, U, pred_out_ga(Y, Z)) → U6_ga(X, U, half_in_ga(Z, U))
U6_ga(X, U, half_out_ga(Z, U)) → half_out_ga(s(s(X)), s(U))
U7_g(X, half_out_ga(s(X), Y)) → U8_g(X, double_in_ga(Y, Z))
double_in_ga(0, 0) → double_out_ga(0, 0)
double_in_ga(s(X), s(s(Y))) → U2_ga(X, Y, pred_in_ga(s(X), Z))
U2_ga(X, Y, pred_out_ga(s(X), Z)) → U3_ga(X, Y, double_in_ga(Z, Y))
U3_ga(X, Y, double_out_ga(Z, Y)) → double_out_ga(s(X), s(s(Y)))
U8_g(X, double_out_ga(Y, Z)) → U9_g(X, f_in_g(Z))
U9_g(X, f_out_g(Z)) → f_out_g(s(X))

The argument filtering Pi contains the following mapping:
f_in_g(x1)  =  f_in_g(x1)
s(x1)  =  s(x1)
U7_g(x1, x2)  =  U7_g(x1, x2)
half_in_ga(x1, x2)  =  half_in_ga(x1)
0  =  0
half_out_ga(x1, x2)  =  half_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
pred_in_ga(x1, x2)  =  pred_in_ga(x1)
pred_out_ga(x1, x2)  =  pred_out_ga(x1, x2)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
U6_ga(x1, x2, x3)  =  U6_ga(x1, x3)
U8_g(x1, x2)  =  U8_g(x1, x2)
double_in_ga(x1, x2)  =  double_in_ga(x1)
double_out_ga(x1, x2)  =  double_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
U9_g(x1, x2)  =  U9_g(x1, x2)
f_out_g(x1)  =  f_out_g(x1)
DOUBLE_IN_GA(x1, x2)  =  DOUBLE_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)

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

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

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

U2_GA(X, Y, pred_out_ga(s(X), Z)) → DOUBLE_IN_GA(Z, Y)
DOUBLE_IN_GA(s(X), s(s(Y))) → U2_GA(X, Y, pred_in_ga(s(X), Z))

The TRS R consists of the following rules:

pred_in_ga(s(0), 0) → pred_out_ga(s(0), 0)
pred_in_ga(s(s(X)), s(Y)) → U1_ga(X, Y, pred_in_ga(s(X), Y))
U1_ga(X, Y, pred_out_ga(s(X), Y)) → pred_out_ga(s(s(X)), s(Y))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
pred_in_ga(x1, x2)  =  pred_in_ga(x1)
pred_out_ga(x1, x2)  =  pred_out_ga(x1, x2)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
DOUBLE_IN_GA(x1, x2)  =  DOUBLE_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)

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

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPOrderProof
              ↳ PiDP
              ↳ PiDP

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

DOUBLE_IN_GA(s(X)) → U2_GA(X, pred_in_ga(s(X)))
U2_GA(X, pred_out_ga(s(X), Z)) → DOUBLE_IN_GA(Z)

The TRS R consists of the following rules:

pred_in_ga(s(0)) → pred_out_ga(s(0), 0)
pred_in_ga(s(s(X))) → U1_ga(X, pred_in_ga(s(X)))
U1_ga(X, pred_out_ga(s(X), Y)) → pred_out_ga(s(s(X)), s(Y))

The set Q consists of the following terms:

pred_in_ga(x0)
U1_ga(x0, x1)

We have to consider all (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


U2_GA(X, pred_out_ga(s(X), Z)) → DOUBLE_IN_GA(Z)
The remaining pairs can at least be oriented weakly.

DOUBLE_IN_GA(s(X)) → U2_GA(X, pred_in_ga(s(X)))
Used ordering: Polynomial interpretation [25]:

POL(0) = 0   
POL(DOUBLE_IN_GA(x1)) = 1 + x1   
POL(U1_ga(x1, x2)) = 1 + x2   
POL(U2_GA(x1, x2)) = 1 + x2   
POL(pred_in_ga(x1)) = x1   
POL(pred_out_ga(x1, x2)) = 1 + x2   
POL(s(x1)) = 1 + x1   

The following usable rules [17] were oriented:

pred_in_ga(s(s(X))) → U1_ga(X, pred_in_ga(s(X)))
pred_in_ga(s(0)) → pred_out_ga(s(0), 0)
U1_ga(X, pred_out_ga(s(X), Y)) → pred_out_ga(s(s(X)), s(Y))



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPOrderProof
                          ↳ QDP
                            ↳ DependencyGraphProof
              ↳ PiDP
              ↳ PiDP

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

DOUBLE_IN_GA(s(X)) → U2_GA(X, pred_in_ga(s(X)))

The TRS R consists of the following rules:

pred_in_ga(s(0)) → pred_out_ga(s(0), 0)
pred_in_ga(s(s(X))) → U1_ga(X, pred_in_ga(s(X)))
U1_ga(X, pred_out_ga(s(X), Y)) → pred_out_ga(s(s(X)), s(Y))

The set Q consists of the following terms:

pred_in_ga(x0)
U1_ga(x0, x1)

We have to consider all (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 1 less node.

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

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

HALF_IN_GA(s(s(X)), s(U)) → U4_GA(X, U, pred_in_ga(s(s(X)), Y))
U5_GA(X, U, pred_out_ga(Y, Z)) → HALF_IN_GA(Z, U)
U4_GA(X, U, pred_out_ga(s(s(X)), Y)) → U5_GA(X, U, pred_in_ga(Y, Z))

The TRS R consists of the following rules:

f_in_g(s(X)) → U7_g(X, half_in_ga(s(X), Y))
half_in_ga(0, 0) → half_out_ga(0, 0)
half_in_ga(s(s(X)), s(U)) → U4_ga(X, U, pred_in_ga(s(s(X)), Y))
pred_in_ga(0, 0) → pred_out_ga(0, 0)
pred_in_ga(s(0), 0) → pred_out_ga(s(0), 0)
pred_in_ga(s(s(X)), s(Y)) → U1_ga(X, Y, pred_in_ga(s(X), Y))
U1_ga(X, Y, pred_out_ga(s(X), Y)) → pred_out_ga(s(s(X)), s(Y))
U4_ga(X, U, pred_out_ga(s(s(X)), Y)) → U5_ga(X, U, pred_in_ga(Y, Z))
U5_ga(X, U, pred_out_ga(Y, Z)) → U6_ga(X, U, half_in_ga(Z, U))
U6_ga(X, U, half_out_ga(Z, U)) → half_out_ga(s(s(X)), s(U))
U7_g(X, half_out_ga(s(X), Y)) → U8_g(X, double_in_ga(Y, Z))
double_in_ga(0, 0) → double_out_ga(0, 0)
double_in_ga(s(X), s(s(Y))) → U2_ga(X, Y, pred_in_ga(s(X), Z))
U2_ga(X, Y, pred_out_ga(s(X), Z)) → U3_ga(X, Y, double_in_ga(Z, Y))
U3_ga(X, Y, double_out_ga(Z, Y)) → double_out_ga(s(X), s(s(Y)))
U8_g(X, double_out_ga(Y, Z)) → U9_g(X, f_in_g(Z))
U9_g(X, f_out_g(Z)) → f_out_g(s(X))

The argument filtering Pi contains the following mapping:
f_in_g(x1)  =  f_in_g(x1)
s(x1)  =  s(x1)
U7_g(x1, x2)  =  U7_g(x1, x2)
half_in_ga(x1, x2)  =  half_in_ga(x1)
0  =  0
half_out_ga(x1, x2)  =  half_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
pred_in_ga(x1, x2)  =  pred_in_ga(x1)
pred_out_ga(x1, x2)  =  pred_out_ga(x1, x2)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
U6_ga(x1, x2, x3)  =  U6_ga(x1, x3)
U8_g(x1, x2)  =  U8_g(x1, x2)
double_in_ga(x1, x2)  =  double_in_ga(x1)
double_out_ga(x1, x2)  =  double_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
U9_g(x1, x2)  =  U9_g(x1, x2)
f_out_g(x1)  =  f_out_g(x1)
U5_GA(x1, x2, x3)  =  U5_GA(x1, x3)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
HALF_IN_GA(x1, x2)  =  HALF_IN_GA(x1)

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

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

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

HALF_IN_GA(s(s(X)), s(U)) → U4_GA(X, U, pred_in_ga(s(s(X)), Y))
U5_GA(X, U, pred_out_ga(Y, Z)) → HALF_IN_GA(Z, U)
U4_GA(X, U, pred_out_ga(s(s(X)), Y)) → U5_GA(X, U, pred_in_ga(Y, Z))

The TRS R consists of the following rules:

pred_in_ga(s(s(X)), s(Y)) → U1_ga(X, Y, pred_in_ga(s(X), Y))
pred_in_ga(0, 0) → pred_out_ga(0, 0)
pred_in_ga(s(0), 0) → pred_out_ga(s(0), 0)
U1_ga(X, Y, pred_out_ga(s(X), Y)) → pred_out_ga(s(s(X)), s(Y))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
pred_in_ga(x1, x2)  =  pred_in_ga(x1)
pred_out_ga(x1, x2)  =  pred_out_ga(x1, x2)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
U5_GA(x1, x2, x3)  =  U5_GA(x1, x3)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
HALF_IN_GA(x1, x2)  =  HALF_IN_GA(x1)

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

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Rewriting
              ↳ PiDP

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

U4_GA(X, pred_out_ga(s(s(X)), Y)) → U5_GA(X, pred_in_ga(Y))
HALF_IN_GA(s(s(X))) → U4_GA(X, pred_in_ga(s(s(X))))
U5_GA(X, pred_out_ga(Y, Z)) → HALF_IN_GA(Z)

The TRS R consists of the following rules:

pred_in_ga(s(s(X))) → U1_ga(X, pred_in_ga(s(X)))
pred_in_ga(0) → pred_out_ga(0, 0)
pred_in_ga(s(0)) → pred_out_ga(s(0), 0)
U1_ga(X, pred_out_ga(s(X), Y)) → pred_out_ga(s(s(X)), s(Y))

The set Q consists of the following terms:

pred_in_ga(x0)
U1_ga(x0, x1)

We have to consider all (P,Q,R)-chains.
By rewriting [15] the rule HALF_IN_GA(s(s(X))) → U4_GA(X, pred_in_ga(s(s(X)))) at position [1] we obtained the following new rules:

HALF_IN_GA(s(s(X))) → U4_GA(X, U1_ga(X, pred_in_ga(s(X))))



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Rewriting
                          ↳ QDP
                            ↳ QDPOrderProof
              ↳ PiDP

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

U4_GA(X, pred_out_ga(s(s(X)), Y)) → U5_GA(X, pred_in_ga(Y))
U5_GA(X, pred_out_ga(Y, Z)) → HALF_IN_GA(Z)
HALF_IN_GA(s(s(X))) → U4_GA(X, U1_ga(X, pred_in_ga(s(X))))

The TRS R consists of the following rules:

pred_in_ga(s(s(X))) → U1_ga(X, pred_in_ga(s(X)))
pred_in_ga(0) → pred_out_ga(0, 0)
pred_in_ga(s(0)) → pred_out_ga(s(0), 0)
U1_ga(X, pred_out_ga(s(X), Y)) → pred_out_ga(s(s(X)), s(Y))

The set Q consists of the following terms:

pred_in_ga(x0)
U1_ga(x0, x1)

We have to consider all (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


HALF_IN_GA(s(s(X))) → U4_GA(X, U1_ga(X, pred_in_ga(s(X))))
The remaining pairs can at least be oriented weakly.

U4_GA(X, pred_out_ga(s(s(X)), Y)) → U5_GA(X, pred_in_ga(Y))
U5_GA(X, pred_out_ga(Y, Z)) → HALF_IN_GA(Z)
Used ordering: Matrix interpretation [3]:
Non-tuple symbols:
M( U1_ga(x1, x2) ) =
/1\
\0/
+
/00\
\00/
·x1+
/10\
\10/
·x2

M( s(x1) ) =
/0\
\1/
+
/00\
\01/
·x1

M( 0 ) =
/1\
\0/

M( pred_in_ga(x1) ) =
/0\
\0/
+
/11\
\01/
·x1

M( pred_out_ga(x1, x2) ) =
/1\
\0/
+
/00\
\00/
·x1+
/01\
\01/
·x2

Tuple symbols:
M( HALF_IN_GA(x1) ) = 0+
[0,1]
·x1

M( U4_GA(x1, x2) ) = 0+
[0,0]
·x1+
[0,1]
·x2

M( U5_GA(x1, x2) ) = 0+
[0,0]
·x1+
[0,1]
·x2


Matrix type:
We used a basic matrix type which is not further parametrizeable.


As matrix orders are CE-compatible, we used usable rules w.r.t. argument filtering in the order.
The following usable rules [17] were oriented:

U1_ga(X, pred_out_ga(s(X), Y)) → pred_out_ga(s(s(X)), s(Y))
pred_in_ga(0) → pred_out_ga(0, 0)
pred_in_ga(s(0)) → pred_out_ga(s(0), 0)
pred_in_ga(s(s(X))) → U1_ga(X, pred_in_ga(s(X)))



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Rewriting
                          ↳ QDP
                            ↳ QDPOrderProof
                              ↳ QDP
                                ↳ DependencyGraphProof
              ↳ PiDP

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

U4_GA(X, pred_out_ga(s(s(X)), Y)) → U5_GA(X, pred_in_ga(Y))
U5_GA(X, pred_out_ga(Y, Z)) → HALF_IN_GA(Z)

The TRS R consists of the following rules:

pred_in_ga(s(s(X))) → U1_ga(X, pred_in_ga(s(X)))
pred_in_ga(0) → pred_out_ga(0, 0)
pred_in_ga(s(0)) → pred_out_ga(s(0), 0)
U1_ga(X, pred_out_ga(s(X), Y)) → pred_out_ga(s(s(X)), s(Y))

The set Q consists of the following terms:

pred_in_ga(x0)
U1_ga(x0, x1)

We have to consider all (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 2 less nodes.

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

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

U7_G(X, half_out_ga(s(X), Y)) → U8_G(X, double_in_ga(Y, Z))
F_IN_G(s(X)) → U7_G(X, half_in_ga(s(X), Y))
U8_G(X, double_out_ga(Y, Z)) → F_IN_G(Z)

The TRS R consists of the following rules:

f_in_g(s(X)) → U7_g(X, half_in_ga(s(X), Y))
half_in_ga(0, 0) → half_out_ga(0, 0)
half_in_ga(s(s(X)), s(U)) → U4_ga(X, U, pred_in_ga(s(s(X)), Y))
pred_in_ga(0, 0) → pred_out_ga(0, 0)
pred_in_ga(s(0), 0) → pred_out_ga(s(0), 0)
pred_in_ga(s(s(X)), s(Y)) → U1_ga(X, Y, pred_in_ga(s(X), Y))
U1_ga(X, Y, pred_out_ga(s(X), Y)) → pred_out_ga(s(s(X)), s(Y))
U4_ga(X, U, pred_out_ga(s(s(X)), Y)) → U5_ga(X, U, pred_in_ga(Y, Z))
U5_ga(X, U, pred_out_ga(Y, Z)) → U6_ga(X, U, half_in_ga(Z, U))
U6_ga(X, U, half_out_ga(Z, U)) → half_out_ga(s(s(X)), s(U))
U7_g(X, half_out_ga(s(X), Y)) → U8_g(X, double_in_ga(Y, Z))
double_in_ga(0, 0) → double_out_ga(0, 0)
double_in_ga(s(X), s(s(Y))) → U2_ga(X, Y, pred_in_ga(s(X), Z))
U2_ga(X, Y, pred_out_ga(s(X), Z)) → U3_ga(X, Y, double_in_ga(Z, Y))
U3_ga(X, Y, double_out_ga(Z, Y)) → double_out_ga(s(X), s(s(Y)))
U8_g(X, double_out_ga(Y, Z)) → U9_g(X, f_in_g(Z))
U9_g(X, f_out_g(Z)) → f_out_g(s(X))

The argument filtering Pi contains the following mapping:
f_in_g(x1)  =  f_in_g(x1)
s(x1)  =  s(x1)
U7_g(x1, x2)  =  U7_g(x1, x2)
half_in_ga(x1, x2)  =  half_in_ga(x1)
0  =  0
half_out_ga(x1, x2)  =  half_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
pred_in_ga(x1, x2)  =  pred_in_ga(x1)
pred_out_ga(x1, x2)  =  pred_out_ga(x1, x2)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
U6_ga(x1, x2, x3)  =  U6_ga(x1, x3)
U8_g(x1, x2)  =  U8_g(x1, x2)
double_in_ga(x1, x2)  =  double_in_ga(x1)
double_out_ga(x1, x2)  =  double_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
U9_g(x1, x2)  =  U9_g(x1, x2)
f_out_g(x1)  =  f_out_g(x1)
F_IN_G(x1)  =  F_IN_G(x1)
U8_G(x1, x2)  =  U8_G(x1, x2)
U7_G(x1, x2)  =  U7_G(x1, x2)

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

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

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

U7_G(X, half_out_ga(s(X), Y)) → U8_G(X, double_in_ga(Y, Z))
F_IN_G(s(X)) → U7_G(X, half_in_ga(s(X), Y))
U8_G(X, double_out_ga(Y, Z)) → F_IN_G(Z)

The TRS R consists of the following rules:

double_in_ga(0, 0) → double_out_ga(0, 0)
double_in_ga(s(X), s(s(Y))) → U2_ga(X, Y, pred_in_ga(s(X), Z))
half_in_ga(s(s(X)), s(U)) → U4_ga(X, U, pred_in_ga(s(s(X)), Y))
U2_ga(X, Y, pred_out_ga(s(X), Z)) → U3_ga(X, Y, double_in_ga(Z, Y))
U4_ga(X, U, pred_out_ga(s(s(X)), Y)) → U5_ga(X, U, pred_in_ga(Y, Z))
pred_in_ga(s(0), 0) → pred_out_ga(s(0), 0)
pred_in_ga(s(s(X)), s(Y)) → U1_ga(X, Y, pred_in_ga(s(X), Y))
U3_ga(X, Y, double_out_ga(Z, Y)) → double_out_ga(s(X), s(s(Y)))
U5_ga(X, U, pred_out_ga(Y, Z)) → U6_ga(X, U, half_in_ga(Z, U))
U1_ga(X, Y, pred_out_ga(s(X), Y)) → pred_out_ga(s(s(X)), s(Y))
pred_in_ga(0, 0) → pred_out_ga(0, 0)
U6_ga(X, U, half_out_ga(Z, U)) → half_out_ga(s(s(X)), s(U))
half_in_ga(0, 0) → half_out_ga(0, 0)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
half_in_ga(x1, x2)  =  half_in_ga(x1)
0  =  0
half_out_ga(x1, x2)  =  half_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
pred_in_ga(x1, x2)  =  pred_in_ga(x1)
pred_out_ga(x1, x2)  =  pred_out_ga(x1, x2)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
U6_ga(x1, x2, x3)  =  U6_ga(x1, x3)
double_in_ga(x1, x2)  =  double_in_ga(x1)
double_out_ga(x1, x2)  =  double_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
F_IN_G(x1)  =  F_IN_G(x1)
U8_G(x1, x2)  =  U8_G(x1, x2)
U7_G(x1, x2)  =  U7_G(x1, x2)

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

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP

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

U7_G(X, half_out_ga(s(X), Y)) → U8_G(X, double_in_ga(Y))
U8_G(X, double_out_ga(Y, Z)) → F_IN_G(Z)
F_IN_G(s(X)) → U7_G(X, half_in_ga(s(X)))

The TRS R consists of the following rules:

double_in_ga(0) → double_out_ga(0, 0)
double_in_ga(s(X)) → U2_ga(X, pred_in_ga(s(X)))
half_in_ga(s(s(X))) → U4_ga(X, pred_in_ga(s(s(X))))
U2_ga(X, pred_out_ga(s(X), Z)) → U3_ga(X, double_in_ga(Z))
U4_ga(X, pred_out_ga(s(s(X)), Y)) → U5_ga(X, pred_in_ga(Y))
pred_in_ga(s(0)) → pred_out_ga(s(0), 0)
pred_in_ga(s(s(X))) → U1_ga(X, pred_in_ga(s(X)))
U3_ga(X, double_out_ga(Z, Y)) → double_out_ga(s(X), s(s(Y)))
U5_ga(X, pred_out_ga(Y, Z)) → U6_ga(X, half_in_ga(Z))
U1_ga(X, pred_out_ga(s(X), Y)) → pred_out_ga(s(s(X)), s(Y))
pred_in_ga(0) → pred_out_ga(0, 0)
U6_ga(X, half_out_ga(Z, U)) → half_out_ga(s(s(X)), s(U))
half_in_ga(0) → half_out_ga(0, 0)

The set Q consists of the following terms:

double_in_ga(x0)
half_in_ga(x0)
U2_ga(x0, x1)
U4_ga(x0, x1)
pred_in_ga(x0)
U3_ga(x0, x1)
U5_ga(x0, x1)
U1_ga(x0, x1)
U6_ga(x0, x1)

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