(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 sequence

DIV_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 +
[0,1]
·x1 +
[0,0]
·x2

POL(s(x1)) =
/0\
\1/
+
/00\
\11/
·x1

POL(U4_GGAA(x1, x2, x3)) = 0 +
[0,0]
·x1 +
[0,0]
·x2 +
[0,1]
·x3

POL(U6_gga(x1, x2, x3)) =
/0\
\0/
+
/10\
\00/
·x1 +
/00\
\00/
·x2 +
/01\
\10/
·x3

POL(minus_in_gga(x1, x2)) =
/0\
\0/
+
/01\
\01/
·x1 +
/00\
\00/
·x2

POL(minus_out_gga(x1, x2, x3)) =
/0\
\0/
+
/00\
\00/
·x1 +
/00\
\00/
·x2 +
/01\
\01/
·x3

POL(0) =
/0\
\0/

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 sequence

DIV_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