(0) Obligation:
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).
(1) PrologToPiTRSProof (SOUND transformation)
We use the technique of [LOPSTR]. 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
(2) Obligation:
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)
(3) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LOPSTR] 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)
F_IN_G(
x1) =
F_IN_G(
x1)
U7_G(
x1,
x2) =
U7_G(
x1,
x2)
HALF_IN_GA(
x1,
x2) =
HALF_IN_GA(
x1)
U4_GA(
x1,
x2,
x3) =
U4_GA(
x1,
x3)
PRED_IN_GA(
x1,
x2) =
PRED_IN_GA(
x1)
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)
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)
We have to consider all (P,R,Pi)-chains
(4) Obligation:
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)
F_IN_G(
x1) =
F_IN_G(
x1)
U7_G(
x1,
x2) =
U7_G(
x1,
x2)
HALF_IN_GA(
x1,
x2) =
HALF_IN_GA(
x1)
U4_GA(
x1,
x2,
x3) =
U4_GA(
x1,
x3)
PRED_IN_GA(
x1,
x2) =
PRED_IN_GA(
x1)
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)
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)
We have to consider all (P,R,Pi)-chains
(5) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 4 SCCs with 9 less nodes.
(6) Complex Obligation (AND)
(7) Obligation:
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
(8) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(9) Obligation:
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
(10) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(11) Obligation:
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.
(12) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] 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:
- PRED_IN_GA(s(s(X))) → PRED_IN_GA(s(X))
The graph contains the following edges 1 > 1
(13) TRUE
(14) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
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)) → DOUBLE_IN_GA(Z, 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)
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
(15) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(16) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
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)) → DOUBLE_IN_GA(Z, Y)
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
(17) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(18) Obligation:
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.
(19) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
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.
Used ordering: Polynomial interpretation [POLO]:
POL(0) = 0
POL(DOUBLE_IN_GA(x1)) = x1
POL(U1_ga(x1, x2)) = 1 + x2
POL(U2_GA(x1, x2)) = x2
POL(pred_in_ga(x1)) = x1
POL(pred_out_ga(x1, x2)) = 1 + x2
POL(s(x1)) = 1 + x1
The following usable rules [FROCOS05] were oriented:
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))
(20) Obligation:
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.
(21) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.
(22) TRUE
(23) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
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)) → HALF_IN_GA(Z, U)
HALF_IN_GA(s(s(X)), s(U)) → U4_GA(X, U, pred_in_ga(s(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)
HALF_IN_GA(
x1,
x2) =
HALF_IN_GA(
x1)
U4_GA(
x1,
x2,
x3) =
U4_GA(
x1,
x3)
U5_GA(
x1,
x2,
x3) =
U5_GA(
x1,
x3)
We have to consider all (P,R,Pi)-chains
(24) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(25) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
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)) → HALF_IN_GA(Z, U)
HALF_IN_GA(s(s(X)), s(U)) → U4_GA(X, U, pred_in_ga(s(s(X)), Y))
The TRS R consists of the following rules:
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))
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)
HALF_IN_GA(
x1,
x2) =
HALF_IN_GA(
x1)
U4_GA(
x1,
x2,
x3) =
U4_GA(
x1,
x3)
U5_GA(
x1,
x2,
x3) =
U5_GA(
x1,
x3)
We have to consider all (P,R,Pi)-chains
(26) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(27) Obligation:
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, pred_in_ga(s(s(X))))
The TRS R consists of the following rules:
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)))
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.
(28) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
HALF_IN_GA(s(s(X))) → U4_GA(X, pred_in_ga(s(s(X))))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:
| POL(U4_GA(x1, x2)) = | 1 | + | | · | x1 | + | | · | x2 |
| POL(pred_out_ga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
| POL(U5_GA(x1, x2)) = | 1 | + | | · | x1 | + | | · | x2 |
| POL(pred_in_ga(x1)) = | | + | | · | x1 |
| POL(HALF_IN_GA(x1)) = | 1 | + | | · | x1 |
| POL(U1_ga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
The following usable rules [FROCOS05] were oriented:
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)))
U1_ga(X, pred_out_ga(s(X), Y)) → pred_out_ga(s(s(X)), s(Y))
(29) Obligation:
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(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)))
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.
(30) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.
(31) TRUE
(32) Obligation:
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))
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), 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)
F_IN_G(
x1) =
F_IN_G(
x1)
U7_G(
x1,
x2) =
U7_G(
x1,
x2)
U8_G(
x1,
x2) =
U8_G(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(33) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(34) Obligation:
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))
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), Y))
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)
U7_G(
x1,
x2) =
U7_G(
x1,
x2)
U8_G(
x1,
x2) =
U8_G(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(35) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(36) Obligation:
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.
(37) Narrowing (SOUND transformation)
By narrowing [LPAR04] the rule
U7_G(
X,
half_out_ga(
s(
X),
Y)) →
U8_G(
X,
double_in_ga(
Y)) at position [1] we obtained the following new rules [LPAR04]:
U7_G(y0, half_out_ga(s(y0), 0)) → U8_G(y0, double_out_ga(0, 0))
U7_G(y0, half_out_ga(s(y0), s(x0))) → U8_G(y0, U2_ga(x0, pred_in_ga(s(x0))))
(38) Obligation:
Q DP problem:
The TRS P consists of the following rules:
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)))
U7_G(y0, half_out_ga(s(y0), 0)) → U8_G(y0, double_out_ga(0, 0))
U7_G(y0, half_out_ga(s(y0), s(x0))) → U8_G(y0, U2_ga(x0, pred_in_ga(s(x0))))
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.
(39) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(40) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F_IN_G(s(X)) → U7_G(X, half_in_ga(s(X)))
U7_G(y0, half_out_ga(s(y0), s(x0))) → U8_G(y0, U2_ga(x0, pred_in_ga(s(x0))))
U8_G(X, double_out_ga(Y, Z)) → F_IN_G(Z)
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.
(41) Narrowing (SOUND transformation)
By narrowing [LPAR04] the rule
F_IN_G(
s(
X)) →
U7_G(
X,
half_in_ga(
s(
X))) at position [1] we obtained the following new rules [LPAR04]:
F_IN_G(s(s(x0))) → U7_G(s(x0), U4_ga(x0, pred_in_ga(s(s(x0)))))
(42) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U7_G(y0, half_out_ga(s(y0), s(x0))) → U8_G(y0, U2_ga(x0, pred_in_ga(s(x0))))
U8_G(X, double_out_ga(Y, Z)) → F_IN_G(Z)
F_IN_G(s(s(x0))) → U7_G(s(x0), U4_ga(x0, pred_in_ga(s(s(x0)))))
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.
(43) Rewriting (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
F_IN_G(
s(
s(
x0))) →
U7_G(
s(
x0),
U4_ga(
x0,
pred_in_ga(
s(
s(
x0))))) at position [1,1] we obtained the following new rules [LPAR04]:
F_IN_G(s(s(x0))) → U7_G(s(x0), U4_ga(x0, U1_ga(x0, pred_in_ga(s(x0)))))
(44) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U7_G(y0, half_out_ga(s(y0), s(x0))) → U8_G(y0, U2_ga(x0, pred_in_ga(s(x0))))
U8_G(X, double_out_ga(Y, Z)) → F_IN_G(Z)
F_IN_G(s(s(x0))) → U7_G(s(x0), U4_ga(x0, U1_ga(x0, pred_in_ga(s(x0)))))
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.
(45) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
U7_G(
y0,
half_out_ga(
s(
y0),
s(
x0))) →
U8_G(
y0,
U2_ga(
x0,
pred_in_ga(
s(
x0)))) we obtained the following new rules [LPAR04]:
U7_G(s(z0), half_out_ga(s(s(z0)), s(x1))) → U8_G(s(z0), U2_ga(x1, pred_in_ga(s(x1))))
(46) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U8_G(X, double_out_ga(Y, Z)) → F_IN_G(Z)
F_IN_G(s(s(x0))) → U7_G(s(x0), U4_ga(x0, U1_ga(x0, pred_in_ga(s(x0)))))
U7_G(s(z0), half_out_ga(s(s(z0)), s(x1))) → U8_G(s(z0), U2_ga(x1, pred_in_ga(s(x1))))
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.
(47) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
U8_G(
X,
double_out_ga(
Y,
Z)) →
F_IN_G(
Z) we obtained the following new rules [LPAR04]:
U8_G(s(z0), double_out_ga(x1, x2)) → F_IN_G(x2)
(48) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F_IN_G(s(s(x0))) → U7_G(s(x0), U4_ga(x0, U1_ga(x0, pred_in_ga(s(x0)))))
U7_G(s(z0), half_out_ga(s(s(z0)), s(x1))) → U8_G(s(z0), U2_ga(x1, pred_in_ga(s(x1))))
U8_G(s(z0), double_out_ga(x1, x2)) → F_IN_G(x2)
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.
(49) ForwardInstantiation (EQUIVALENT transformation)
By forward instantiating [JAR06] the rule
U8_G(
s(
z0),
double_out_ga(
x1,
x2)) →
F_IN_G(
x2) we obtained the following new rules [LPAR04]:
U8_G(s(x0), double_out_ga(x1, s(s(y_0)))) → F_IN_G(s(s(y_0)))
(50) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F_IN_G(s(s(x0))) → U7_G(s(x0), U4_ga(x0, U1_ga(x0, pred_in_ga(s(x0)))))
U7_G(s(z0), half_out_ga(s(s(z0)), s(x1))) → U8_G(s(z0), U2_ga(x1, pred_in_ga(s(x1))))
U8_G(s(x0), double_out_ga(x1, s(s(y_0)))) → F_IN_G(s(s(y_0)))
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.
(51) PrologToPiTRSProof (SOUND transformation)
We use the technique of [LOPSTR]. 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
(52) Obligation:
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
(53) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LOPSTR] 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
F_IN_G(
x1) =
F_IN_G(
x1)
U7_G(
x1,
x2) =
U7_G(
x2)
HALF_IN_GA(
x1,
x2) =
HALF_IN_GA(
x1)
U4_GA(
x1,
x2,
x3) =
U4_GA(
x3)
PRED_IN_GA(
x1,
x2) =
PRED_IN_GA(
x1)
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)
U2_GA(
x1,
x2,
x3) =
U2_GA(
x3)
U3_GA(
x1,
x2,
x3) =
U3_GA(
x3)
U9_G(
x1,
x2) =
U9_G(
x2)
We have to consider all (P,R,Pi)-chains
(54) Obligation:
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
F_IN_G(
x1) =
F_IN_G(
x1)
U7_G(
x1,
x2) =
U7_G(
x2)
HALF_IN_GA(
x1,
x2) =
HALF_IN_GA(
x1)
U4_GA(
x1,
x2,
x3) =
U4_GA(
x3)
PRED_IN_GA(
x1,
x2) =
PRED_IN_GA(
x1)
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)
U2_GA(
x1,
x2,
x3) =
U2_GA(
x3)
U3_GA(
x1,
x2,
x3) =
U3_GA(
x3)
U9_G(
x1,
x2) =
U9_G(
x2)
We have to consider all (P,R,Pi)-chains
(55) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 4 SCCs with 9 less nodes.
(56) Complex Obligation (AND)
(57) Obligation:
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
(58) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(59) Obligation:
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
(60) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(61) Obligation:
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.
(62) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] 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:
- PRED_IN_GA(s(s(X))) → PRED_IN_GA(s(X))
The graph contains the following edges 1 > 1
(63) TRUE
(64) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
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)) → DOUBLE_IN_GA(Z, 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
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
(65) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(66) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
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)) → DOUBLE_IN_GA(Z, Y)
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
(67) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(68) Obligation:
Q DP problem:
The TRS P consists of the following rules:
DOUBLE_IN_GA(s(X)) → U2_GA(pred_in_ga(s(X)))
U2_GA(pred_out_ga(Z)) → DOUBLE_IN_GA(Z)
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.
(69) MRRProof (EQUIVALENT transformation)
By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:
DOUBLE_IN_GA(s(X)) → U2_GA(pred_in_ga(s(X)))
U2_GA(pred_out_ga(Z)) → DOUBLE_IN_GA(Z)
Strictly oriented rules of the TRS R:
pred_in_ga(s(0)) → pred_out_ga(0)
Used ordering: Polynomial interpretation [POLO]:
POL(0) = 0
POL(DOUBLE_IN_GA(x1)) = 1 + x1
POL(U1_ga(x1)) = 3 + x1
POL(U2_GA(x1)) = x1
POL(pred_in_ga(x1)) = x1
POL(pred_out_ga(x1)) = 2 + x1
POL(s(x1)) = 3 + x1
(70) Obligation:
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)))
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.
(71) PisEmptyProof (EQUIVALENT transformation)
The TRS P is empty. Hence, there is no (P,Q,R) chain.
(72) TRUE
(73) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
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)) → HALF_IN_GA(Z, U)
HALF_IN_GA(s(s(X)), s(U)) → U4_GA(X, U, pred_in_ga(s(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
HALF_IN_GA(
x1,
x2) =
HALF_IN_GA(
x1)
U4_GA(
x1,
x2,
x3) =
U4_GA(
x3)
U5_GA(
x1,
x2,
x3) =
U5_GA(
x3)
We have to consider all (P,R,Pi)-chains
(74) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(75) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
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)) → HALF_IN_GA(Z, U)
HALF_IN_GA(s(s(X)), s(U)) → U4_GA(X, U, pred_in_ga(s(s(X)), Y))
The TRS R consists of the following rules:
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))
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)
HALF_IN_GA(
x1,
x2) =
HALF_IN_GA(
x1)
U4_GA(
x1,
x2,
x3) =
U4_GA(
x3)
U5_GA(
x1,
x2,
x3) =
U5_GA(
x3)
We have to consider all (P,R,Pi)-chains
(76) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(77) Obligation:
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(0) → pred_out_ga(0)
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.
(78) MRRProof (EQUIVALENT transformation)
By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented rules of the TRS R:
pred_in_ga(s(0)) → pred_out_ga(0)
Used ordering: Polynomial interpretation [POLO]:
POL(0) = 0
POL(HALF_IN_GA(x1)) = x1
POL(U1_ga(x1)) = 1 + x1
POL(U4_GA(x1)) = x1
POL(U5_GA(x1)) = x1
POL(pred_in_ga(x1)) = x1
POL(pred_out_ga(x1)) = x1
POL(s(x1)) = 1 + x1
(79) Obligation:
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(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.
(80) RFCMatchBoundsDPProof (EQUIVALENT transformation)
Termination of the TRS P cup R can be shown by a matchbound [MATCHBOUNDS1,MATCHBOUNDS2] 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(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))
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 certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
375, 386, 389, 388, 387, 390, 391, 392, 393, 396, 394, 395, 397, 398, 399, 400, 401
Node 375 is start node and node 386 is final node.
Those nodes are connect through the following edges:
- 375 to 387 labelled U4_GA_1(0)
- 375 to 390 labelled U1_ga_1(0)
- 375 to 392 labelled pred_out_ga_1(0)
- 375 to 386 labelled HALF_IN_GA_1(0)
- 375 to 389 labelled pred_out_ga_1(0)
- 375 to 393 labelled U5_GA_1(0)
- 375 to 394 labelled U4_GA_1(1)
- 375 to 399 labelled HALF_IN_GA_1(1)
- 386 to 386 labelled #_1(0)
- 389 to 386 labelled s_1(0)
- 388 to 389 labelled s_1(0)
- 387 to 388 labelled pred_in_ga_1(0)
- 387 to 397 labelled U1_ga_1(1)
- 390 to 391 labelled pred_in_ga_1(0)
- 390 to 397 labelled U1_ga_1(1)
- 391 to 386 labelled s_1(0)
- 392 to 386 labelled 0(0)
- 393 to 386 labelled pred_in_ga_1(0)
- 393 to 397 labelled U1_ga_1(1)
- 393 to 399 labelled pred_out_ga_1(1)
- 396 to 386 labelled s_1(1)
- 394 to 395 labelled pred_in_ga_1(1)
- 394 to 400 labelled U1_ga_1(2)
- 395 to 396 labelled s_1(1)
- 397 to 398 labelled pred_in_ga_1(1)
- 397 to 397 labelled U1_ga_1(1)
- 398 to 386 labelled s_1(1)
- 399 to 386 labelled 0(1)
- 400 to 401 labelled pred_in_ga_1(2)
- 400 to 397 labelled U1_ga_1(1)
- 401 to 386 labelled s_1(2)
(81) TRUE
(82) Obligation:
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))
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), 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
F_IN_G(
x1) =
F_IN_G(
x1)
U7_G(
x1,
x2) =
U7_G(
x2)
U8_G(
x1,
x2) =
U8_G(
x2)
We have to consider all (P,R,Pi)-chains
(83) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(84) Obligation:
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))
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), Y))
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)
U7_G(
x1,
x2) =
U7_G(
x2)
U8_G(
x1,
x2) =
U8_G(
x2)
We have to consider all (P,R,Pi)-chains
(85) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(86) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U7_G(half_out_ga(Y)) → U8_G(double_in_ga(Y))
U8_G(double_out_ga(Z)) → F_IN_G(Z)
F_IN_G(s(X)) → U7_G(half_in_ga(s(X)))
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.
(87) Narrowing (SOUND transformation)
By narrowing [LPAR04] the rule
U7_G(
half_out_ga(
Y)) →
U8_G(
double_in_ga(
Y)) at position [0] we obtained the following new rules [LPAR04]:
U7_G(half_out_ga(0)) → U8_G(double_out_ga(0))
U7_G(half_out_ga(s(x0))) → U8_G(U2_ga(pred_in_ga(s(x0))))
(88) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U8_G(double_out_ga(Z)) → F_IN_G(Z)
F_IN_G(s(X)) → U7_G(half_in_ga(s(X)))
U7_G(half_out_ga(0)) → U8_G(double_out_ga(0))
U7_G(half_out_ga(s(x0))) → U8_G(U2_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.
(89) Narrowing (SOUND transformation)
By narrowing [LPAR04] the rule
F_IN_G(
s(
X)) →
U7_G(
half_in_ga(
s(
X))) at position [0] we obtained the following new rules [LPAR04]:
F_IN_G(s(s(x0))) → U7_G(U4_ga(pred_in_ga(s(s(x0)))))
(90) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U8_G(double_out_ga(Z)) → F_IN_G(Z)
U7_G(half_out_ga(0)) → U8_G(double_out_ga(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(pred_in_ga(s(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.
(91) Rewriting (EQUIVALENT transformation)
By rewriting [LPAR04] 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 [LPAR04]:
F_IN_G(s(s(x0))) → U7_G(U4_ga(U1_ga(pred_in_ga(s(x0)))))
(92) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U8_G(double_out_ga(Z)) → F_IN_G(Z)
U7_G(half_out_ga(0)) → U8_G(double_out_ga(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)))))
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.
(93) ForwardInstantiation (EQUIVALENT transformation)
By forward instantiating [JAR06] the rule
U8_G(
double_out_ga(
Z)) →
F_IN_G(
Z) we obtained the following new rules [LPAR04]:
U8_G(double_out_ga(s(s(y_0)))) → F_IN_G(s(s(y_0)))
(94) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U7_G(half_out_ga(0)) → U8_G(double_out_ga(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)))))
U8_G(double_out_ga(s(s(y_0)))) → F_IN_G(s(s(y_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.
(95) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(96) Obligation:
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.