(0) Obligation:
Clauses:
div(X1, 0, X2, X3) :- ','(!, failure(a)).
div(0, X4, Z, R) :- ','(!, ','(eq(Z, 0), eq(R, 0))).
div(X, Y, s(Z), R) :- ','(minus(X, Y, U), ','(!, div(U, Y, Z, R))).
div(X, X5, X6, X).
minus(X, 0, X).
minus(s(X), s(Y), Z) :- minus(X, Y, Z).
failure(b).
eq(X, X).
Queries:
div(g,g,a,a).
(1) CutEliminatorProof (SOUND transformation)
Eliminated all cuts by simply ignoring them[PROLOG].
(2) Obligation:
Clauses:
div(X1, 0, X2, X3) :- failure(a).
div(0, X4, Z, R) :- ','(eq(Z, 0), eq(R, 0)).
div(X, Y, s(Z), R) :- ','(minus(X, Y, U), div(U, Y, Z, R)).
div(X, X5, X6, X).
minus(X, 0, X).
minus(s(X), s(Y), Z) :- minus(X, Y, Z).
failure(b).
eq(X, X).
Queries:
div(g,g,a,a).
(3) PrologToPiTRSProof (SOUND transformation)
We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
div_in: (b,b,f,f)
minus_in: (b,b,f)
Transforming
Prolog into the following
Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
div_in_ggaa(X1, 0, X2, X3) → U1_ggaa(X1, X2, X3, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U1_ggaa(X1, X2, X3, failure_out_g(a)) → div_out_ggaa(X1, 0, X2, X3)
div_in_ggaa(0, X4, Z, R) → U2_ggaa(X4, Z, R, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U2_ggaa(X4, Z, R, eq_out_ag(Z, 0)) → U3_ggaa(X4, Z, R, eq_in_ag(R, 0))
U3_ggaa(X4, Z, R, eq_out_ag(R, 0)) → div_out_ggaa(0, X4, Z, R)
div_in_ggaa(X, Y, s(Z), R) → U4_ggaa(X, Y, Z, R, minus_in_gga(X, Y, U))
minus_in_gga(X, 0, X) → minus_out_gga(X, 0, X)
minus_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, minus_in_gga(X, Y, Z))
U6_gga(X, Y, Z, minus_out_gga(X, Y, Z)) → minus_out_gga(s(X), s(Y), Z)
U4_ggaa(X, Y, Z, R, minus_out_gga(X, Y, U)) → U5_ggaa(X, Y, Z, R, div_in_ggaa(U, Y, Z, R))
div_in_ggaa(X, X5, X6, X) → div_out_ggaa(X, X5, X6, X)
U5_ggaa(X, Y, Z, R, div_out_ggaa(U, Y, Z, R)) → div_out_ggaa(X, Y, s(Z), R)
The argument filtering Pi contains the following mapping:
div_in_ggaa(
x1,
x2,
x3,
x4) =
div_in_ggaa(
x1,
x2)
0 =
0
U1_ggaa(
x1,
x2,
x3,
x4) =
U1_ggaa(
x4)
failure_in_g(
x1) =
failure_in_g(
x1)
b =
b
failure_out_g(
x1) =
failure_out_g
a =
a
div_out_ggaa(
x1,
x2,
x3,
x4) =
div_out_ggaa
U2_ggaa(
x1,
x2,
x3,
x4) =
U2_ggaa(
x4)
eq_in_ag(
x1,
x2) =
eq_in_ag(
x2)
eq_out_ag(
x1,
x2) =
eq_out_ag(
x1)
U3_ggaa(
x1,
x2,
x3,
x4) =
U3_ggaa(
x4)
U4_ggaa(
x1,
x2,
x3,
x4,
x5) =
U4_ggaa(
x2,
x5)
minus_in_gga(
x1,
x2,
x3) =
minus_in_gga(
x1,
x2)
minus_out_gga(
x1,
x2,
x3) =
minus_out_gga(
x3)
s(
x1) =
s(
x1)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x4)
U5_ggaa(
x1,
x2,
x3,
x4,
x5) =
U5_ggaa(
x5)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
(4) Obligation:
Pi-finite rewrite system:
The TRS R consists of the following rules:
div_in_ggaa(X1, 0, X2, X3) → U1_ggaa(X1, X2, X3, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U1_ggaa(X1, X2, X3, failure_out_g(a)) → div_out_ggaa(X1, 0, X2, X3)
div_in_ggaa(0, X4, Z, R) → U2_ggaa(X4, Z, R, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U2_ggaa(X4, Z, R, eq_out_ag(Z, 0)) → U3_ggaa(X4, Z, R, eq_in_ag(R, 0))
U3_ggaa(X4, Z, R, eq_out_ag(R, 0)) → div_out_ggaa(0, X4, Z, R)
div_in_ggaa(X, Y, s(Z), R) → U4_ggaa(X, Y, Z, R, minus_in_gga(X, Y, U))
minus_in_gga(X, 0, X) → minus_out_gga(X, 0, X)
minus_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, minus_in_gga(X, Y, Z))
U6_gga(X, Y, Z, minus_out_gga(X, Y, Z)) → minus_out_gga(s(X), s(Y), Z)
U4_ggaa(X, Y, Z, R, minus_out_gga(X, Y, U)) → U5_ggaa(X, Y, Z, R, div_in_ggaa(U, Y, Z, R))
div_in_ggaa(X, X5, X6, X) → div_out_ggaa(X, X5, X6, X)
U5_ggaa(X, Y, Z, R, div_out_ggaa(U, Y, Z, R)) → div_out_ggaa(X, Y, s(Z), R)
The argument filtering Pi contains the following mapping:
div_in_ggaa(
x1,
x2,
x3,
x4) =
div_in_ggaa(
x1,
x2)
0 =
0
U1_ggaa(
x1,
x2,
x3,
x4) =
U1_ggaa(
x4)
failure_in_g(
x1) =
failure_in_g(
x1)
b =
b
failure_out_g(
x1) =
failure_out_g
a =
a
div_out_ggaa(
x1,
x2,
x3,
x4) =
div_out_ggaa
U2_ggaa(
x1,
x2,
x3,
x4) =
U2_ggaa(
x4)
eq_in_ag(
x1,
x2) =
eq_in_ag(
x2)
eq_out_ag(
x1,
x2) =
eq_out_ag(
x1)
U3_ggaa(
x1,
x2,
x3,
x4) =
U3_ggaa(
x4)
U4_ggaa(
x1,
x2,
x3,
x4,
x5) =
U4_ggaa(
x2,
x5)
minus_in_gga(
x1,
x2,
x3) =
minus_in_gga(
x1,
x2)
minus_out_gga(
x1,
x2,
x3) =
minus_out_gga(
x3)
s(
x1) =
s(
x1)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x4)
U5_ggaa(
x1,
x2,
x3,
x4,
x5) =
U5_ggaa(
x5)
(5) 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:
DIV_IN_GGAA(X1, 0, X2, X3) → U1_GGAA(X1, X2, X3, failure_in_g(a))
DIV_IN_GGAA(X1, 0, X2, X3) → FAILURE_IN_G(a)
DIV_IN_GGAA(0, X4, Z, R) → U2_GGAA(X4, Z, R, eq_in_ag(Z, 0))
DIV_IN_GGAA(0, X4, Z, R) → EQ_IN_AG(Z, 0)
U2_GGAA(X4, Z, R, eq_out_ag(Z, 0)) → U3_GGAA(X4, Z, R, eq_in_ag(R, 0))
U2_GGAA(X4, Z, R, eq_out_ag(Z, 0)) → EQ_IN_AG(R, 0)
DIV_IN_GGAA(X, Y, s(Z), R) → U4_GGAA(X, Y, Z, R, minus_in_gga(X, Y, U))
DIV_IN_GGAA(X, Y, s(Z), R) → MINUS_IN_GGA(X, Y, U)
MINUS_IN_GGA(s(X), s(Y), Z) → U6_GGA(X, Y, Z, minus_in_gga(X, Y, Z))
MINUS_IN_GGA(s(X), s(Y), Z) → MINUS_IN_GGA(X, Y, Z)
U4_GGAA(X, Y, Z, R, minus_out_gga(X, Y, U)) → U5_GGAA(X, Y, Z, R, div_in_ggaa(U, Y, Z, R))
U4_GGAA(X, Y, Z, R, minus_out_gga(X, Y, U)) → DIV_IN_GGAA(U, Y, Z, R)
The TRS R consists of the following rules:
div_in_ggaa(X1, 0, X2, X3) → U1_ggaa(X1, X2, X3, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U1_ggaa(X1, X2, X3, failure_out_g(a)) → div_out_ggaa(X1, 0, X2, X3)
div_in_ggaa(0, X4, Z, R) → U2_ggaa(X4, Z, R, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U2_ggaa(X4, Z, R, eq_out_ag(Z, 0)) → U3_ggaa(X4, Z, R, eq_in_ag(R, 0))
U3_ggaa(X4, Z, R, eq_out_ag(R, 0)) → div_out_ggaa(0, X4, Z, R)
div_in_ggaa(X, Y, s(Z), R) → U4_ggaa(X, Y, Z, R, minus_in_gga(X, Y, U))
minus_in_gga(X, 0, X) → minus_out_gga(X, 0, X)
minus_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, minus_in_gga(X, Y, Z))
U6_gga(X, Y, Z, minus_out_gga(X, Y, Z)) → minus_out_gga(s(X), s(Y), Z)
U4_ggaa(X, Y, Z, R, minus_out_gga(X, Y, U)) → U5_ggaa(X, Y, Z, R, div_in_ggaa(U, Y, Z, R))
div_in_ggaa(X, X5, X6, X) → div_out_ggaa(X, X5, X6, X)
U5_ggaa(X, Y, Z, R, div_out_ggaa(U, Y, Z, R)) → div_out_ggaa(X, Y, s(Z), R)
The argument filtering Pi contains the following mapping:
div_in_ggaa(
x1,
x2,
x3,
x4) =
div_in_ggaa(
x1,
x2)
0 =
0
U1_ggaa(
x1,
x2,
x3,
x4) =
U1_ggaa(
x4)
failure_in_g(
x1) =
failure_in_g(
x1)
b =
b
failure_out_g(
x1) =
failure_out_g
a =
a
div_out_ggaa(
x1,
x2,
x3,
x4) =
div_out_ggaa
U2_ggaa(
x1,
x2,
x3,
x4) =
U2_ggaa(
x4)
eq_in_ag(
x1,
x2) =
eq_in_ag(
x2)
eq_out_ag(
x1,
x2) =
eq_out_ag(
x1)
U3_ggaa(
x1,
x2,
x3,
x4) =
U3_ggaa(
x4)
U4_ggaa(
x1,
x2,
x3,
x4,
x5) =
U4_ggaa(
x2,
x5)
minus_in_gga(
x1,
x2,
x3) =
minus_in_gga(
x1,
x2)
minus_out_gga(
x1,
x2,
x3) =
minus_out_gga(
x3)
s(
x1) =
s(
x1)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x4)
U5_ggaa(
x1,
x2,
x3,
x4,
x5) =
U5_ggaa(
x5)
DIV_IN_GGAA(
x1,
x2,
x3,
x4) =
DIV_IN_GGAA(
x1,
x2)
U1_GGAA(
x1,
x2,
x3,
x4) =
U1_GGAA(
x4)
FAILURE_IN_G(
x1) =
FAILURE_IN_G(
x1)
U2_GGAA(
x1,
x2,
x3,
x4) =
U2_GGAA(
x4)
EQ_IN_AG(
x1,
x2) =
EQ_IN_AG(
x2)
U3_GGAA(
x1,
x2,
x3,
x4) =
U3_GGAA(
x4)
U4_GGAA(
x1,
x2,
x3,
x4,
x5) =
U4_GGAA(
x2,
x5)
MINUS_IN_GGA(
x1,
x2,
x3) =
MINUS_IN_GGA(
x1,
x2)
U6_GGA(
x1,
x2,
x3,
x4) =
U6_GGA(
x4)
U5_GGAA(
x1,
x2,
x3,
x4,
x5) =
U5_GGAA(
x5)
We have to consider all (P,R,Pi)-chains
(6) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
DIV_IN_GGAA(X1, 0, X2, X3) → U1_GGAA(X1, X2, X3, failure_in_g(a))
DIV_IN_GGAA(X1, 0, X2, X3) → FAILURE_IN_G(a)
DIV_IN_GGAA(0, X4, Z, R) → U2_GGAA(X4, Z, R, eq_in_ag(Z, 0))
DIV_IN_GGAA(0, X4, Z, R) → EQ_IN_AG(Z, 0)
U2_GGAA(X4, Z, R, eq_out_ag(Z, 0)) → U3_GGAA(X4, Z, R, eq_in_ag(R, 0))
U2_GGAA(X4, Z, R, eq_out_ag(Z, 0)) → EQ_IN_AG(R, 0)
DIV_IN_GGAA(X, Y, s(Z), R) → U4_GGAA(X, Y, Z, R, minus_in_gga(X, Y, U))
DIV_IN_GGAA(X, Y, s(Z), R) → MINUS_IN_GGA(X, Y, U)
MINUS_IN_GGA(s(X), s(Y), Z) → U6_GGA(X, Y, Z, minus_in_gga(X, Y, Z))
MINUS_IN_GGA(s(X), s(Y), Z) → MINUS_IN_GGA(X, Y, Z)
U4_GGAA(X, Y, Z, R, minus_out_gga(X, Y, U)) → U5_GGAA(X, Y, Z, R, div_in_ggaa(U, Y, Z, R))
U4_GGAA(X, Y, Z, R, minus_out_gga(X, Y, U)) → DIV_IN_GGAA(U, Y, Z, R)
The TRS R consists of the following rules:
div_in_ggaa(X1, 0, X2, X3) → U1_ggaa(X1, X2, X3, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U1_ggaa(X1, X2, X3, failure_out_g(a)) → div_out_ggaa(X1, 0, X2, X3)
div_in_ggaa(0, X4, Z, R) → U2_ggaa(X4, Z, R, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U2_ggaa(X4, Z, R, eq_out_ag(Z, 0)) → U3_ggaa(X4, Z, R, eq_in_ag(R, 0))
U3_ggaa(X4, Z, R, eq_out_ag(R, 0)) → div_out_ggaa(0, X4, Z, R)
div_in_ggaa(X, Y, s(Z), R) → U4_ggaa(X, Y, Z, R, minus_in_gga(X, Y, U))
minus_in_gga(X, 0, X) → minus_out_gga(X, 0, X)
minus_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, minus_in_gga(X, Y, Z))
U6_gga(X, Y, Z, minus_out_gga(X, Y, Z)) → minus_out_gga(s(X), s(Y), Z)
U4_ggaa(X, Y, Z, R, minus_out_gga(X, Y, U)) → U5_ggaa(X, Y, Z, R, div_in_ggaa(U, Y, Z, R))
div_in_ggaa(X, X5, X6, X) → div_out_ggaa(X, X5, X6, X)
U5_ggaa(X, Y, Z, R, div_out_ggaa(U, Y, Z, R)) → div_out_ggaa(X, Y, s(Z), R)
The argument filtering Pi contains the following mapping:
div_in_ggaa(
x1,
x2,
x3,
x4) =
div_in_ggaa(
x1,
x2)
0 =
0
U1_ggaa(
x1,
x2,
x3,
x4) =
U1_ggaa(
x4)
failure_in_g(
x1) =
failure_in_g(
x1)
b =
b
failure_out_g(
x1) =
failure_out_g
a =
a
div_out_ggaa(
x1,
x2,
x3,
x4) =
div_out_ggaa
U2_ggaa(
x1,
x2,
x3,
x4) =
U2_ggaa(
x4)
eq_in_ag(
x1,
x2) =
eq_in_ag(
x2)
eq_out_ag(
x1,
x2) =
eq_out_ag(
x1)
U3_ggaa(
x1,
x2,
x3,
x4) =
U3_ggaa(
x4)
U4_ggaa(
x1,
x2,
x3,
x4,
x5) =
U4_ggaa(
x2,
x5)
minus_in_gga(
x1,
x2,
x3) =
minus_in_gga(
x1,
x2)
minus_out_gga(
x1,
x2,
x3) =
minus_out_gga(
x3)
s(
x1) =
s(
x1)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x4)
U5_ggaa(
x1,
x2,
x3,
x4,
x5) =
U5_ggaa(
x5)
DIV_IN_GGAA(
x1,
x2,
x3,
x4) =
DIV_IN_GGAA(
x1,
x2)
U1_GGAA(
x1,
x2,
x3,
x4) =
U1_GGAA(
x4)
FAILURE_IN_G(
x1) =
FAILURE_IN_G(
x1)
U2_GGAA(
x1,
x2,
x3,
x4) =
U2_GGAA(
x4)
EQ_IN_AG(
x1,
x2) =
EQ_IN_AG(
x2)
U3_GGAA(
x1,
x2,
x3,
x4) =
U3_GGAA(
x4)
U4_GGAA(
x1,
x2,
x3,
x4,
x5) =
U4_GGAA(
x2,
x5)
MINUS_IN_GGA(
x1,
x2,
x3) =
MINUS_IN_GGA(
x1,
x2)
U6_GGA(
x1,
x2,
x3,
x4) =
U6_GGA(
x4)
U5_GGAA(
x1,
x2,
x3,
x4,
x5) =
U5_GGAA(
x5)
We have to consider all (P,R,Pi)-chains
(7) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 9 less nodes.
(8) Complex Obligation (AND)
(9) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
MINUS_IN_GGA(s(X), s(Y), Z) → MINUS_IN_GGA(X, Y, Z)
The TRS R consists of the following rules:
div_in_ggaa(X1, 0, X2, X3) → U1_ggaa(X1, X2, X3, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U1_ggaa(X1, X2, X3, failure_out_g(a)) → div_out_ggaa(X1, 0, X2, X3)
div_in_ggaa(0, X4, Z, R) → U2_ggaa(X4, Z, R, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U2_ggaa(X4, Z, R, eq_out_ag(Z, 0)) → U3_ggaa(X4, Z, R, eq_in_ag(R, 0))
U3_ggaa(X4, Z, R, eq_out_ag(R, 0)) → div_out_ggaa(0, X4, Z, R)
div_in_ggaa(X, Y, s(Z), R) → U4_ggaa(X, Y, Z, R, minus_in_gga(X, Y, U))
minus_in_gga(X, 0, X) → minus_out_gga(X, 0, X)
minus_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, minus_in_gga(X, Y, Z))
U6_gga(X, Y, Z, minus_out_gga(X, Y, Z)) → minus_out_gga(s(X), s(Y), Z)
U4_ggaa(X, Y, Z, R, minus_out_gga(X, Y, U)) → U5_ggaa(X, Y, Z, R, div_in_ggaa(U, Y, Z, R))
div_in_ggaa(X, X5, X6, X) → div_out_ggaa(X, X5, X6, X)
U5_ggaa(X, Y, Z, R, div_out_ggaa(U, Y, Z, R)) → div_out_ggaa(X, Y, s(Z), R)
The argument filtering Pi contains the following mapping:
div_in_ggaa(
x1,
x2,
x3,
x4) =
div_in_ggaa(
x1,
x2)
0 =
0
U1_ggaa(
x1,
x2,
x3,
x4) =
U1_ggaa(
x4)
failure_in_g(
x1) =
failure_in_g(
x1)
b =
b
failure_out_g(
x1) =
failure_out_g
a =
a
div_out_ggaa(
x1,
x2,
x3,
x4) =
div_out_ggaa
U2_ggaa(
x1,
x2,
x3,
x4) =
U2_ggaa(
x4)
eq_in_ag(
x1,
x2) =
eq_in_ag(
x2)
eq_out_ag(
x1,
x2) =
eq_out_ag(
x1)
U3_ggaa(
x1,
x2,
x3,
x4) =
U3_ggaa(
x4)
U4_ggaa(
x1,
x2,
x3,
x4,
x5) =
U4_ggaa(
x2,
x5)
minus_in_gga(
x1,
x2,
x3) =
minus_in_gga(
x1,
x2)
minus_out_gga(
x1,
x2,
x3) =
minus_out_gga(
x3)
s(
x1) =
s(
x1)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x4)
U5_ggaa(
x1,
x2,
x3,
x4,
x5) =
U5_ggaa(
x5)
MINUS_IN_GGA(
x1,
x2,
x3) =
MINUS_IN_GGA(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(10) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(11) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
MINUS_IN_GGA(s(X), s(Y), Z) → MINUS_IN_GGA(X, Y, Z)
R is empty.
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
MINUS_IN_GGA(
x1,
x2,
x3) =
MINUS_IN_GGA(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(12) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(13) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MINUS_IN_GGA(s(X), s(Y)) → MINUS_IN_GGA(X, Y)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(14) 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:
- MINUS_IN_GGA(s(X), s(Y)) → MINUS_IN_GGA(X, Y)
The graph contains the following edges 1 > 1, 2 > 2
(15) TRUE
(16) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
DIV_IN_GGAA(X, Y, s(Z), R) → U4_GGAA(X, Y, Z, R, minus_in_gga(X, Y, U))
U4_GGAA(X, Y, Z, R, minus_out_gga(X, Y, U)) → DIV_IN_GGAA(U, Y, Z, R)
The TRS R consists of the following rules:
div_in_ggaa(X1, 0, X2, X3) → U1_ggaa(X1, X2, X3, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U1_ggaa(X1, X2, X3, failure_out_g(a)) → div_out_ggaa(X1, 0, X2, X3)
div_in_ggaa(0, X4, Z, R) → U2_ggaa(X4, Z, R, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U2_ggaa(X4, Z, R, eq_out_ag(Z, 0)) → U3_ggaa(X4, Z, R, eq_in_ag(R, 0))
U3_ggaa(X4, Z, R, eq_out_ag(R, 0)) → div_out_ggaa(0, X4, Z, R)
div_in_ggaa(X, Y, s(Z), R) → U4_ggaa(X, Y, Z, R, minus_in_gga(X, Y, U))
minus_in_gga(X, 0, X) → minus_out_gga(X, 0, X)
minus_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, minus_in_gga(X, Y, Z))
U6_gga(X, Y, Z, minus_out_gga(X, Y, Z)) → minus_out_gga(s(X), s(Y), Z)
U4_ggaa(X, Y, Z, R, minus_out_gga(X, Y, U)) → U5_ggaa(X, Y, Z, R, div_in_ggaa(U, Y, Z, R))
div_in_ggaa(X, X5, X6, X) → div_out_ggaa(X, X5, X6, X)
U5_ggaa(X, Y, Z, R, div_out_ggaa(U, Y, Z, R)) → div_out_ggaa(X, Y, s(Z), R)
The argument filtering Pi contains the following mapping:
div_in_ggaa(
x1,
x2,
x3,
x4) =
div_in_ggaa(
x1,
x2)
0 =
0
U1_ggaa(
x1,
x2,
x3,
x4) =
U1_ggaa(
x4)
failure_in_g(
x1) =
failure_in_g(
x1)
b =
b
failure_out_g(
x1) =
failure_out_g
a =
a
div_out_ggaa(
x1,
x2,
x3,
x4) =
div_out_ggaa
U2_ggaa(
x1,
x2,
x3,
x4) =
U2_ggaa(
x4)
eq_in_ag(
x1,
x2) =
eq_in_ag(
x2)
eq_out_ag(
x1,
x2) =
eq_out_ag(
x1)
U3_ggaa(
x1,
x2,
x3,
x4) =
U3_ggaa(
x4)
U4_ggaa(
x1,
x2,
x3,
x4,
x5) =
U4_ggaa(
x2,
x5)
minus_in_gga(
x1,
x2,
x3) =
minus_in_gga(
x1,
x2)
minus_out_gga(
x1,
x2,
x3) =
minus_out_gga(
x3)
s(
x1) =
s(
x1)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x4)
U5_ggaa(
x1,
x2,
x3,
x4,
x5) =
U5_ggaa(
x5)
DIV_IN_GGAA(
x1,
x2,
x3,
x4) =
DIV_IN_GGAA(
x1,
x2)
U4_GGAA(
x1,
x2,
x3,
x4,
x5) =
U4_GGAA(
x2,
x5)
We have to consider all (P,R,Pi)-chains
(17) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(18) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
DIV_IN_GGAA(X, Y, s(Z), R) → U4_GGAA(X, Y, Z, R, minus_in_gga(X, Y, U))
U4_GGAA(X, Y, Z, R, minus_out_gga(X, Y, U)) → DIV_IN_GGAA(U, Y, Z, R)
The TRS R consists of the following rules:
minus_in_gga(X, 0, X) → minus_out_gga(X, 0, X)
minus_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, minus_in_gga(X, Y, Z))
U6_gga(X, Y, Z, minus_out_gga(X, Y, Z)) → minus_out_gga(s(X), s(Y), Z)
The argument filtering Pi contains the following mapping:
0 =
0
minus_in_gga(
x1,
x2,
x3) =
minus_in_gga(
x1,
x2)
minus_out_gga(
x1,
x2,
x3) =
minus_out_gga(
x3)
s(
x1) =
s(
x1)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x4)
DIV_IN_GGAA(
x1,
x2,
x3,
x4) =
DIV_IN_GGAA(
x1,
x2)
U4_GGAA(
x1,
x2,
x3,
x4,
x5) =
U4_GGAA(
x2,
x5)
We have to consider all (P,R,Pi)-chains
(19) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(20) Obligation:
Q DP problem:
The TRS P consists of the following rules:
DIV_IN_GGAA(X, Y) → U4_GGAA(Y, minus_in_gga(X, Y))
U4_GGAA(Y, minus_out_gga(U)) → DIV_IN_GGAA(U, Y)
The TRS R consists of the following rules:
minus_in_gga(X, 0) → minus_out_gga(X)
minus_in_gga(s(X), s(Y)) → U6_gga(minus_in_gga(X, Y))
U6_gga(minus_out_gga(Z)) → minus_out_gga(Z)
The set Q consists of the following terms:
minus_in_gga(x0, x1)
U6_gga(x0)
We have to consider all (P,Q,R)-chains.
(21) Narrowing (SOUND transformation)
By narrowing [LPAR04] the rule
DIV_IN_GGAA(
X,
Y) →
U4_GGAA(
Y,
minus_in_gga(
X,
Y)) at position [1] we obtained the following new rules [LPAR04]:
DIV_IN_GGAA(x0, 0) → U4_GGAA(0, minus_out_gga(x0))
DIV_IN_GGAA(s(x0), s(x1)) → U4_GGAA(s(x1), U6_gga(minus_in_gga(x0, x1)))
(22) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_GGAA(Y, minus_out_gga(U)) → DIV_IN_GGAA(U, Y)
DIV_IN_GGAA(x0, 0) → U4_GGAA(0, minus_out_gga(x0))
DIV_IN_GGAA(s(x0), s(x1)) → U4_GGAA(s(x1), U6_gga(minus_in_gga(x0, x1)))
The TRS R consists of the following rules:
minus_in_gga(X, 0) → minus_out_gga(X)
minus_in_gga(s(X), s(Y)) → U6_gga(minus_in_gga(X, Y))
U6_gga(minus_out_gga(Z)) → minus_out_gga(Z)
The set Q consists of the following terms:
minus_in_gga(x0, x1)
U6_gga(x0)
We have to consider all (P,Q,R)-chains.
(23) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
U4_GGAA(
Y,
minus_out_gga(
U)) →
DIV_IN_GGAA(
U,
Y) we obtained the following new rules [LPAR04]:
U4_GGAA(0, minus_out_gga(z0)) → DIV_IN_GGAA(z0, 0)
U4_GGAA(s(z1), minus_out_gga(x1)) → DIV_IN_GGAA(x1, s(z1))
(24) Obligation:
Q DP problem:
The TRS P consists of the following rules:
DIV_IN_GGAA(x0, 0) → U4_GGAA(0, minus_out_gga(x0))
DIV_IN_GGAA(s(x0), s(x1)) → U4_GGAA(s(x1), U6_gga(minus_in_gga(x0, x1)))
U4_GGAA(0, minus_out_gga(z0)) → DIV_IN_GGAA(z0, 0)
U4_GGAA(s(z1), minus_out_gga(x1)) → DIV_IN_GGAA(x1, s(z1))
The TRS R consists of the following rules:
minus_in_gga(X, 0) → minus_out_gga(X)
minus_in_gga(s(X), s(Y)) → U6_gga(minus_in_gga(X, Y))
U6_gga(minus_out_gga(Z)) → minus_out_gga(Z)
The set Q consists of the following terms:
minus_in_gga(x0, x1)
U6_gga(x0)
We have to consider all (P,Q,R)-chains.
(25) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs.
(26) Complex Obligation (AND)
(27) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_GGAA(s(z1), minus_out_gga(x1)) → DIV_IN_GGAA(x1, s(z1))
DIV_IN_GGAA(s(x0), s(x1)) → U4_GGAA(s(x1), U6_gga(minus_in_gga(x0, x1)))
The TRS R consists of the following rules:
minus_in_gga(X, 0) → minus_out_gga(X)
minus_in_gga(s(X), s(Y)) → U6_gga(minus_in_gga(X, Y))
U6_gga(minus_out_gga(Z)) → minus_out_gga(Z)
The set Q consists of the following terms:
minus_in_gga(x0, x1)
U6_gga(x0)
We have to consider all (P,Q,R)-chains.
(28) ForwardInstantiation (EQUIVALENT transformation)
By forward instantiating [JAR06] the rule
U4_GGAA(
s(
z1),
minus_out_gga(
x1)) →
DIV_IN_GGAA(
x1,
s(
z1)) we obtained the following new rules [LPAR04]:
U4_GGAA(s(x0), minus_out_gga(s(y_0))) → DIV_IN_GGAA(s(y_0), s(x0))
(29) Obligation:
Q DP problem:
The TRS P consists of the following rules:
DIV_IN_GGAA(s(x0), s(x1)) → U4_GGAA(s(x1), U6_gga(minus_in_gga(x0, x1)))
U4_GGAA(s(x0), minus_out_gga(s(y_0))) → DIV_IN_GGAA(s(y_0), s(x0))
The TRS R consists of the following rules:
minus_in_gga(X, 0) → minus_out_gga(X)
minus_in_gga(s(X), s(Y)) → U6_gga(minus_in_gga(X, Y))
U6_gga(minus_out_gga(Z)) → minus_out_gga(Z)
The set Q consists of the following terms:
minus_in_gga(x0, x1)
U6_gga(x0)
We have to consider all (P,Q,R)-chains.
(30) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
DIV_IN_GGAA(s(x0), s(x1)) → U4_GGAA(s(x1), U6_gga(minus_in_gga(x0, x1)))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:
POL(0) = 0
POL(DIV_IN_GGAA(x1, x2)) = 1 + x1 + x2
POL(U4_GGAA(x1, x2)) = x1 + x2
POL(U6_gga(x1)) = x1
POL(minus_in_gga(x1, x2)) = 1 + x1
POL(minus_out_gga(x1)) = 1 + x1
POL(s(x1)) = 1 + x1
The following usable rules [FROCOS05] were oriented:
minus_in_gga(X, 0) → minus_out_gga(X)
minus_in_gga(s(X), s(Y)) → U6_gga(minus_in_gga(X, Y))
U6_gga(minus_out_gga(Z)) → minus_out_gga(Z)
(31) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_GGAA(s(x0), minus_out_gga(s(y_0))) → DIV_IN_GGAA(s(y_0), s(x0))
The TRS R consists of the following rules:
minus_in_gga(X, 0) → minus_out_gga(X)
minus_in_gga(s(X), s(Y)) → U6_gga(minus_in_gga(X, Y))
U6_gga(minus_out_gga(Z)) → minus_out_gga(Z)
The set Q consists of the following terms:
minus_in_gga(x0, x1)
U6_gga(x0)
We have to consider all (P,Q,R)-chains.
(32) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.
(33) TRUE
(34) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_GGAA(0, minus_out_gga(z0)) → DIV_IN_GGAA(z0, 0)
DIV_IN_GGAA(x0, 0) → U4_GGAA(0, minus_out_gga(x0))
The TRS R consists of the following rules:
minus_in_gga(X, 0) → minus_out_gga(X)
minus_in_gga(s(X), s(Y)) → U6_gga(minus_in_gga(X, Y))
U6_gga(minus_out_gga(Z)) → minus_out_gga(Z)
The set Q consists of the following terms:
minus_in_gga(x0, x1)
U6_gga(x0)
We have to consider all (P,Q,R)-chains.
(35) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(36) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_GGAA(0, minus_out_gga(z0)) → DIV_IN_GGAA(z0, 0)
DIV_IN_GGAA(x0, 0) → U4_GGAA(0, minus_out_gga(x0))
R is empty.
The set Q consists of the following terms:
minus_in_gga(x0, x1)
U6_gga(x0)
We have to consider all (P,Q,R)-chains.
(37) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
minus_in_gga(x0, x1)
U6_gga(x0)
(38) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_GGAA(0, minus_out_gga(z0)) → DIV_IN_GGAA(z0, 0)
DIV_IN_GGAA(x0, 0) → U4_GGAA(0, minus_out_gga(x0))
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(39) NonTerminationProof (EQUIVALENT transformation)
We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:
s =
DIV_IN_GGAA(
x0,
0) evaluates to t =
DIV_IN_GGAA(
x0,
0)
Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
- Semiunifier: [ ]
- Matcher: [ ]
Rewriting sequenceDIV_IN_GGAA(x0, 0) →
U4_GGAA(
0,
minus_out_gga(
x0))
with rule
DIV_IN_GGAA(
x0',
0) →
U4_GGAA(
0,
minus_out_gga(
x0')) at position [] and matcher [
x0' /
x0]
U4_GGAA(0, minus_out_gga(x0)) →
DIV_IN_GGAA(
x0,
0)
with rule
U4_GGAA(
0,
minus_out_gga(
z0)) →
DIV_IN_GGAA(
z0,
0)
Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence
All these steps are and every following step will be a correct step w.r.t to Q.
(40) FALSE
(41) PrologToPiTRSProof (SOUND transformation)
We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
div_in: (b,b,f,f)
minus_in: (b,b,f)
Transforming
Prolog into the following
Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
div_in_ggaa(X1, 0, X2, X3) → U1_ggaa(X1, X2, X3, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U1_ggaa(X1, X2, X3, failure_out_g(a)) → div_out_ggaa(X1, 0, X2, X3)
div_in_ggaa(0, X4, Z, R) → U2_ggaa(X4, Z, R, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U2_ggaa(X4, Z, R, eq_out_ag(Z, 0)) → U3_ggaa(X4, Z, R, eq_in_ag(R, 0))
U3_ggaa(X4, Z, R, eq_out_ag(R, 0)) → div_out_ggaa(0, X4, Z, R)
div_in_ggaa(X, Y, s(Z), R) → U4_ggaa(X, Y, Z, R, minus_in_gga(X, Y, U))
minus_in_gga(X, 0, X) → minus_out_gga(X, 0, X)
minus_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, minus_in_gga(X, Y, Z))
U6_gga(X, Y, Z, minus_out_gga(X, Y, Z)) → minus_out_gga(s(X), s(Y), Z)
U4_ggaa(X, Y, Z, R, minus_out_gga(X, Y, U)) → U5_ggaa(X, Y, Z, R, div_in_ggaa(U, Y, Z, R))
div_in_ggaa(X, X5, X6, X) → div_out_ggaa(X, X5, X6, X)
U5_ggaa(X, Y, Z, R, div_out_ggaa(U, Y, Z, R)) → div_out_ggaa(X, Y, s(Z), R)
The argument filtering Pi contains the following mapping:
div_in_ggaa(
x1,
x2,
x3,
x4) =
div_in_ggaa(
x1,
x2)
0 =
0
U1_ggaa(
x1,
x2,
x3,
x4) =
U1_ggaa(
x1,
x4)
failure_in_g(
x1) =
failure_in_g(
x1)
b =
b
failure_out_g(
x1) =
failure_out_g(
x1)
a =
a
div_out_ggaa(
x1,
x2,
x3,
x4) =
div_out_ggaa(
x1,
x2)
U2_ggaa(
x1,
x2,
x3,
x4) =
U2_ggaa(
x1,
x4)
eq_in_ag(
x1,
x2) =
eq_in_ag(
x2)
eq_out_ag(
x1,
x2) =
eq_out_ag(
x1,
x2)
U3_ggaa(
x1,
x2,
x3,
x4) =
U3_ggaa(
x1,
x4)
U4_ggaa(
x1,
x2,
x3,
x4,
x5) =
U4_ggaa(
x1,
x2,
x5)
minus_in_gga(
x1,
x2,
x3) =
minus_in_gga(
x1,
x2)
minus_out_gga(
x1,
x2,
x3) =
minus_out_gga(
x1,
x2,
x3)
s(
x1) =
s(
x1)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x1,
x2,
x4)
U5_ggaa(
x1,
x2,
x3,
x4,
x5) =
U5_ggaa(
x1,
x2,
x5)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
(42) Obligation:
Pi-finite rewrite system:
The TRS R consists of the following rules:
div_in_ggaa(X1, 0, X2, X3) → U1_ggaa(X1, X2, X3, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U1_ggaa(X1, X2, X3, failure_out_g(a)) → div_out_ggaa(X1, 0, X2, X3)
div_in_ggaa(0, X4, Z, R) → U2_ggaa(X4, Z, R, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U2_ggaa(X4, Z, R, eq_out_ag(Z, 0)) → U3_ggaa(X4, Z, R, eq_in_ag(R, 0))
U3_ggaa(X4, Z, R, eq_out_ag(R, 0)) → div_out_ggaa(0, X4, Z, R)
div_in_ggaa(X, Y, s(Z), R) → U4_ggaa(X, Y, Z, R, minus_in_gga(X, Y, U))
minus_in_gga(X, 0, X) → minus_out_gga(X, 0, X)
minus_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, minus_in_gga(X, Y, Z))
U6_gga(X, Y, Z, minus_out_gga(X, Y, Z)) → minus_out_gga(s(X), s(Y), Z)
U4_ggaa(X, Y, Z, R, minus_out_gga(X, Y, U)) → U5_ggaa(X, Y, Z, R, div_in_ggaa(U, Y, Z, R))
div_in_ggaa(X, X5, X6, X) → div_out_ggaa(X, X5, X6, X)
U5_ggaa(X, Y, Z, R, div_out_ggaa(U, Y, Z, R)) → div_out_ggaa(X, Y, s(Z), R)
The argument filtering Pi contains the following mapping:
div_in_ggaa(
x1,
x2,
x3,
x4) =
div_in_ggaa(
x1,
x2)
0 =
0
U1_ggaa(
x1,
x2,
x3,
x4) =
U1_ggaa(
x1,
x4)
failure_in_g(
x1) =
failure_in_g(
x1)
b =
b
failure_out_g(
x1) =
failure_out_g(
x1)
a =
a
div_out_ggaa(
x1,
x2,
x3,
x4) =
div_out_ggaa(
x1,
x2)
U2_ggaa(
x1,
x2,
x3,
x4) =
U2_ggaa(
x1,
x4)
eq_in_ag(
x1,
x2) =
eq_in_ag(
x2)
eq_out_ag(
x1,
x2) =
eq_out_ag(
x1,
x2)
U3_ggaa(
x1,
x2,
x3,
x4) =
U3_ggaa(
x1,
x4)
U4_ggaa(
x1,
x2,
x3,
x4,
x5) =
U4_ggaa(
x1,
x2,
x5)
minus_in_gga(
x1,
x2,
x3) =
minus_in_gga(
x1,
x2)
minus_out_gga(
x1,
x2,
x3) =
minus_out_gga(
x1,
x2,
x3)
s(
x1) =
s(
x1)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x1,
x2,
x4)
U5_ggaa(
x1,
x2,
x3,
x4,
x5) =
U5_ggaa(
x1,
x2,
x5)
(43) 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:
DIV_IN_GGAA(X1, 0, X2, X3) → U1_GGAA(X1, X2, X3, failure_in_g(a))
DIV_IN_GGAA(X1, 0, X2, X3) → FAILURE_IN_G(a)
DIV_IN_GGAA(0, X4, Z, R) → U2_GGAA(X4, Z, R, eq_in_ag(Z, 0))
DIV_IN_GGAA(0, X4, Z, R) → EQ_IN_AG(Z, 0)
U2_GGAA(X4, Z, R, eq_out_ag(Z, 0)) → U3_GGAA(X4, Z, R, eq_in_ag(R, 0))
U2_GGAA(X4, Z, R, eq_out_ag(Z, 0)) → EQ_IN_AG(R, 0)
DIV_IN_GGAA(X, Y, s(Z), R) → U4_GGAA(X, Y, Z, R, minus_in_gga(X, Y, U))
DIV_IN_GGAA(X, Y, s(Z), R) → MINUS_IN_GGA(X, Y, U)
MINUS_IN_GGA(s(X), s(Y), Z) → U6_GGA(X, Y, Z, minus_in_gga(X, Y, Z))
MINUS_IN_GGA(s(X), s(Y), Z) → MINUS_IN_GGA(X, Y, Z)
U4_GGAA(X, Y, Z, R, minus_out_gga(X, Y, U)) → U5_GGAA(X, Y, Z, R, div_in_ggaa(U, Y, Z, R))
U4_GGAA(X, Y, Z, R, minus_out_gga(X, Y, U)) → DIV_IN_GGAA(U, Y, Z, R)
The TRS R consists of the following rules:
div_in_ggaa(X1, 0, X2, X3) → U1_ggaa(X1, X2, X3, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U1_ggaa(X1, X2, X3, failure_out_g(a)) → div_out_ggaa(X1, 0, X2, X3)
div_in_ggaa(0, X4, Z, R) → U2_ggaa(X4, Z, R, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U2_ggaa(X4, Z, R, eq_out_ag(Z, 0)) → U3_ggaa(X4, Z, R, eq_in_ag(R, 0))
U3_ggaa(X4, Z, R, eq_out_ag(R, 0)) → div_out_ggaa(0, X4, Z, R)
div_in_ggaa(X, Y, s(Z), R) → U4_ggaa(X, Y, Z, R, minus_in_gga(X, Y, U))
minus_in_gga(X, 0, X) → minus_out_gga(X, 0, X)
minus_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, minus_in_gga(X, Y, Z))
U6_gga(X, Y, Z, minus_out_gga(X, Y, Z)) → minus_out_gga(s(X), s(Y), Z)
U4_ggaa(X, Y, Z, R, minus_out_gga(X, Y, U)) → U5_ggaa(X, Y, Z, R, div_in_ggaa(U, Y, Z, R))
div_in_ggaa(X, X5, X6, X) → div_out_ggaa(X, X5, X6, X)
U5_ggaa(X, Y, Z, R, div_out_ggaa(U, Y, Z, R)) → div_out_ggaa(X, Y, s(Z), R)
The argument filtering Pi contains the following mapping:
div_in_ggaa(
x1,
x2,
x3,
x4) =
div_in_ggaa(
x1,
x2)
0 =
0
U1_ggaa(
x1,
x2,
x3,
x4) =
U1_ggaa(
x1,
x4)
failure_in_g(
x1) =
failure_in_g(
x1)
b =
b
failure_out_g(
x1) =
failure_out_g(
x1)
a =
a
div_out_ggaa(
x1,
x2,
x3,
x4) =
div_out_ggaa(
x1,
x2)
U2_ggaa(
x1,
x2,
x3,
x4) =
U2_ggaa(
x1,
x4)
eq_in_ag(
x1,
x2) =
eq_in_ag(
x2)
eq_out_ag(
x1,
x2) =
eq_out_ag(
x1,
x2)
U3_ggaa(
x1,
x2,
x3,
x4) =
U3_ggaa(
x1,
x4)
U4_ggaa(
x1,
x2,
x3,
x4,
x5) =
U4_ggaa(
x1,
x2,
x5)
minus_in_gga(
x1,
x2,
x3) =
minus_in_gga(
x1,
x2)
minus_out_gga(
x1,
x2,
x3) =
minus_out_gga(
x1,
x2,
x3)
s(
x1) =
s(
x1)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x1,
x2,
x4)
U5_ggaa(
x1,
x2,
x3,
x4,
x5) =
U5_ggaa(
x1,
x2,
x5)
DIV_IN_GGAA(
x1,
x2,
x3,
x4) =
DIV_IN_GGAA(
x1,
x2)
U1_GGAA(
x1,
x2,
x3,
x4) =
U1_GGAA(
x1,
x4)
FAILURE_IN_G(
x1) =
FAILURE_IN_G(
x1)
U2_GGAA(
x1,
x2,
x3,
x4) =
U2_GGAA(
x1,
x4)
EQ_IN_AG(
x1,
x2) =
EQ_IN_AG(
x2)
U3_GGAA(
x1,
x2,
x3,
x4) =
U3_GGAA(
x1,
x4)
U4_GGAA(
x1,
x2,
x3,
x4,
x5) =
U4_GGAA(
x1,
x2,
x5)
MINUS_IN_GGA(
x1,
x2,
x3) =
MINUS_IN_GGA(
x1,
x2)
U6_GGA(
x1,
x2,
x3,
x4) =
U6_GGA(
x1,
x2,
x4)
U5_GGAA(
x1,
x2,
x3,
x4,
x5) =
U5_GGAA(
x1,
x2,
x5)
We have to consider all (P,R,Pi)-chains
(44) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
DIV_IN_GGAA(X1, 0, X2, X3) → U1_GGAA(X1, X2, X3, failure_in_g(a))
DIV_IN_GGAA(X1, 0, X2, X3) → FAILURE_IN_G(a)
DIV_IN_GGAA(0, X4, Z, R) → U2_GGAA(X4, Z, R, eq_in_ag(Z, 0))
DIV_IN_GGAA(0, X4, Z, R) → EQ_IN_AG(Z, 0)
U2_GGAA(X4, Z, R, eq_out_ag(Z, 0)) → U3_GGAA(X4, Z, R, eq_in_ag(R, 0))
U2_GGAA(X4, Z, R, eq_out_ag(Z, 0)) → EQ_IN_AG(R, 0)
DIV_IN_GGAA(X, Y, s(Z), R) → U4_GGAA(X, Y, Z, R, minus_in_gga(X, Y, U))
DIV_IN_GGAA(X, Y, s(Z), R) → MINUS_IN_GGA(X, Y, U)
MINUS_IN_GGA(s(X), s(Y), Z) → U6_GGA(X, Y, Z, minus_in_gga(X, Y, Z))
MINUS_IN_GGA(s(X), s(Y), Z) → MINUS_IN_GGA(X, Y, Z)
U4_GGAA(X, Y, Z, R, minus_out_gga(X, Y, U)) → U5_GGAA(X, Y, Z, R, div_in_ggaa(U, Y, Z, R))
U4_GGAA(X, Y, Z, R, minus_out_gga(X, Y, U)) → DIV_IN_GGAA(U, Y, Z, R)
The TRS R consists of the following rules:
div_in_ggaa(X1, 0, X2, X3) → U1_ggaa(X1, X2, X3, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U1_ggaa(X1, X2, X3, failure_out_g(a)) → div_out_ggaa(X1, 0, X2, X3)
div_in_ggaa(0, X4, Z, R) → U2_ggaa(X4, Z, R, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U2_ggaa(X4, Z, R, eq_out_ag(Z, 0)) → U3_ggaa(X4, Z, R, eq_in_ag(R, 0))
U3_ggaa(X4, Z, R, eq_out_ag(R, 0)) → div_out_ggaa(0, X4, Z, R)
div_in_ggaa(X, Y, s(Z), R) → U4_ggaa(X, Y, Z, R, minus_in_gga(X, Y, U))
minus_in_gga(X, 0, X) → minus_out_gga(X, 0, X)
minus_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, minus_in_gga(X, Y, Z))
U6_gga(X, Y, Z, minus_out_gga(X, Y, Z)) → minus_out_gga(s(X), s(Y), Z)
U4_ggaa(X, Y, Z, R, minus_out_gga(X, Y, U)) → U5_ggaa(X, Y, Z, R, div_in_ggaa(U, Y, Z, R))
div_in_ggaa(X, X5, X6, X) → div_out_ggaa(X, X5, X6, X)
U5_ggaa(X, Y, Z, R, div_out_ggaa(U, Y, Z, R)) → div_out_ggaa(X, Y, s(Z), R)
The argument filtering Pi contains the following mapping:
div_in_ggaa(
x1,
x2,
x3,
x4) =
div_in_ggaa(
x1,
x2)
0 =
0
U1_ggaa(
x1,
x2,
x3,
x4) =
U1_ggaa(
x1,
x4)
failure_in_g(
x1) =
failure_in_g(
x1)
b =
b
failure_out_g(
x1) =
failure_out_g(
x1)
a =
a
div_out_ggaa(
x1,
x2,
x3,
x4) =
div_out_ggaa(
x1,
x2)
U2_ggaa(
x1,
x2,
x3,
x4) =
U2_ggaa(
x1,
x4)
eq_in_ag(
x1,
x2) =
eq_in_ag(
x2)
eq_out_ag(
x1,
x2) =
eq_out_ag(
x1,
x2)
U3_ggaa(
x1,
x2,
x3,
x4) =
U3_ggaa(
x1,
x4)
U4_ggaa(
x1,
x2,
x3,
x4,
x5) =
U4_ggaa(
x1,
x2,
x5)
minus_in_gga(
x1,
x2,
x3) =
minus_in_gga(
x1,
x2)
minus_out_gga(
x1,
x2,
x3) =
minus_out_gga(
x1,
x2,
x3)
s(
x1) =
s(
x1)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x1,
x2,
x4)
U5_ggaa(
x1,
x2,
x3,
x4,
x5) =
U5_ggaa(
x1,
x2,
x5)
DIV_IN_GGAA(
x1,
x2,
x3,
x4) =
DIV_IN_GGAA(
x1,
x2)
U1_GGAA(
x1,
x2,
x3,
x4) =
U1_GGAA(
x1,
x4)
FAILURE_IN_G(
x1) =
FAILURE_IN_G(
x1)
U2_GGAA(
x1,
x2,
x3,
x4) =
U2_GGAA(
x1,
x4)
EQ_IN_AG(
x1,
x2) =
EQ_IN_AG(
x2)
U3_GGAA(
x1,
x2,
x3,
x4) =
U3_GGAA(
x1,
x4)
U4_GGAA(
x1,
x2,
x3,
x4,
x5) =
U4_GGAA(
x1,
x2,
x5)
MINUS_IN_GGA(
x1,
x2,
x3) =
MINUS_IN_GGA(
x1,
x2)
U6_GGA(
x1,
x2,
x3,
x4) =
U6_GGA(
x1,
x2,
x4)
U5_GGAA(
x1,
x2,
x3,
x4,
x5) =
U5_GGAA(
x1,
x2,
x5)
We have to consider all (P,R,Pi)-chains
(45) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 9 less nodes.
(46) Complex Obligation (AND)
(47) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
MINUS_IN_GGA(s(X), s(Y), Z) → MINUS_IN_GGA(X, Y, Z)
The TRS R consists of the following rules:
div_in_ggaa(X1, 0, X2, X3) → U1_ggaa(X1, X2, X3, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U1_ggaa(X1, X2, X3, failure_out_g(a)) → div_out_ggaa(X1, 0, X2, X3)
div_in_ggaa(0, X4, Z, R) → U2_ggaa(X4, Z, R, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U2_ggaa(X4, Z, R, eq_out_ag(Z, 0)) → U3_ggaa(X4, Z, R, eq_in_ag(R, 0))
U3_ggaa(X4, Z, R, eq_out_ag(R, 0)) → div_out_ggaa(0, X4, Z, R)
div_in_ggaa(X, Y, s(Z), R) → U4_ggaa(X, Y, Z, R, minus_in_gga(X, Y, U))
minus_in_gga(X, 0, X) → minus_out_gga(X, 0, X)
minus_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, minus_in_gga(X, Y, Z))
U6_gga(X, Y, Z, minus_out_gga(X, Y, Z)) → minus_out_gga(s(X), s(Y), Z)
U4_ggaa(X, Y, Z, R, minus_out_gga(X, Y, U)) → U5_ggaa(X, Y, Z, R, div_in_ggaa(U, Y, Z, R))
div_in_ggaa(X, X5, X6, X) → div_out_ggaa(X, X5, X6, X)
U5_ggaa(X, Y, Z, R, div_out_ggaa(U, Y, Z, R)) → div_out_ggaa(X, Y, s(Z), R)
The argument filtering Pi contains the following mapping:
div_in_ggaa(
x1,
x2,
x3,
x4) =
div_in_ggaa(
x1,
x2)
0 =
0
U1_ggaa(
x1,
x2,
x3,
x4) =
U1_ggaa(
x1,
x4)
failure_in_g(
x1) =
failure_in_g(
x1)
b =
b
failure_out_g(
x1) =
failure_out_g(
x1)
a =
a
div_out_ggaa(
x1,
x2,
x3,
x4) =
div_out_ggaa(
x1,
x2)
U2_ggaa(
x1,
x2,
x3,
x4) =
U2_ggaa(
x1,
x4)
eq_in_ag(
x1,
x2) =
eq_in_ag(
x2)
eq_out_ag(
x1,
x2) =
eq_out_ag(
x1,
x2)
U3_ggaa(
x1,
x2,
x3,
x4) =
U3_ggaa(
x1,
x4)
U4_ggaa(
x1,
x2,
x3,
x4,
x5) =
U4_ggaa(
x1,
x2,
x5)
minus_in_gga(
x1,
x2,
x3) =
minus_in_gga(
x1,
x2)
minus_out_gga(
x1,
x2,
x3) =
minus_out_gga(
x1,
x2,
x3)
s(
x1) =
s(
x1)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x1,
x2,
x4)
U5_ggaa(
x1,
x2,
x3,
x4,
x5) =
U5_ggaa(
x1,
x2,
x5)
MINUS_IN_GGA(
x1,
x2,
x3) =
MINUS_IN_GGA(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(48) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(49) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
MINUS_IN_GGA(s(X), s(Y), Z) → MINUS_IN_GGA(X, Y, Z)
R is empty.
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
MINUS_IN_GGA(
x1,
x2,
x3) =
MINUS_IN_GGA(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(50) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(51) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MINUS_IN_GGA(s(X), s(Y)) → MINUS_IN_GGA(X, Y)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(52) 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:
- MINUS_IN_GGA(s(X), s(Y)) → MINUS_IN_GGA(X, Y)
The graph contains the following edges 1 > 1, 2 > 2
(53) TRUE
(54) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
DIV_IN_GGAA(X, Y, s(Z), R) → U4_GGAA(X, Y, Z, R, minus_in_gga(X, Y, U))
U4_GGAA(X, Y, Z, R, minus_out_gga(X, Y, U)) → DIV_IN_GGAA(U, Y, Z, R)
The TRS R consists of the following rules:
div_in_ggaa(X1, 0, X2, X3) → U1_ggaa(X1, X2, X3, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U1_ggaa(X1, X2, X3, failure_out_g(a)) → div_out_ggaa(X1, 0, X2, X3)
div_in_ggaa(0, X4, Z, R) → U2_ggaa(X4, Z, R, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U2_ggaa(X4, Z, R, eq_out_ag(Z, 0)) → U3_ggaa(X4, Z, R, eq_in_ag(R, 0))
U3_ggaa(X4, Z, R, eq_out_ag(R, 0)) → div_out_ggaa(0, X4, Z, R)
div_in_ggaa(X, Y, s(Z), R) → U4_ggaa(X, Y, Z, R, minus_in_gga(X, Y, U))
minus_in_gga(X, 0, X) → minus_out_gga(X, 0, X)
minus_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, minus_in_gga(X, Y, Z))
U6_gga(X, Y, Z, minus_out_gga(X, Y, Z)) → minus_out_gga(s(X), s(Y), Z)
U4_ggaa(X, Y, Z, R, minus_out_gga(X, Y, U)) → U5_ggaa(X, Y, Z, R, div_in_ggaa(U, Y, Z, R))
div_in_ggaa(X, X5, X6, X) → div_out_ggaa(X, X5, X6, X)
U5_ggaa(X, Y, Z, R, div_out_ggaa(U, Y, Z, R)) → div_out_ggaa(X, Y, s(Z), R)
The argument filtering Pi contains the following mapping:
div_in_ggaa(
x1,
x2,
x3,
x4) =
div_in_ggaa(
x1,
x2)
0 =
0
U1_ggaa(
x1,
x2,
x3,
x4) =
U1_ggaa(
x1,
x4)
failure_in_g(
x1) =
failure_in_g(
x1)
b =
b
failure_out_g(
x1) =
failure_out_g(
x1)
a =
a
div_out_ggaa(
x1,
x2,
x3,
x4) =
div_out_ggaa(
x1,
x2)
U2_ggaa(
x1,
x2,
x3,
x4) =
U2_ggaa(
x1,
x4)
eq_in_ag(
x1,
x2) =
eq_in_ag(
x2)
eq_out_ag(
x1,
x2) =
eq_out_ag(
x1,
x2)
U3_ggaa(
x1,
x2,
x3,
x4) =
U3_ggaa(
x1,
x4)
U4_ggaa(
x1,
x2,
x3,
x4,
x5) =
U4_ggaa(
x1,
x2,
x5)
minus_in_gga(
x1,
x2,
x3) =
minus_in_gga(
x1,
x2)
minus_out_gga(
x1,
x2,
x3) =
minus_out_gga(
x1,
x2,
x3)
s(
x1) =
s(
x1)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x1,
x2,
x4)
U5_ggaa(
x1,
x2,
x3,
x4,
x5) =
U5_ggaa(
x1,
x2,
x5)
DIV_IN_GGAA(
x1,
x2,
x3,
x4) =
DIV_IN_GGAA(
x1,
x2)
U4_GGAA(
x1,
x2,
x3,
x4,
x5) =
U4_GGAA(
x1,
x2,
x5)
We have to consider all (P,R,Pi)-chains
(55) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(56) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
DIV_IN_GGAA(X, Y, s(Z), R) → U4_GGAA(X, Y, Z, R, minus_in_gga(X, Y, U))
U4_GGAA(X, Y, Z, R, minus_out_gga(X, Y, U)) → DIV_IN_GGAA(U, Y, Z, R)
The TRS R consists of the following rules:
minus_in_gga(X, 0, X) → minus_out_gga(X, 0, X)
minus_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, minus_in_gga(X, Y, Z))
U6_gga(X, Y, Z, minus_out_gga(X, Y, Z)) → minus_out_gga(s(X), s(Y), Z)
The argument filtering Pi contains the following mapping:
0 =
0
minus_in_gga(
x1,
x2,
x3) =
minus_in_gga(
x1,
x2)
minus_out_gga(
x1,
x2,
x3) =
minus_out_gga(
x1,
x2,
x3)
s(
x1) =
s(
x1)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x1,
x2,
x4)
DIV_IN_GGAA(
x1,
x2,
x3,
x4) =
DIV_IN_GGAA(
x1,
x2)
U4_GGAA(
x1,
x2,
x3,
x4,
x5) =
U4_GGAA(
x1,
x2,
x5)
We have to consider all (P,R,Pi)-chains
(57) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(58) Obligation:
Q DP problem:
The TRS P consists of the following rules:
DIV_IN_GGAA(X, Y) → U4_GGAA(X, Y, minus_in_gga(X, Y))
U4_GGAA(X, Y, minus_out_gga(X, Y, U)) → DIV_IN_GGAA(U, Y)
The TRS R consists of the following rules:
minus_in_gga(X, 0) → minus_out_gga(X, 0, X)
minus_in_gga(s(X), s(Y)) → U6_gga(X, Y, minus_in_gga(X, Y))
U6_gga(X, Y, minus_out_gga(X, Y, Z)) → minus_out_gga(s(X), s(Y), Z)
The set Q consists of the following terms:
minus_in_gga(x0, x1)
U6_gga(x0, x1, x2)
We have to consider all (P,Q,R)-chains.
(59) Narrowing (SOUND transformation)
By narrowing [LPAR04] the rule
DIV_IN_GGAA(
X,
Y) →
U4_GGAA(
X,
Y,
minus_in_gga(
X,
Y)) at position [2] we obtained the following new rules [LPAR04]:
DIV_IN_GGAA(x0, 0) → U4_GGAA(x0, 0, minus_out_gga(x0, 0, x0))
DIV_IN_GGAA(s(x0), s(x1)) → U4_GGAA(s(x0), s(x1), U6_gga(x0, x1, minus_in_gga(x0, x1)))
(60) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_GGAA(X, Y, minus_out_gga(X, Y, U)) → DIV_IN_GGAA(U, Y)
DIV_IN_GGAA(x0, 0) → U4_GGAA(x0, 0, minus_out_gga(x0, 0, x0))
DIV_IN_GGAA(s(x0), s(x1)) → U4_GGAA(s(x0), s(x1), U6_gga(x0, x1, minus_in_gga(x0, x1)))
The TRS R consists of the following rules:
minus_in_gga(X, 0) → minus_out_gga(X, 0, X)
minus_in_gga(s(X), s(Y)) → U6_gga(X, Y, minus_in_gga(X, Y))
U6_gga(X, Y, minus_out_gga(X, Y, Z)) → minus_out_gga(s(X), s(Y), Z)
The set Q consists of the following terms:
minus_in_gga(x0, x1)
U6_gga(x0, x1, x2)
We have to consider all (P,Q,R)-chains.
(61) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
U4_GGAA(
X,
Y,
minus_out_gga(
X,
Y,
U)) →
DIV_IN_GGAA(
U,
Y) we obtained the following new rules [LPAR04]:
U4_GGAA(z0, 0, minus_out_gga(z0, 0, z0)) → DIV_IN_GGAA(z0, 0)
U4_GGAA(s(z0), s(z1), minus_out_gga(s(z0), s(z1), x2)) → DIV_IN_GGAA(x2, s(z1))
(62) Obligation:
Q DP problem:
The TRS P consists of the following rules:
DIV_IN_GGAA(x0, 0) → U4_GGAA(x0, 0, minus_out_gga(x0, 0, x0))
DIV_IN_GGAA(s(x0), s(x1)) → U4_GGAA(s(x0), s(x1), U6_gga(x0, x1, minus_in_gga(x0, x1)))
U4_GGAA(z0, 0, minus_out_gga(z0, 0, z0)) → DIV_IN_GGAA(z0, 0)
U4_GGAA(s(z0), s(z1), minus_out_gga(s(z0), s(z1), x2)) → DIV_IN_GGAA(x2, s(z1))
The TRS R consists of the following rules:
minus_in_gga(X, 0) → minus_out_gga(X, 0, X)
minus_in_gga(s(X), s(Y)) → U6_gga(X, Y, minus_in_gga(X, Y))
U6_gga(X, Y, minus_out_gga(X, Y, Z)) → minus_out_gga(s(X), s(Y), Z)
The set Q consists of the following terms:
minus_in_gga(x0, x1)
U6_gga(x0, x1, x2)
We have to consider all (P,Q,R)-chains.
(63) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs.
(64) Complex Obligation (AND)
(65) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_GGAA(s(z0), s(z1), minus_out_gga(s(z0), s(z1), x2)) → DIV_IN_GGAA(x2, s(z1))
DIV_IN_GGAA(s(x0), s(x1)) → U4_GGAA(s(x0), s(x1), U6_gga(x0, x1, minus_in_gga(x0, x1)))
The TRS R consists of the following rules:
minus_in_gga(X, 0) → minus_out_gga(X, 0, X)
minus_in_gga(s(X), s(Y)) → U6_gga(X, Y, minus_in_gga(X, Y))
U6_gga(X, Y, minus_out_gga(X, Y, Z)) → minus_out_gga(s(X), s(Y), Z)
The set Q consists of the following terms:
minus_in_gga(x0, x1)
U6_gga(x0, x1, x2)
We have to consider all (P,Q,R)-chains.
(66) ForwardInstantiation (EQUIVALENT transformation)
By forward instantiating [JAR06] the rule
U4_GGAA(
s(
z0),
s(
z1),
minus_out_gga(
s(
z0),
s(
z1),
x2)) →
DIV_IN_GGAA(
x2,
s(
z1)) we obtained the following new rules [LPAR04]:
U4_GGAA(s(x0), s(x1), minus_out_gga(s(x0), s(x1), s(y_0))) → DIV_IN_GGAA(s(y_0), s(x1))
(67) Obligation:
Q DP problem:
The TRS P consists of the following rules:
DIV_IN_GGAA(s(x0), s(x1)) → U4_GGAA(s(x0), s(x1), U6_gga(x0, x1, minus_in_gga(x0, x1)))
U4_GGAA(s(x0), s(x1), minus_out_gga(s(x0), s(x1), s(y_0))) → DIV_IN_GGAA(s(y_0), s(x1))
The TRS R consists of the following rules:
minus_in_gga(X, 0) → minus_out_gga(X, 0, X)
minus_in_gga(s(X), s(Y)) → U6_gga(X, Y, minus_in_gga(X, Y))
U6_gga(X, Y, minus_out_gga(X, Y, Z)) → minus_out_gga(s(X), s(Y), Z)
The set Q consists of the following terms:
minus_in_gga(x0, x1)
U6_gga(x0, x1, x2)
We have to consider all (P,Q,R)-chains.
(68) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
DIV_IN_GGAA(s(x0), s(x1)) → U4_GGAA(s(x0), s(x1), U6_gga(x0, x1, minus_in_gga(x0, x1)))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:
| POL(DIV_IN_GGAA(x1, x2)) = | 0 | + | | · | x1 | + | | · | x2 |
| POL(U4_GGAA(x1, x2, x3)) = | 0 | + | | · | x1 | + | | · | x2 | + | | · | x3 |
| POL(U6_gga(x1, x2, x3)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 |
| POL(minus_in_gga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
| POL(minus_out_gga(x1, x2, x3)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 |
The following usable rules [FROCOS05] were oriented:
minus_in_gga(X, 0) → minus_out_gga(X, 0, X)
minus_in_gga(s(X), s(Y)) → U6_gga(X, Y, minus_in_gga(X, Y))
U6_gga(X, Y, minus_out_gga(X, Y, Z)) → minus_out_gga(s(X), s(Y), Z)
(69) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_GGAA(s(x0), s(x1), minus_out_gga(s(x0), s(x1), s(y_0))) → DIV_IN_GGAA(s(y_0), s(x1))
The TRS R consists of the following rules:
minus_in_gga(X, 0) → minus_out_gga(X, 0, X)
minus_in_gga(s(X), s(Y)) → U6_gga(X, Y, minus_in_gga(X, Y))
U6_gga(X, Y, minus_out_gga(X, Y, Z)) → minus_out_gga(s(X), s(Y), Z)
The set Q consists of the following terms:
minus_in_gga(x0, x1)
U6_gga(x0, x1, x2)
We have to consider all (P,Q,R)-chains.
(70) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.
(71) TRUE
(72) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_GGAA(z0, 0, minus_out_gga(z0, 0, z0)) → DIV_IN_GGAA(z0, 0)
DIV_IN_GGAA(x0, 0) → U4_GGAA(x0, 0, minus_out_gga(x0, 0, x0))
The TRS R consists of the following rules:
minus_in_gga(X, 0) → minus_out_gga(X, 0, X)
minus_in_gga(s(X), s(Y)) → U6_gga(X, Y, minus_in_gga(X, Y))
U6_gga(X, Y, minus_out_gga(X, Y, Z)) → minus_out_gga(s(X), s(Y), Z)
The set Q consists of the following terms:
minus_in_gga(x0, x1)
U6_gga(x0, x1, x2)
We have to consider all (P,Q,R)-chains.
(73) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(74) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_GGAA(z0, 0, minus_out_gga(z0, 0, z0)) → DIV_IN_GGAA(z0, 0)
DIV_IN_GGAA(x0, 0) → U4_GGAA(x0, 0, minus_out_gga(x0, 0, x0))
R is empty.
The set Q consists of the following terms:
minus_in_gga(x0, x1)
U6_gga(x0, x1, x2)
We have to consider all (P,Q,R)-chains.
(75) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
minus_in_gga(x0, x1)
U6_gga(x0, x1, x2)
(76) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_GGAA(z0, 0, minus_out_gga(z0, 0, z0)) → DIV_IN_GGAA(z0, 0)
DIV_IN_GGAA(x0, 0) → U4_GGAA(x0, 0, minus_out_gga(x0, 0, x0))
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(77) NonTerminationProof (EQUIVALENT transformation)
We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:
s =
DIV_IN_GGAA(
x0,
0) evaluates to t =
DIV_IN_GGAA(
x0,
0)
Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
- Semiunifier: [ ]
- Matcher: [ ]
Rewriting sequenceDIV_IN_GGAA(x0, 0) →
U4_GGAA(
x0,
0,
minus_out_gga(
x0,
0,
x0))
with rule
DIV_IN_GGAA(
x0',
0) →
U4_GGAA(
x0',
0,
minus_out_gga(
x0',
0,
x0')) at position [] and matcher [
x0' /
x0]
U4_GGAA(x0, 0, minus_out_gga(x0, 0, x0)) →
DIV_IN_GGAA(
x0,
0)
with rule
U4_GGAA(
z0,
0,
minus_out_gga(
z0,
0,
z0)) →
DIV_IN_GGAA(
z0,
0)
Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence
All these steps are and every following step will be a correct step w.r.t to Q.
(78) FALSE