(0) Obligation:
Clauses:
convert([], B, 0).
convert(.(0, XS), B, X) :- ','(convert(XS, B, Y), times(Y, B, X)).
convert(.(s(Y), XS), B, s(X)) :- convert(.(Y, XS), B, X).
plus(0, Y, Y).
plus(s(X), Y, s(Z)) :- plus(X, Y, Z).
times(0, Y, 0).
times(s(X), Y, Z) :- ','(times(X, Y, U), plus(Y, U, Z)).
Queries:
convert(g,g,a).
(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:
convert_in: (b,b,f)
times_in: (b,b,f)
plus_in: (b,b,f)
Transforming
Prolog into the following
Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
convert_in_gga([], B, 0) → convert_out_gga([], B, 0)
convert_in_gga(.(0, XS), B, X) → U1_gga(XS, B, X, convert_in_gga(XS, B, Y))
convert_in_gga(.(s(Y), XS), B, s(X)) → U3_gga(Y, XS, B, X, convert_in_gga(.(Y, XS), B, X))
U3_gga(Y, XS, B, X, convert_out_gga(.(Y, XS), B, X)) → convert_out_gga(.(s(Y), XS), B, s(X))
U1_gga(XS, B, X, convert_out_gga(XS, B, Y)) → U2_gga(XS, B, X, times_in_gga(Y, B, X))
times_in_gga(0, Y, 0) → times_out_gga(0, Y, 0)
times_in_gga(s(X), Y, Z) → U5_gga(X, Y, Z, times_in_gga(X, Y, U))
U5_gga(X, Y, Z, times_out_gga(X, Y, U)) → U6_gga(X, Y, Z, plus_in_gga(Y, U, Z))
plus_in_gga(0, Y, Y) → plus_out_gga(0, Y, Y)
plus_in_gga(s(X), Y, s(Z)) → U4_gga(X, Y, Z, plus_in_gga(X, Y, Z))
U4_gga(X, Y, Z, plus_out_gga(X, Y, Z)) → plus_out_gga(s(X), Y, s(Z))
U6_gga(X, Y, Z, plus_out_gga(Y, U, Z)) → times_out_gga(s(X), Y, Z)
U2_gga(XS, B, X, times_out_gga(Y, B, X)) → convert_out_gga(.(0, XS), B, X)
The argument filtering Pi contains the following mapping:
convert_in_gga(
x1,
x2,
x3) =
convert_in_gga(
x1,
x2)
[] =
[]
convert_out_gga(
x1,
x2,
x3) =
convert_out_gga(
x3)
.(
x1,
x2) =
.(
x1,
x2)
0 =
0
U1_gga(
x1,
x2,
x3,
x4) =
U1_gga(
x2,
x4)
s(
x1) =
s(
x1)
U3_gga(
x1,
x2,
x3,
x4,
x5) =
U3_gga(
x5)
U2_gga(
x1,
x2,
x3,
x4) =
U2_gga(
x4)
times_in_gga(
x1,
x2,
x3) =
times_in_gga(
x1,
x2)
times_out_gga(
x1,
x2,
x3) =
times_out_gga(
x3)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x2,
x4)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x4)
plus_in_gga(
x1,
x2,
x3) =
plus_in_gga(
x1,
x2)
plus_out_gga(
x1,
x2,
x3) =
plus_out_gga(
x3)
U4_gga(
x1,
x2,
x3,
x4) =
U4_gga(
x4)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
(2) Obligation:
Pi-finite rewrite system:
The TRS R consists of the following rules:
convert_in_gga([], B, 0) → convert_out_gga([], B, 0)
convert_in_gga(.(0, XS), B, X) → U1_gga(XS, B, X, convert_in_gga(XS, B, Y))
convert_in_gga(.(s(Y), XS), B, s(X)) → U3_gga(Y, XS, B, X, convert_in_gga(.(Y, XS), B, X))
U3_gga(Y, XS, B, X, convert_out_gga(.(Y, XS), B, X)) → convert_out_gga(.(s(Y), XS), B, s(X))
U1_gga(XS, B, X, convert_out_gga(XS, B, Y)) → U2_gga(XS, B, X, times_in_gga(Y, B, X))
times_in_gga(0, Y, 0) → times_out_gga(0, Y, 0)
times_in_gga(s(X), Y, Z) → U5_gga(X, Y, Z, times_in_gga(X, Y, U))
U5_gga(X, Y, Z, times_out_gga(X, Y, U)) → U6_gga(X, Y, Z, plus_in_gga(Y, U, Z))
plus_in_gga(0, Y, Y) → plus_out_gga(0, Y, Y)
plus_in_gga(s(X), Y, s(Z)) → U4_gga(X, Y, Z, plus_in_gga(X, Y, Z))
U4_gga(X, Y, Z, plus_out_gga(X, Y, Z)) → plus_out_gga(s(X), Y, s(Z))
U6_gga(X, Y, Z, plus_out_gga(Y, U, Z)) → times_out_gga(s(X), Y, Z)
U2_gga(XS, B, X, times_out_gga(Y, B, X)) → convert_out_gga(.(0, XS), B, X)
The argument filtering Pi contains the following mapping:
convert_in_gga(
x1,
x2,
x3) =
convert_in_gga(
x1,
x2)
[] =
[]
convert_out_gga(
x1,
x2,
x3) =
convert_out_gga(
x3)
.(
x1,
x2) =
.(
x1,
x2)
0 =
0
U1_gga(
x1,
x2,
x3,
x4) =
U1_gga(
x2,
x4)
s(
x1) =
s(
x1)
U3_gga(
x1,
x2,
x3,
x4,
x5) =
U3_gga(
x5)
U2_gga(
x1,
x2,
x3,
x4) =
U2_gga(
x4)
times_in_gga(
x1,
x2,
x3) =
times_in_gga(
x1,
x2)
times_out_gga(
x1,
x2,
x3) =
times_out_gga(
x3)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x2,
x4)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x4)
plus_in_gga(
x1,
x2,
x3) =
plus_in_gga(
x1,
x2)
plus_out_gga(
x1,
x2,
x3) =
plus_out_gga(
x3)
U4_gga(
x1,
x2,
x3,
x4) =
U4_gga(
x4)
(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:
CONVERT_IN_GGA(.(0, XS), B, X) → U1_GGA(XS, B, X, convert_in_gga(XS, B, Y))
CONVERT_IN_GGA(.(0, XS), B, X) → CONVERT_IN_GGA(XS, B, Y)
CONVERT_IN_GGA(.(s(Y), XS), B, s(X)) → U3_GGA(Y, XS, B, X, convert_in_gga(.(Y, XS), B, X))
CONVERT_IN_GGA(.(s(Y), XS), B, s(X)) → CONVERT_IN_GGA(.(Y, XS), B, X)
U1_GGA(XS, B, X, convert_out_gga(XS, B, Y)) → U2_GGA(XS, B, X, times_in_gga(Y, B, X))
U1_GGA(XS, B, X, convert_out_gga(XS, B, Y)) → TIMES_IN_GGA(Y, B, X)
TIMES_IN_GGA(s(X), Y, Z) → U5_GGA(X, Y, Z, times_in_gga(X, Y, U))
TIMES_IN_GGA(s(X), Y, Z) → TIMES_IN_GGA(X, Y, U)
U5_GGA(X, Y, Z, times_out_gga(X, Y, U)) → U6_GGA(X, Y, Z, plus_in_gga(Y, U, Z))
U5_GGA(X, Y, Z, times_out_gga(X, Y, U)) → PLUS_IN_GGA(Y, U, Z)
PLUS_IN_GGA(s(X), Y, s(Z)) → U4_GGA(X, Y, Z, plus_in_gga(X, Y, Z))
PLUS_IN_GGA(s(X), Y, s(Z)) → PLUS_IN_GGA(X, Y, Z)
The TRS R consists of the following rules:
convert_in_gga([], B, 0) → convert_out_gga([], B, 0)
convert_in_gga(.(0, XS), B, X) → U1_gga(XS, B, X, convert_in_gga(XS, B, Y))
convert_in_gga(.(s(Y), XS), B, s(X)) → U3_gga(Y, XS, B, X, convert_in_gga(.(Y, XS), B, X))
U3_gga(Y, XS, B, X, convert_out_gga(.(Y, XS), B, X)) → convert_out_gga(.(s(Y), XS), B, s(X))
U1_gga(XS, B, X, convert_out_gga(XS, B, Y)) → U2_gga(XS, B, X, times_in_gga(Y, B, X))
times_in_gga(0, Y, 0) → times_out_gga(0, Y, 0)
times_in_gga(s(X), Y, Z) → U5_gga(X, Y, Z, times_in_gga(X, Y, U))
U5_gga(X, Y, Z, times_out_gga(X, Y, U)) → U6_gga(X, Y, Z, plus_in_gga(Y, U, Z))
plus_in_gga(0, Y, Y) → plus_out_gga(0, Y, Y)
plus_in_gga(s(X), Y, s(Z)) → U4_gga(X, Y, Z, plus_in_gga(X, Y, Z))
U4_gga(X, Y, Z, plus_out_gga(X, Y, Z)) → plus_out_gga(s(X), Y, s(Z))
U6_gga(X, Y, Z, plus_out_gga(Y, U, Z)) → times_out_gga(s(X), Y, Z)
U2_gga(XS, B, X, times_out_gga(Y, B, X)) → convert_out_gga(.(0, XS), B, X)
The argument filtering Pi contains the following mapping:
convert_in_gga(
x1,
x2,
x3) =
convert_in_gga(
x1,
x2)
[] =
[]
convert_out_gga(
x1,
x2,
x3) =
convert_out_gga(
x3)
.(
x1,
x2) =
.(
x1,
x2)
0 =
0
U1_gga(
x1,
x2,
x3,
x4) =
U1_gga(
x2,
x4)
s(
x1) =
s(
x1)
U3_gga(
x1,
x2,
x3,
x4,
x5) =
U3_gga(
x5)
U2_gga(
x1,
x2,
x3,
x4) =
U2_gga(
x4)
times_in_gga(
x1,
x2,
x3) =
times_in_gga(
x1,
x2)
times_out_gga(
x1,
x2,
x3) =
times_out_gga(
x3)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x2,
x4)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x4)
plus_in_gga(
x1,
x2,
x3) =
plus_in_gga(
x1,
x2)
plus_out_gga(
x1,
x2,
x3) =
plus_out_gga(
x3)
U4_gga(
x1,
x2,
x3,
x4) =
U4_gga(
x4)
CONVERT_IN_GGA(
x1,
x2,
x3) =
CONVERT_IN_GGA(
x1,
x2)
U1_GGA(
x1,
x2,
x3,
x4) =
U1_GGA(
x2,
x4)
U3_GGA(
x1,
x2,
x3,
x4,
x5) =
U3_GGA(
x5)
U2_GGA(
x1,
x2,
x3,
x4) =
U2_GGA(
x4)
TIMES_IN_GGA(
x1,
x2,
x3) =
TIMES_IN_GGA(
x1,
x2)
U5_GGA(
x1,
x2,
x3,
x4) =
U5_GGA(
x2,
x4)
U6_GGA(
x1,
x2,
x3,
x4) =
U6_GGA(
x4)
PLUS_IN_GGA(
x1,
x2,
x3) =
PLUS_IN_GGA(
x1,
x2)
U4_GGA(
x1,
x2,
x3,
x4) =
U4_GGA(
x4)
We have to consider all (P,R,Pi)-chains
(4) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
CONVERT_IN_GGA(.(0, XS), B, X) → U1_GGA(XS, B, X, convert_in_gga(XS, B, Y))
CONVERT_IN_GGA(.(0, XS), B, X) → CONVERT_IN_GGA(XS, B, Y)
CONVERT_IN_GGA(.(s(Y), XS), B, s(X)) → U3_GGA(Y, XS, B, X, convert_in_gga(.(Y, XS), B, X))
CONVERT_IN_GGA(.(s(Y), XS), B, s(X)) → CONVERT_IN_GGA(.(Y, XS), B, X)
U1_GGA(XS, B, X, convert_out_gga(XS, B, Y)) → U2_GGA(XS, B, X, times_in_gga(Y, B, X))
U1_GGA(XS, B, X, convert_out_gga(XS, B, Y)) → TIMES_IN_GGA(Y, B, X)
TIMES_IN_GGA(s(X), Y, Z) → U5_GGA(X, Y, Z, times_in_gga(X, Y, U))
TIMES_IN_GGA(s(X), Y, Z) → TIMES_IN_GGA(X, Y, U)
U5_GGA(X, Y, Z, times_out_gga(X, Y, U)) → U6_GGA(X, Y, Z, plus_in_gga(Y, U, Z))
U5_GGA(X, Y, Z, times_out_gga(X, Y, U)) → PLUS_IN_GGA(Y, U, Z)
PLUS_IN_GGA(s(X), Y, s(Z)) → U4_GGA(X, Y, Z, plus_in_gga(X, Y, Z))
PLUS_IN_GGA(s(X), Y, s(Z)) → PLUS_IN_GGA(X, Y, Z)
The TRS R consists of the following rules:
convert_in_gga([], B, 0) → convert_out_gga([], B, 0)
convert_in_gga(.(0, XS), B, X) → U1_gga(XS, B, X, convert_in_gga(XS, B, Y))
convert_in_gga(.(s(Y), XS), B, s(X)) → U3_gga(Y, XS, B, X, convert_in_gga(.(Y, XS), B, X))
U3_gga(Y, XS, B, X, convert_out_gga(.(Y, XS), B, X)) → convert_out_gga(.(s(Y), XS), B, s(X))
U1_gga(XS, B, X, convert_out_gga(XS, B, Y)) → U2_gga(XS, B, X, times_in_gga(Y, B, X))
times_in_gga(0, Y, 0) → times_out_gga(0, Y, 0)
times_in_gga(s(X), Y, Z) → U5_gga(X, Y, Z, times_in_gga(X, Y, U))
U5_gga(X, Y, Z, times_out_gga(X, Y, U)) → U6_gga(X, Y, Z, plus_in_gga(Y, U, Z))
plus_in_gga(0, Y, Y) → plus_out_gga(0, Y, Y)
plus_in_gga(s(X), Y, s(Z)) → U4_gga(X, Y, Z, plus_in_gga(X, Y, Z))
U4_gga(X, Y, Z, plus_out_gga(X, Y, Z)) → plus_out_gga(s(X), Y, s(Z))
U6_gga(X, Y, Z, plus_out_gga(Y, U, Z)) → times_out_gga(s(X), Y, Z)
U2_gga(XS, B, X, times_out_gga(Y, B, X)) → convert_out_gga(.(0, XS), B, X)
The argument filtering Pi contains the following mapping:
convert_in_gga(
x1,
x2,
x3) =
convert_in_gga(
x1,
x2)
[] =
[]
convert_out_gga(
x1,
x2,
x3) =
convert_out_gga(
x3)
.(
x1,
x2) =
.(
x1,
x2)
0 =
0
U1_gga(
x1,
x2,
x3,
x4) =
U1_gga(
x2,
x4)
s(
x1) =
s(
x1)
U3_gga(
x1,
x2,
x3,
x4,
x5) =
U3_gga(
x5)
U2_gga(
x1,
x2,
x3,
x4) =
U2_gga(
x4)
times_in_gga(
x1,
x2,
x3) =
times_in_gga(
x1,
x2)
times_out_gga(
x1,
x2,
x3) =
times_out_gga(
x3)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x2,
x4)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x4)
plus_in_gga(
x1,
x2,
x3) =
plus_in_gga(
x1,
x2)
plus_out_gga(
x1,
x2,
x3) =
plus_out_gga(
x3)
U4_gga(
x1,
x2,
x3,
x4) =
U4_gga(
x4)
CONVERT_IN_GGA(
x1,
x2,
x3) =
CONVERT_IN_GGA(
x1,
x2)
U1_GGA(
x1,
x2,
x3,
x4) =
U1_GGA(
x2,
x4)
U3_GGA(
x1,
x2,
x3,
x4,
x5) =
U3_GGA(
x5)
U2_GGA(
x1,
x2,
x3,
x4) =
U2_GGA(
x4)
TIMES_IN_GGA(
x1,
x2,
x3) =
TIMES_IN_GGA(
x1,
x2)
U5_GGA(
x1,
x2,
x3,
x4) =
U5_GGA(
x2,
x4)
U6_GGA(
x1,
x2,
x3,
x4) =
U6_GGA(
x4)
PLUS_IN_GGA(
x1,
x2,
x3) =
PLUS_IN_GGA(
x1,
x2)
U4_GGA(
x1,
x2,
x3,
x4) =
U4_GGA(
x4)
We have to consider all (P,R,Pi)-chains
(5) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 8 less nodes.
(6) Complex Obligation (AND)
(7) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
PLUS_IN_GGA(s(X), Y, s(Z)) → PLUS_IN_GGA(X, Y, Z)
The TRS R consists of the following rules:
convert_in_gga([], B, 0) → convert_out_gga([], B, 0)
convert_in_gga(.(0, XS), B, X) → U1_gga(XS, B, X, convert_in_gga(XS, B, Y))
convert_in_gga(.(s(Y), XS), B, s(X)) → U3_gga(Y, XS, B, X, convert_in_gga(.(Y, XS), B, X))
U3_gga(Y, XS, B, X, convert_out_gga(.(Y, XS), B, X)) → convert_out_gga(.(s(Y), XS), B, s(X))
U1_gga(XS, B, X, convert_out_gga(XS, B, Y)) → U2_gga(XS, B, X, times_in_gga(Y, B, X))
times_in_gga(0, Y, 0) → times_out_gga(0, Y, 0)
times_in_gga(s(X), Y, Z) → U5_gga(X, Y, Z, times_in_gga(X, Y, U))
U5_gga(X, Y, Z, times_out_gga(X, Y, U)) → U6_gga(X, Y, Z, plus_in_gga(Y, U, Z))
plus_in_gga(0, Y, Y) → plus_out_gga(0, Y, Y)
plus_in_gga(s(X), Y, s(Z)) → U4_gga(X, Y, Z, plus_in_gga(X, Y, Z))
U4_gga(X, Y, Z, plus_out_gga(X, Y, Z)) → plus_out_gga(s(X), Y, s(Z))
U6_gga(X, Y, Z, plus_out_gga(Y, U, Z)) → times_out_gga(s(X), Y, Z)
U2_gga(XS, B, X, times_out_gga(Y, B, X)) → convert_out_gga(.(0, XS), B, X)
The argument filtering Pi contains the following mapping:
convert_in_gga(
x1,
x2,
x3) =
convert_in_gga(
x1,
x2)
[] =
[]
convert_out_gga(
x1,
x2,
x3) =
convert_out_gga(
x3)
.(
x1,
x2) =
.(
x1,
x2)
0 =
0
U1_gga(
x1,
x2,
x3,
x4) =
U1_gga(
x2,
x4)
s(
x1) =
s(
x1)
U3_gga(
x1,
x2,
x3,
x4,
x5) =
U3_gga(
x5)
U2_gga(
x1,
x2,
x3,
x4) =
U2_gga(
x4)
times_in_gga(
x1,
x2,
x3) =
times_in_gga(
x1,
x2)
times_out_gga(
x1,
x2,
x3) =
times_out_gga(
x3)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x2,
x4)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x4)
plus_in_gga(
x1,
x2,
x3) =
plus_in_gga(
x1,
x2)
plus_out_gga(
x1,
x2,
x3) =
plus_out_gga(
x3)
U4_gga(
x1,
x2,
x3,
x4) =
U4_gga(
x4)
PLUS_IN_GGA(
x1,
x2,
x3) =
PLUS_IN_GGA(
x1,
x2)
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:
PLUS_IN_GGA(s(X), Y, s(Z)) → PLUS_IN_GGA(X, Y, Z)
R is empty.
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
PLUS_IN_GGA(
x1,
x2,
x3) =
PLUS_IN_GGA(
x1,
x2)
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:
PLUS_IN_GGA(s(X), Y) → PLUS_IN_GGA(X, Y)
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:
- PLUS_IN_GGA(s(X), Y) → PLUS_IN_GGA(X, Y)
The graph contains the following edges 1 > 1, 2 >= 2
(13) TRUE
(14) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
TIMES_IN_GGA(s(X), Y, Z) → TIMES_IN_GGA(X, Y, U)
The TRS R consists of the following rules:
convert_in_gga([], B, 0) → convert_out_gga([], B, 0)
convert_in_gga(.(0, XS), B, X) → U1_gga(XS, B, X, convert_in_gga(XS, B, Y))
convert_in_gga(.(s(Y), XS), B, s(X)) → U3_gga(Y, XS, B, X, convert_in_gga(.(Y, XS), B, X))
U3_gga(Y, XS, B, X, convert_out_gga(.(Y, XS), B, X)) → convert_out_gga(.(s(Y), XS), B, s(X))
U1_gga(XS, B, X, convert_out_gga(XS, B, Y)) → U2_gga(XS, B, X, times_in_gga(Y, B, X))
times_in_gga(0, Y, 0) → times_out_gga(0, Y, 0)
times_in_gga(s(X), Y, Z) → U5_gga(X, Y, Z, times_in_gga(X, Y, U))
U5_gga(X, Y, Z, times_out_gga(X, Y, U)) → U6_gga(X, Y, Z, plus_in_gga(Y, U, Z))
plus_in_gga(0, Y, Y) → plus_out_gga(0, Y, Y)
plus_in_gga(s(X), Y, s(Z)) → U4_gga(X, Y, Z, plus_in_gga(X, Y, Z))
U4_gga(X, Y, Z, plus_out_gga(X, Y, Z)) → plus_out_gga(s(X), Y, s(Z))
U6_gga(X, Y, Z, plus_out_gga(Y, U, Z)) → times_out_gga(s(X), Y, Z)
U2_gga(XS, B, X, times_out_gga(Y, B, X)) → convert_out_gga(.(0, XS), B, X)
The argument filtering Pi contains the following mapping:
convert_in_gga(
x1,
x2,
x3) =
convert_in_gga(
x1,
x2)
[] =
[]
convert_out_gga(
x1,
x2,
x3) =
convert_out_gga(
x3)
.(
x1,
x2) =
.(
x1,
x2)
0 =
0
U1_gga(
x1,
x2,
x3,
x4) =
U1_gga(
x2,
x4)
s(
x1) =
s(
x1)
U3_gga(
x1,
x2,
x3,
x4,
x5) =
U3_gga(
x5)
U2_gga(
x1,
x2,
x3,
x4) =
U2_gga(
x4)
times_in_gga(
x1,
x2,
x3) =
times_in_gga(
x1,
x2)
times_out_gga(
x1,
x2,
x3) =
times_out_gga(
x3)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x2,
x4)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x4)
plus_in_gga(
x1,
x2,
x3) =
plus_in_gga(
x1,
x2)
plus_out_gga(
x1,
x2,
x3) =
plus_out_gga(
x3)
U4_gga(
x1,
x2,
x3,
x4) =
U4_gga(
x4)
TIMES_IN_GGA(
x1,
x2,
x3) =
TIMES_IN_GGA(
x1,
x2)
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:
TIMES_IN_GGA(s(X), Y, Z) → TIMES_IN_GGA(X, Y, U)
R is empty.
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
TIMES_IN_GGA(
x1,
x2,
x3) =
TIMES_IN_GGA(
x1,
x2)
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:
TIMES_IN_GGA(s(X), Y) → TIMES_IN_GGA(X, Y)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(19) 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:
- TIMES_IN_GGA(s(X), Y) → TIMES_IN_GGA(X, Y)
The graph contains the following edges 1 > 1, 2 >= 2
(20) TRUE
(21) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
CONVERT_IN_GGA(.(s(Y), XS), B, s(X)) → CONVERT_IN_GGA(.(Y, XS), B, X)
CONVERT_IN_GGA(.(0, XS), B, X) → CONVERT_IN_GGA(XS, B, Y)
The TRS R consists of the following rules:
convert_in_gga([], B, 0) → convert_out_gga([], B, 0)
convert_in_gga(.(0, XS), B, X) → U1_gga(XS, B, X, convert_in_gga(XS, B, Y))
convert_in_gga(.(s(Y), XS), B, s(X)) → U3_gga(Y, XS, B, X, convert_in_gga(.(Y, XS), B, X))
U3_gga(Y, XS, B, X, convert_out_gga(.(Y, XS), B, X)) → convert_out_gga(.(s(Y), XS), B, s(X))
U1_gga(XS, B, X, convert_out_gga(XS, B, Y)) → U2_gga(XS, B, X, times_in_gga(Y, B, X))
times_in_gga(0, Y, 0) → times_out_gga(0, Y, 0)
times_in_gga(s(X), Y, Z) → U5_gga(X, Y, Z, times_in_gga(X, Y, U))
U5_gga(X, Y, Z, times_out_gga(X, Y, U)) → U6_gga(X, Y, Z, plus_in_gga(Y, U, Z))
plus_in_gga(0, Y, Y) → plus_out_gga(0, Y, Y)
plus_in_gga(s(X), Y, s(Z)) → U4_gga(X, Y, Z, plus_in_gga(X, Y, Z))
U4_gga(X, Y, Z, plus_out_gga(X, Y, Z)) → plus_out_gga(s(X), Y, s(Z))
U6_gga(X, Y, Z, plus_out_gga(Y, U, Z)) → times_out_gga(s(X), Y, Z)
U2_gga(XS, B, X, times_out_gga(Y, B, X)) → convert_out_gga(.(0, XS), B, X)
The argument filtering Pi contains the following mapping:
convert_in_gga(
x1,
x2,
x3) =
convert_in_gga(
x1,
x2)
[] =
[]
convert_out_gga(
x1,
x2,
x3) =
convert_out_gga(
x3)
.(
x1,
x2) =
.(
x1,
x2)
0 =
0
U1_gga(
x1,
x2,
x3,
x4) =
U1_gga(
x2,
x4)
s(
x1) =
s(
x1)
U3_gga(
x1,
x2,
x3,
x4,
x5) =
U3_gga(
x5)
U2_gga(
x1,
x2,
x3,
x4) =
U2_gga(
x4)
times_in_gga(
x1,
x2,
x3) =
times_in_gga(
x1,
x2)
times_out_gga(
x1,
x2,
x3) =
times_out_gga(
x3)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x2,
x4)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x4)
plus_in_gga(
x1,
x2,
x3) =
plus_in_gga(
x1,
x2)
plus_out_gga(
x1,
x2,
x3) =
plus_out_gga(
x3)
U4_gga(
x1,
x2,
x3,
x4) =
U4_gga(
x4)
CONVERT_IN_GGA(
x1,
x2,
x3) =
CONVERT_IN_GGA(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(22) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(23) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
CONVERT_IN_GGA(.(s(Y), XS), B, s(X)) → CONVERT_IN_GGA(.(Y, XS), B, X)
CONVERT_IN_GGA(.(0, XS), B, X) → CONVERT_IN_GGA(XS, B, Y)
R is empty.
The argument filtering Pi contains the following mapping:
.(
x1,
x2) =
.(
x1,
x2)
0 =
0
s(
x1) =
s(
x1)
CONVERT_IN_GGA(
x1,
x2,
x3) =
CONVERT_IN_GGA(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(24) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(25) Obligation:
Q DP problem:
The TRS P consists of the following rules:
CONVERT_IN_GGA(.(s(Y), XS), B) → CONVERT_IN_GGA(.(Y, XS), B)
CONVERT_IN_GGA(.(0, XS), B) → CONVERT_IN_GGA(XS, B)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(26) UsableRulesReductionPairsProof (EQUIVALENT transformation)
By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.
The following dependency pairs can be deleted:
CONVERT_IN_GGA(.(s(Y), XS), B) → CONVERT_IN_GGA(.(Y, XS), B)
CONVERT_IN_GGA(.(0, XS), B) → CONVERT_IN_GGA(XS, B)
No rules are removed from R.
Used ordering: POLO with Polynomial interpretation [POLO]:
POL(.(x1, x2)) = 2·x1 + 2·x2
POL(0) = 0
POL(CONVERT_IN_GGA(x1, x2)) = 2·x1 + x2
POL(s(x1)) = 2·x1
(27) Obligation:
Q DP problem:
P is empty.
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(28) PrologToPiTRSProof (SOUND transformation)
We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
convert_in: (b,b,f)
times_in: (b,b,f)
plus_in: (b,b,f)
Transforming
Prolog into the following
Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
convert_in_gga([], B, 0) → convert_out_gga([], B, 0)
convert_in_gga(.(0, XS), B, X) → U1_gga(XS, B, X, convert_in_gga(XS, B, Y))
convert_in_gga(.(s(Y), XS), B, s(X)) → U3_gga(Y, XS, B, X, convert_in_gga(.(Y, XS), B, X))
U3_gga(Y, XS, B, X, convert_out_gga(.(Y, XS), B, X)) → convert_out_gga(.(s(Y), XS), B, s(X))
U1_gga(XS, B, X, convert_out_gga(XS, B, Y)) → U2_gga(XS, B, X, times_in_gga(Y, B, X))
times_in_gga(0, Y, 0) → times_out_gga(0, Y, 0)
times_in_gga(s(X), Y, Z) → U5_gga(X, Y, Z, times_in_gga(X, Y, U))
U5_gga(X, Y, Z, times_out_gga(X, Y, U)) → U6_gga(X, Y, Z, plus_in_gga(Y, U, Z))
plus_in_gga(0, Y, Y) → plus_out_gga(0, Y, Y)
plus_in_gga(s(X), Y, s(Z)) → U4_gga(X, Y, Z, plus_in_gga(X, Y, Z))
U4_gga(X, Y, Z, plus_out_gga(X, Y, Z)) → plus_out_gga(s(X), Y, s(Z))
U6_gga(X, Y, Z, plus_out_gga(Y, U, Z)) → times_out_gga(s(X), Y, Z)
U2_gga(XS, B, X, times_out_gga(Y, B, X)) → convert_out_gga(.(0, XS), B, X)
The argument filtering Pi contains the following mapping:
convert_in_gga(
x1,
x2,
x3) =
convert_in_gga(
x1,
x2)
[] =
[]
convert_out_gga(
x1,
x2,
x3) =
convert_out_gga(
x1,
x2,
x3)
.(
x1,
x2) =
.(
x1,
x2)
0 =
0
U1_gga(
x1,
x2,
x3,
x4) =
U1_gga(
x1,
x2,
x4)
s(
x1) =
s(
x1)
U3_gga(
x1,
x2,
x3,
x4,
x5) =
U3_gga(
x1,
x2,
x3,
x5)
U2_gga(
x1,
x2,
x3,
x4) =
U2_gga(
x1,
x2,
x4)
times_in_gga(
x1,
x2,
x3) =
times_in_gga(
x1,
x2)
times_out_gga(
x1,
x2,
x3) =
times_out_gga(
x1,
x2,
x3)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x1,
x2,
x4)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x1,
x2,
x4)
plus_in_gga(
x1,
x2,
x3) =
plus_in_gga(
x1,
x2)
plus_out_gga(
x1,
x2,
x3) =
plus_out_gga(
x1,
x2,
x3)
U4_gga(
x1,
x2,
x3,
x4) =
U4_gga(
x1,
x2,
x4)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
(29) Obligation:
Pi-finite rewrite system:
The TRS R consists of the following rules:
convert_in_gga([], B, 0) → convert_out_gga([], B, 0)
convert_in_gga(.(0, XS), B, X) → U1_gga(XS, B, X, convert_in_gga(XS, B, Y))
convert_in_gga(.(s(Y), XS), B, s(X)) → U3_gga(Y, XS, B, X, convert_in_gga(.(Y, XS), B, X))
U3_gga(Y, XS, B, X, convert_out_gga(.(Y, XS), B, X)) → convert_out_gga(.(s(Y), XS), B, s(X))
U1_gga(XS, B, X, convert_out_gga(XS, B, Y)) → U2_gga(XS, B, X, times_in_gga(Y, B, X))
times_in_gga(0, Y, 0) → times_out_gga(0, Y, 0)
times_in_gga(s(X), Y, Z) → U5_gga(X, Y, Z, times_in_gga(X, Y, U))
U5_gga(X, Y, Z, times_out_gga(X, Y, U)) → U6_gga(X, Y, Z, plus_in_gga(Y, U, Z))
plus_in_gga(0, Y, Y) → plus_out_gga(0, Y, Y)
plus_in_gga(s(X), Y, s(Z)) → U4_gga(X, Y, Z, plus_in_gga(X, Y, Z))
U4_gga(X, Y, Z, plus_out_gga(X, Y, Z)) → plus_out_gga(s(X), Y, s(Z))
U6_gga(X, Y, Z, plus_out_gga(Y, U, Z)) → times_out_gga(s(X), Y, Z)
U2_gga(XS, B, X, times_out_gga(Y, B, X)) → convert_out_gga(.(0, XS), B, X)
The argument filtering Pi contains the following mapping:
convert_in_gga(
x1,
x2,
x3) =
convert_in_gga(
x1,
x2)
[] =
[]
convert_out_gga(
x1,
x2,
x3) =
convert_out_gga(
x1,
x2,
x3)
.(
x1,
x2) =
.(
x1,
x2)
0 =
0
U1_gga(
x1,
x2,
x3,
x4) =
U1_gga(
x1,
x2,
x4)
s(
x1) =
s(
x1)
U3_gga(
x1,
x2,
x3,
x4,
x5) =
U3_gga(
x1,
x2,
x3,
x5)
U2_gga(
x1,
x2,
x3,
x4) =
U2_gga(
x1,
x2,
x4)
times_in_gga(
x1,
x2,
x3) =
times_in_gga(
x1,
x2)
times_out_gga(
x1,
x2,
x3) =
times_out_gga(
x1,
x2,
x3)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x1,
x2,
x4)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x1,
x2,
x4)
plus_in_gga(
x1,
x2,
x3) =
plus_in_gga(
x1,
x2)
plus_out_gga(
x1,
x2,
x3) =
plus_out_gga(
x1,
x2,
x3)
U4_gga(
x1,
x2,
x3,
x4) =
U4_gga(
x1,
x2,
x4)
(30) 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:
CONVERT_IN_GGA(.(0, XS), B, X) → U1_GGA(XS, B, X, convert_in_gga(XS, B, Y))
CONVERT_IN_GGA(.(0, XS), B, X) → CONVERT_IN_GGA(XS, B, Y)
CONVERT_IN_GGA(.(s(Y), XS), B, s(X)) → U3_GGA(Y, XS, B, X, convert_in_gga(.(Y, XS), B, X))
CONVERT_IN_GGA(.(s(Y), XS), B, s(X)) → CONVERT_IN_GGA(.(Y, XS), B, X)
U1_GGA(XS, B, X, convert_out_gga(XS, B, Y)) → U2_GGA(XS, B, X, times_in_gga(Y, B, X))
U1_GGA(XS, B, X, convert_out_gga(XS, B, Y)) → TIMES_IN_GGA(Y, B, X)
TIMES_IN_GGA(s(X), Y, Z) → U5_GGA(X, Y, Z, times_in_gga(X, Y, U))
TIMES_IN_GGA(s(X), Y, Z) → TIMES_IN_GGA(X, Y, U)
U5_GGA(X, Y, Z, times_out_gga(X, Y, U)) → U6_GGA(X, Y, Z, plus_in_gga(Y, U, Z))
U5_GGA(X, Y, Z, times_out_gga(X, Y, U)) → PLUS_IN_GGA(Y, U, Z)
PLUS_IN_GGA(s(X), Y, s(Z)) → U4_GGA(X, Y, Z, plus_in_gga(X, Y, Z))
PLUS_IN_GGA(s(X), Y, s(Z)) → PLUS_IN_GGA(X, Y, Z)
The TRS R consists of the following rules:
convert_in_gga([], B, 0) → convert_out_gga([], B, 0)
convert_in_gga(.(0, XS), B, X) → U1_gga(XS, B, X, convert_in_gga(XS, B, Y))
convert_in_gga(.(s(Y), XS), B, s(X)) → U3_gga(Y, XS, B, X, convert_in_gga(.(Y, XS), B, X))
U3_gga(Y, XS, B, X, convert_out_gga(.(Y, XS), B, X)) → convert_out_gga(.(s(Y), XS), B, s(X))
U1_gga(XS, B, X, convert_out_gga(XS, B, Y)) → U2_gga(XS, B, X, times_in_gga(Y, B, X))
times_in_gga(0, Y, 0) → times_out_gga(0, Y, 0)
times_in_gga(s(X), Y, Z) → U5_gga(X, Y, Z, times_in_gga(X, Y, U))
U5_gga(X, Y, Z, times_out_gga(X, Y, U)) → U6_gga(X, Y, Z, plus_in_gga(Y, U, Z))
plus_in_gga(0, Y, Y) → plus_out_gga(0, Y, Y)
plus_in_gga(s(X), Y, s(Z)) → U4_gga(X, Y, Z, plus_in_gga(X, Y, Z))
U4_gga(X, Y, Z, plus_out_gga(X, Y, Z)) → plus_out_gga(s(X), Y, s(Z))
U6_gga(X, Y, Z, plus_out_gga(Y, U, Z)) → times_out_gga(s(X), Y, Z)
U2_gga(XS, B, X, times_out_gga(Y, B, X)) → convert_out_gga(.(0, XS), B, X)
The argument filtering Pi contains the following mapping:
convert_in_gga(
x1,
x2,
x3) =
convert_in_gga(
x1,
x2)
[] =
[]
convert_out_gga(
x1,
x2,
x3) =
convert_out_gga(
x1,
x2,
x3)
.(
x1,
x2) =
.(
x1,
x2)
0 =
0
U1_gga(
x1,
x2,
x3,
x4) =
U1_gga(
x1,
x2,
x4)
s(
x1) =
s(
x1)
U3_gga(
x1,
x2,
x3,
x4,
x5) =
U3_gga(
x1,
x2,
x3,
x5)
U2_gga(
x1,
x2,
x3,
x4) =
U2_gga(
x1,
x2,
x4)
times_in_gga(
x1,
x2,
x3) =
times_in_gga(
x1,
x2)
times_out_gga(
x1,
x2,
x3) =
times_out_gga(
x1,
x2,
x3)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x1,
x2,
x4)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x1,
x2,
x4)
plus_in_gga(
x1,
x2,
x3) =
plus_in_gga(
x1,
x2)
plus_out_gga(
x1,
x2,
x3) =
plus_out_gga(
x1,
x2,
x3)
U4_gga(
x1,
x2,
x3,
x4) =
U4_gga(
x1,
x2,
x4)
CONVERT_IN_GGA(
x1,
x2,
x3) =
CONVERT_IN_GGA(
x1,
x2)
U1_GGA(
x1,
x2,
x3,
x4) =
U1_GGA(
x1,
x2,
x4)
U3_GGA(
x1,
x2,
x3,
x4,
x5) =
U3_GGA(
x1,
x2,
x3,
x5)
U2_GGA(
x1,
x2,
x3,
x4) =
U2_GGA(
x1,
x2,
x4)
TIMES_IN_GGA(
x1,
x2,
x3) =
TIMES_IN_GGA(
x1,
x2)
U5_GGA(
x1,
x2,
x3,
x4) =
U5_GGA(
x1,
x2,
x4)
U6_GGA(
x1,
x2,
x3,
x4) =
U6_GGA(
x1,
x2,
x4)
PLUS_IN_GGA(
x1,
x2,
x3) =
PLUS_IN_GGA(
x1,
x2)
U4_GGA(
x1,
x2,
x3,
x4) =
U4_GGA(
x1,
x2,
x4)
We have to consider all (P,R,Pi)-chains
(31) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
CONVERT_IN_GGA(.(0, XS), B, X) → U1_GGA(XS, B, X, convert_in_gga(XS, B, Y))
CONVERT_IN_GGA(.(0, XS), B, X) → CONVERT_IN_GGA(XS, B, Y)
CONVERT_IN_GGA(.(s(Y), XS), B, s(X)) → U3_GGA(Y, XS, B, X, convert_in_gga(.(Y, XS), B, X))
CONVERT_IN_GGA(.(s(Y), XS), B, s(X)) → CONVERT_IN_GGA(.(Y, XS), B, X)
U1_GGA(XS, B, X, convert_out_gga(XS, B, Y)) → U2_GGA(XS, B, X, times_in_gga(Y, B, X))
U1_GGA(XS, B, X, convert_out_gga(XS, B, Y)) → TIMES_IN_GGA(Y, B, X)
TIMES_IN_GGA(s(X), Y, Z) → U5_GGA(X, Y, Z, times_in_gga(X, Y, U))
TIMES_IN_GGA(s(X), Y, Z) → TIMES_IN_GGA(X, Y, U)
U5_GGA(X, Y, Z, times_out_gga(X, Y, U)) → U6_GGA(X, Y, Z, plus_in_gga(Y, U, Z))
U5_GGA(X, Y, Z, times_out_gga(X, Y, U)) → PLUS_IN_GGA(Y, U, Z)
PLUS_IN_GGA(s(X), Y, s(Z)) → U4_GGA(X, Y, Z, plus_in_gga(X, Y, Z))
PLUS_IN_GGA(s(X), Y, s(Z)) → PLUS_IN_GGA(X, Y, Z)
The TRS R consists of the following rules:
convert_in_gga([], B, 0) → convert_out_gga([], B, 0)
convert_in_gga(.(0, XS), B, X) → U1_gga(XS, B, X, convert_in_gga(XS, B, Y))
convert_in_gga(.(s(Y), XS), B, s(X)) → U3_gga(Y, XS, B, X, convert_in_gga(.(Y, XS), B, X))
U3_gga(Y, XS, B, X, convert_out_gga(.(Y, XS), B, X)) → convert_out_gga(.(s(Y), XS), B, s(X))
U1_gga(XS, B, X, convert_out_gga(XS, B, Y)) → U2_gga(XS, B, X, times_in_gga(Y, B, X))
times_in_gga(0, Y, 0) → times_out_gga(0, Y, 0)
times_in_gga(s(X), Y, Z) → U5_gga(X, Y, Z, times_in_gga(X, Y, U))
U5_gga(X, Y, Z, times_out_gga(X, Y, U)) → U6_gga(X, Y, Z, plus_in_gga(Y, U, Z))
plus_in_gga(0, Y, Y) → plus_out_gga(0, Y, Y)
plus_in_gga(s(X), Y, s(Z)) → U4_gga(X, Y, Z, plus_in_gga(X, Y, Z))
U4_gga(X, Y, Z, plus_out_gga(X, Y, Z)) → plus_out_gga(s(X), Y, s(Z))
U6_gga(X, Y, Z, plus_out_gga(Y, U, Z)) → times_out_gga(s(X), Y, Z)
U2_gga(XS, B, X, times_out_gga(Y, B, X)) → convert_out_gga(.(0, XS), B, X)
The argument filtering Pi contains the following mapping:
convert_in_gga(
x1,
x2,
x3) =
convert_in_gga(
x1,
x2)
[] =
[]
convert_out_gga(
x1,
x2,
x3) =
convert_out_gga(
x1,
x2,
x3)
.(
x1,
x2) =
.(
x1,
x2)
0 =
0
U1_gga(
x1,
x2,
x3,
x4) =
U1_gga(
x1,
x2,
x4)
s(
x1) =
s(
x1)
U3_gga(
x1,
x2,
x3,
x4,
x5) =
U3_gga(
x1,
x2,
x3,
x5)
U2_gga(
x1,
x2,
x3,
x4) =
U2_gga(
x1,
x2,
x4)
times_in_gga(
x1,
x2,
x3) =
times_in_gga(
x1,
x2)
times_out_gga(
x1,
x2,
x3) =
times_out_gga(
x1,
x2,
x3)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x1,
x2,
x4)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x1,
x2,
x4)
plus_in_gga(
x1,
x2,
x3) =
plus_in_gga(
x1,
x2)
plus_out_gga(
x1,
x2,
x3) =
plus_out_gga(
x1,
x2,
x3)
U4_gga(
x1,
x2,
x3,
x4) =
U4_gga(
x1,
x2,
x4)
CONVERT_IN_GGA(
x1,
x2,
x3) =
CONVERT_IN_GGA(
x1,
x2)
U1_GGA(
x1,
x2,
x3,
x4) =
U1_GGA(
x1,
x2,
x4)
U3_GGA(
x1,
x2,
x3,
x4,
x5) =
U3_GGA(
x1,
x2,
x3,
x5)
U2_GGA(
x1,
x2,
x3,
x4) =
U2_GGA(
x1,
x2,
x4)
TIMES_IN_GGA(
x1,
x2,
x3) =
TIMES_IN_GGA(
x1,
x2)
U5_GGA(
x1,
x2,
x3,
x4) =
U5_GGA(
x1,
x2,
x4)
U6_GGA(
x1,
x2,
x3,
x4) =
U6_GGA(
x1,
x2,
x4)
PLUS_IN_GGA(
x1,
x2,
x3) =
PLUS_IN_GGA(
x1,
x2)
U4_GGA(
x1,
x2,
x3,
x4) =
U4_GGA(
x1,
x2,
x4)
We have to consider all (P,R,Pi)-chains
(32) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 8 less nodes.
(33) Complex Obligation (AND)
(34) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
PLUS_IN_GGA(s(X), Y, s(Z)) → PLUS_IN_GGA(X, Y, Z)
The TRS R consists of the following rules:
convert_in_gga([], B, 0) → convert_out_gga([], B, 0)
convert_in_gga(.(0, XS), B, X) → U1_gga(XS, B, X, convert_in_gga(XS, B, Y))
convert_in_gga(.(s(Y), XS), B, s(X)) → U3_gga(Y, XS, B, X, convert_in_gga(.(Y, XS), B, X))
U3_gga(Y, XS, B, X, convert_out_gga(.(Y, XS), B, X)) → convert_out_gga(.(s(Y), XS), B, s(X))
U1_gga(XS, B, X, convert_out_gga(XS, B, Y)) → U2_gga(XS, B, X, times_in_gga(Y, B, X))
times_in_gga(0, Y, 0) → times_out_gga(0, Y, 0)
times_in_gga(s(X), Y, Z) → U5_gga(X, Y, Z, times_in_gga(X, Y, U))
U5_gga(X, Y, Z, times_out_gga(X, Y, U)) → U6_gga(X, Y, Z, plus_in_gga(Y, U, Z))
plus_in_gga(0, Y, Y) → plus_out_gga(0, Y, Y)
plus_in_gga(s(X), Y, s(Z)) → U4_gga(X, Y, Z, plus_in_gga(X, Y, Z))
U4_gga(X, Y, Z, plus_out_gga(X, Y, Z)) → plus_out_gga(s(X), Y, s(Z))
U6_gga(X, Y, Z, plus_out_gga(Y, U, Z)) → times_out_gga(s(X), Y, Z)
U2_gga(XS, B, X, times_out_gga(Y, B, X)) → convert_out_gga(.(0, XS), B, X)
The argument filtering Pi contains the following mapping:
convert_in_gga(
x1,
x2,
x3) =
convert_in_gga(
x1,
x2)
[] =
[]
convert_out_gga(
x1,
x2,
x3) =
convert_out_gga(
x1,
x2,
x3)
.(
x1,
x2) =
.(
x1,
x2)
0 =
0
U1_gga(
x1,
x2,
x3,
x4) =
U1_gga(
x1,
x2,
x4)
s(
x1) =
s(
x1)
U3_gga(
x1,
x2,
x3,
x4,
x5) =
U3_gga(
x1,
x2,
x3,
x5)
U2_gga(
x1,
x2,
x3,
x4) =
U2_gga(
x1,
x2,
x4)
times_in_gga(
x1,
x2,
x3) =
times_in_gga(
x1,
x2)
times_out_gga(
x1,
x2,
x3) =
times_out_gga(
x1,
x2,
x3)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x1,
x2,
x4)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x1,
x2,
x4)
plus_in_gga(
x1,
x2,
x3) =
plus_in_gga(
x1,
x2)
plus_out_gga(
x1,
x2,
x3) =
plus_out_gga(
x1,
x2,
x3)
U4_gga(
x1,
x2,
x3,
x4) =
U4_gga(
x1,
x2,
x4)
PLUS_IN_GGA(
x1,
x2,
x3) =
PLUS_IN_GGA(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(35) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(36) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
PLUS_IN_GGA(s(X), Y, s(Z)) → PLUS_IN_GGA(X, Y, Z)
R is empty.
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
PLUS_IN_GGA(
x1,
x2,
x3) =
PLUS_IN_GGA(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(37) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(38) Obligation:
Q DP problem:
The TRS P consists of the following rules:
PLUS_IN_GGA(s(X), Y) → PLUS_IN_GGA(X, Y)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(39) 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:
- PLUS_IN_GGA(s(X), Y) → PLUS_IN_GGA(X, Y)
The graph contains the following edges 1 > 1, 2 >= 2
(40) TRUE
(41) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
TIMES_IN_GGA(s(X), Y, Z) → TIMES_IN_GGA(X, Y, U)
The TRS R consists of the following rules:
convert_in_gga([], B, 0) → convert_out_gga([], B, 0)
convert_in_gga(.(0, XS), B, X) → U1_gga(XS, B, X, convert_in_gga(XS, B, Y))
convert_in_gga(.(s(Y), XS), B, s(X)) → U3_gga(Y, XS, B, X, convert_in_gga(.(Y, XS), B, X))
U3_gga(Y, XS, B, X, convert_out_gga(.(Y, XS), B, X)) → convert_out_gga(.(s(Y), XS), B, s(X))
U1_gga(XS, B, X, convert_out_gga(XS, B, Y)) → U2_gga(XS, B, X, times_in_gga(Y, B, X))
times_in_gga(0, Y, 0) → times_out_gga(0, Y, 0)
times_in_gga(s(X), Y, Z) → U5_gga(X, Y, Z, times_in_gga(X, Y, U))
U5_gga(X, Y, Z, times_out_gga(X, Y, U)) → U6_gga(X, Y, Z, plus_in_gga(Y, U, Z))
plus_in_gga(0, Y, Y) → plus_out_gga(0, Y, Y)
plus_in_gga(s(X), Y, s(Z)) → U4_gga(X, Y, Z, plus_in_gga(X, Y, Z))
U4_gga(X, Y, Z, plus_out_gga(X, Y, Z)) → plus_out_gga(s(X), Y, s(Z))
U6_gga(X, Y, Z, plus_out_gga(Y, U, Z)) → times_out_gga(s(X), Y, Z)
U2_gga(XS, B, X, times_out_gga(Y, B, X)) → convert_out_gga(.(0, XS), B, X)
The argument filtering Pi contains the following mapping:
convert_in_gga(
x1,
x2,
x3) =
convert_in_gga(
x1,
x2)
[] =
[]
convert_out_gga(
x1,
x2,
x3) =
convert_out_gga(
x1,
x2,
x3)
.(
x1,
x2) =
.(
x1,
x2)
0 =
0
U1_gga(
x1,
x2,
x3,
x4) =
U1_gga(
x1,
x2,
x4)
s(
x1) =
s(
x1)
U3_gga(
x1,
x2,
x3,
x4,
x5) =
U3_gga(
x1,
x2,
x3,
x5)
U2_gga(
x1,
x2,
x3,
x4) =
U2_gga(
x1,
x2,
x4)
times_in_gga(
x1,
x2,
x3) =
times_in_gga(
x1,
x2)
times_out_gga(
x1,
x2,
x3) =
times_out_gga(
x1,
x2,
x3)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x1,
x2,
x4)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x1,
x2,
x4)
plus_in_gga(
x1,
x2,
x3) =
plus_in_gga(
x1,
x2)
plus_out_gga(
x1,
x2,
x3) =
plus_out_gga(
x1,
x2,
x3)
U4_gga(
x1,
x2,
x3,
x4) =
U4_gga(
x1,
x2,
x4)
TIMES_IN_GGA(
x1,
x2,
x3) =
TIMES_IN_GGA(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(42) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(43) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
TIMES_IN_GGA(s(X), Y, Z) → TIMES_IN_GGA(X, Y, U)
R is empty.
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
TIMES_IN_GGA(
x1,
x2,
x3) =
TIMES_IN_GGA(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(44) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(45) Obligation:
Q DP problem:
The TRS P consists of the following rules:
TIMES_IN_GGA(s(X), Y) → TIMES_IN_GGA(X, Y)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(46) 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:
- TIMES_IN_GGA(s(X), Y) → TIMES_IN_GGA(X, Y)
The graph contains the following edges 1 > 1, 2 >= 2
(47) TRUE
(48) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
CONVERT_IN_GGA(.(s(Y), XS), B, s(X)) → CONVERT_IN_GGA(.(Y, XS), B, X)
CONVERT_IN_GGA(.(0, XS), B, X) → CONVERT_IN_GGA(XS, B, Y)
The TRS R consists of the following rules:
convert_in_gga([], B, 0) → convert_out_gga([], B, 0)
convert_in_gga(.(0, XS), B, X) → U1_gga(XS, B, X, convert_in_gga(XS, B, Y))
convert_in_gga(.(s(Y), XS), B, s(X)) → U3_gga(Y, XS, B, X, convert_in_gga(.(Y, XS), B, X))
U3_gga(Y, XS, B, X, convert_out_gga(.(Y, XS), B, X)) → convert_out_gga(.(s(Y), XS), B, s(X))
U1_gga(XS, B, X, convert_out_gga(XS, B, Y)) → U2_gga(XS, B, X, times_in_gga(Y, B, X))
times_in_gga(0, Y, 0) → times_out_gga(0, Y, 0)
times_in_gga(s(X), Y, Z) → U5_gga(X, Y, Z, times_in_gga(X, Y, U))
U5_gga(X, Y, Z, times_out_gga(X, Y, U)) → U6_gga(X, Y, Z, plus_in_gga(Y, U, Z))
plus_in_gga(0, Y, Y) → plus_out_gga(0, Y, Y)
plus_in_gga(s(X), Y, s(Z)) → U4_gga(X, Y, Z, plus_in_gga(X, Y, Z))
U4_gga(X, Y, Z, plus_out_gga(X, Y, Z)) → plus_out_gga(s(X), Y, s(Z))
U6_gga(X, Y, Z, plus_out_gga(Y, U, Z)) → times_out_gga(s(X), Y, Z)
U2_gga(XS, B, X, times_out_gga(Y, B, X)) → convert_out_gga(.(0, XS), B, X)
The argument filtering Pi contains the following mapping:
convert_in_gga(
x1,
x2,
x3) =
convert_in_gga(
x1,
x2)
[] =
[]
convert_out_gga(
x1,
x2,
x3) =
convert_out_gga(
x1,
x2,
x3)
.(
x1,
x2) =
.(
x1,
x2)
0 =
0
U1_gga(
x1,
x2,
x3,
x4) =
U1_gga(
x1,
x2,
x4)
s(
x1) =
s(
x1)
U3_gga(
x1,
x2,
x3,
x4,
x5) =
U3_gga(
x1,
x2,
x3,
x5)
U2_gga(
x1,
x2,
x3,
x4) =
U2_gga(
x1,
x2,
x4)
times_in_gga(
x1,
x2,
x3) =
times_in_gga(
x1,
x2)
times_out_gga(
x1,
x2,
x3) =
times_out_gga(
x1,
x2,
x3)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x1,
x2,
x4)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x1,
x2,
x4)
plus_in_gga(
x1,
x2,
x3) =
plus_in_gga(
x1,
x2)
plus_out_gga(
x1,
x2,
x3) =
plus_out_gga(
x1,
x2,
x3)
U4_gga(
x1,
x2,
x3,
x4) =
U4_gga(
x1,
x2,
x4)
CONVERT_IN_GGA(
x1,
x2,
x3) =
CONVERT_IN_GGA(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(49) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(50) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
CONVERT_IN_GGA(.(s(Y), XS), B, s(X)) → CONVERT_IN_GGA(.(Y, XS), B, X)
CONVERT_IN_GGA(.(0, XS), B, X) → CONVERT_IN_GGA(XS, B, Y)
R is empty.
The argument filtering Pi contains the following mapping:
.(
x1,
x2) =
.(
x1,
x2)
0 =
0
s(
x1) =
s(
x1)
CONVERT_IN_GGA(
x1,
x2,
x3) =
CONVERT_IN_GGA(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(51) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(52) Obligation:
Q DP problem:
The TRS P consists of the following rules:
CONVERT_IN_GGA(.(s(Y), XS), B) → CONVERT_IN_GGA(.(Y, XS), B)
CONVERT_IN_GGA(.(0, XS), B) → CONVERT_IN_GGA(XS, B)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(53) UsableRulesReductionPairsProof (EQUIVALENT transformation)
By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.
The following dependency pairs can be deleted:
CONVERT_IN_GGA(.(s(Y), XS), B) → CONVERT_IN_GGA(.(Y, XS), B)
CONVERT_IN_GGA(.(0, XS), B) → CONVERT_IN_GGA(XS, B)
No rules are removed from R.
Used ordering: POLO with Polynomial interpretation [POLO]:
POL(.(x1, x2)) = 2·x1 + 2·x2
POL(0) = 0
POL(CONVERT_IN_GGA(x1, x2)) = 2·x1 + x2
POL(s(x1)) = 2·x1
(54) Obligation:
Q DP problem:
P is empty.
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(55) PisEmptyProof (EQUIVALENT transformation)
The TRS P is empty. Hence, there is no (P,Q,R) chain.
(56) TRUE