(0) Obligation:

Clauses:

div(0, Y, 0) :- no(zero(Y)).
div(X, Y, s(Z)) :- ','(no(zero(X)), ','(no(zero(Y)), ','(minus(X, Y, U), div(U, Y, Z)))).
minus(0, Y, 0).
minus(X, 0, X).
minus(s(X), s(Y), Z) :- minus(X, Y, Z).
zero(0).
no(X) :- ','(X, ','(!, failure(a))).
no(X1).
failure(b).

Queries:

div(g,g,a).

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph.

(2) Obligation:

Clauses:

div1(0, T6, 0).
div1(T12, T14, s(T10)) :- minus37(T12, T14, X15).
div1(T12, T14, s(T10)) :- ','(minus37(T12, T14, T15), div1(T15, T14, T10)).
minus44(0, T18, 0).
minus44(T19, 0, T19).
minus44(s(T20), s(T21), X47) :- minus44(T20, T21, X47).
minus37(s(0), s(T18), 0).
minus37(s(T19), s(0), T19).
minus37(s(s(T20)), s(s(T21)), X47) :- minus44(T20, T21, X47).

Queries:

div1(g,g,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:
div1_in: (b,b,f)
minus37_in: (b,b,f)
minus44_in: (b,b,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

div1_in_gga(0, T6, 0) → div1_out_gga(0, T6, 0)
div1_in_gga(T12, T14, s(T10)) → U1_gga(T12, T14, T10, minus37_in_gga(T12, T14, X15))
minus37_in_gga(s(0), s(T18), 0) → minus37_out_gga(s(0), s(T18), 0)
minus37_in_gga(s(T19), s(0), T19) → minus37_out_gga(s(T19), s(0), T19)
minus37_in_gga(s(s(T20)), s(s(T21)), X47) → U5_gga(T20, T21, X47, minus44_in_gga(T20, T21, X47))
minus44_in_gga(0, T18, 0) → minus44_out_gga(0, T18, 0)
minus44_in_gga(T19, 0, T19) → minus44_out_gga(T19, 0, T19)
minus44_in_gga(s(T20), s(T21), X47) → U4_gga(T20, T21, X47, minus44_in_gga(T20, T21, X47))
U4_gga(T20, T21, X47, minus44_out_gga(T20, T21, X47)) → minus44_out_gga(s(T20), s(T21), X47)
U5_gga(T20, T21, X47, minus44_out_gga(T20, T21, X47)) → minus37_out_gga(s(s(T20)), s(s(T21)), X47)
U1_gga(T12, T14, T10, minus37_out_gga(T12, T14, X15)) → div1_out_gga(T12, T14, s(T10))
div1_in_gga(T12, T14, s(T10)) → U2_gga(T12, T14, T10, minus37_in_gga(T12, T14, T15))
U2_gga(T12, T14, T10, minus37_out_gga(T12, T14, T15)) → U3_gga(T12, T14, T10, div1_in_gga(T15, T14, T10))
U3_gga(T12, T14, T10, div1_out_gga(T15, T14, T10)) → div1_out_gga(T12, T14, s(T10))

The argument filtering Pi contains the following mapping:
div1_in_gga(x1, x2, x3)  =  div1_in_gga(x1, x2)
0  =  0
div1_out_gga(x1, x2, x3)  =  div1_out_gga
U1_gga(x1, x2, x3, x4)  =  U1_gga(x4)
minus37_in_gga(x1, x2, x3)  =  minus37_in_gga(x1, x2)
s(x1)  =  s(x1)
minus37_out_gga(x1, x2, x3)  =  minus37_out_gga(x3)
U5_gga(x1, x2, x3, x4)  =  U5_gga(x4)
minus44_in_gga(x1, x2, x3)  =  minus44_in_gga(x1, x2)
minus44_out_gga(x1, x2, x3)  =  minus44_out_gga(x3)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x4)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x2, x4)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x4)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

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

div1_in_gga(0, T6, 0) → div1_out_gga(0, T6, 0)
div1_in_gga(T12, T14, s(T10)) → U1_gga(T12, T14, T10, minus37_in_gga(T12, T14, X15))
minus37_in_gga(s(0), s(T18), 0) → minus37_out_gga(s(0), s(T18), 0)
minus37_in_gga(s(T19), s(0), T19) → minus37_out_gga(s(T19), s(0), T19)
minus37_in_gga(s(s(T20)), s(s(T21)), X47) → U5_gga(T20, T21, X47, minus44_in_gga(T20, T21, X47))
minus44_in_gga(0, T18, 0) → minus44_out_gga(0, T18, 0)
minus44_in_gga(T19, 0, T19) → minus44_out_gga(T19, 0, T19)
minus44_in_gga(s(T20), s(T21), X47) → U4_gga(T20, T21, X47, minus44_in_gga(T20, T21, X47))
U4_gga(T20, T21, X47, minus44_out_gga(T20, T21, X47)) → minus44_out_gga(s(T20), s(T21), X47)
U5_gga(T20, T21, X47, minus44_out_gga(T20, T21, X47)) → minus37_out_gga(s(s(T20)), s(s(T21)), X47)
U1_gga(T12, T14, T10, minus37_out_gga(T12, T14, X15)) → div1_out_gga(T12, T14, s(T10))
div1_in_gga(T12, T14, s(T10)) → U2_gga(T12, T14, T10, minus37_in_gga(T12, T14, T15))
U2_gga(T12, T14, T10, minus37_out_gga(T12, T14, T15)) → U3_gga(T12, T14, T10, div1_in_gga(T15, T14, T10))
U3_gga(T12, T14, T10, div1_out_gga(T15, T14, T10)) → div1_out_gga(T12, T14, s(T10))

The argument filtering Pi contains the following mapping:
div1_in_gga(x1, x2, x3)  =  div1_in_gga(x1, x2)
0  =  0
div1_out_gga(x1, x2, x3)  =  div1_out_gga
U1_gga(x1, x2, x3, x4)  =  U1_gga(x4)
minus37_in_gga(x1, x2, x3)  =  minus37_in_gga(x1, x2)
s(x1)  =  s(x1)
minus37_out_gga(x1, x2, x3)  =  minus37_out_gga(x3)
U5_gga(x1, x2, x3, x4)  =  U5_gga(x4)
minus44_in_gga(x1, x2, x3)  =  minus44_in_gga(x1, x2)
minus44_out_gga(x1, x2, x3)  =  minus44_out_gga(x3)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x4)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x2, x4)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x4)

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

DIV1_IN_GGA(T12, T14, s(T10)) → U1_GGA(T12, T14, T10, minus37_in_gga(T12, T14, X15))
DIV1_IN_GGA(T12, T14, s(T10)) → MINUS37_IN_GGA(T12, T14, X15)
MINUS37_IN_GGA(s(s(T20)), s(s(T21)), X47) → U5_GGA(T20, T21, X47, minus44_in_gga(T20, T21, X47))
MINUS37_IN_GGA(s(s(T20)), s(s(T21)), X47) → MINUS44_IN_GGA(T20, T21, X47)
MINUS44_IN_GGA(s(T20), s(T21), X47) → U4_GGA(T20, T21, X47, minus44_in_gga(T20, T21, X47))
MINUS44_IN_GGA(s(T20), s(T21), X47) → MINUS44_IN_GGA(T20, T21, X47)
DIV1_IN_GGA(T12, T14, s(T10)) → U2_GGA(T12, T14, T10, minus37_in_gga(T12, T14, T15))
U2_GGA(T12, T14, T10, minus37_out_gga(T12, T14, T15)) → U3_GGA(T12, T14, T10, div1_in_gga(T15, T14, T10))
U2_GGA(T12, T14, T10, minus37_out_gga(T12, T14, T15)) → DIV1_IN_GGA(T15, T14, T10)

The TRS R consists of the following rules:

div1_in_gga(0, T6, 0) → div1_out_gga(0, T6, 0)
div1_in_gga(T12, T14, s(T10)) → U1_gga(T12, T14, T10, minus37_in_gga(T12, T14, X15))
minus37_in_gga(s(0), s(T18), 0) → minus37_out_gga(s(0), s(T18), 0)
minus37_in_gga(s(T19), s(0), T19) → minus37_out_gga(s(T19), s(0), T19)
minus37_in_gga(s(s(T20)), s(s(T21)), X47) → U5_gga(T20, T21, X47, minus44_in_gga(T20, T21, X47))
minus44_in_gga(0, T18, 0) → minus44_out_gga(0, T18, 0)
minus44_in_gga(T19, 0, T19) → minus44_out_gga(T19, 0, T19)
minus44_in_gga(s(T20), s(T21), X47) → U4_gga(T20, T21, X47, minus44_in_gga(T20, T21, X47))
U4_gga(T20, T21, X47, minus44_out_gga(T20, T21, X47)) → minus44_out_gga(s(T20), s(T21), X47)
U5_gga(T20, T21, X47, minus44_out_gga(T20, T21, X47)) → minus37_out_gga(s(s(T20)), s(s(T21)), X47)
U1_gga(T12, T14, T10, minus37_out_gga(T12, T14, X15)) → div1_out_gga(T12, T14, s(T10))
div1_in_gga(T12, T14, s(T10)) → U2_gga(T12, T14, T10, minus37_in_gga(T12, T14, T15))
U2_gga(T12, T14, T10, minus37_out_gga(T12, T14, T15)) → U3_gga(T12, T14, T10, div1_in_gga(T15, T14, T10))
U3_gga(T12, T14, T10, div1_out_gga(T15, T14, T10)) → div1_out_gga(T12, T14, s(T10))

The argument filtering Pi contains the following mapping:
div1_in_gga(x1, x2, x3)  =  div1_in_gga(x1, x2)
0  =  0
div1_out_gga(x1, x2, x3)  =  div1_out_gga
U1_gga(x1, x2, x3, x4)  =  U1_gga(x4)
minus37_in_gga(x1, x2, x3)  =  minus37_in_gga(x1, x2)
s(x1)  =  s(x1)
minus37_out_gga(x1, x2, x3)  =  minus37_out_gga(x3)
U5_gga(x1, x2, x3, x4)  =  U5_gga(x4)
minus44_in_gga(x1, x2, x3)  =  minus44_in_gga(x1, x2)
minus44_out_gga(x1, x2, x3)  =  minus44_out_gga(x3)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x4)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x2, x4)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x4)
DIV1_IN_GGA(x1, x2, x3)  =  DIV1_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4)  =  U1_GGA(x4)
MINUS37_IN_GGA(x1, x2, x3)  =  MINUS37_IN_GGA(x1, x2)
U5_GGA(x1, x2, x3, x4)  =  U5_GGA(x4)
MINUS44_IN_GGA(x1, x2, x3)  =  MINUS44_IN_GGA(x1, x2)
U4_GGA(x1, x2, x3, x4)  =  U4_GGA(x4)
U2_GGA(x1, x2, x3, x4)  =  U2_GGA(x2, x4)
U3_GGA(x1, x2, x3, x4)  =  U3_GGA(x4)

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

(6) Obligation:

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

DIV1_IN_GGA(T12, T14, s(T10)) → U1_GGA(T12, T14, T10, minus37_in_gga(T12, T14, X15))
DIV1_IN_GGA(T12, T14, s(T10)) → MINUS37_IN_GGA(T12, T14, X15)
MINUS37_IN_GGA(s(s(T20)), s(s(T21)), X47) → U5_GGA(T20, T21, X47, minus44_in_gga(T20, T21, X47))
MINUS37_IN_GGA(s(s(T20)), s(s(T21)), X47) → MINUS44_IN_GGA(T20, T21, X47)
MINUS44_IN_GGA(s(T20), s(T21), X47) → U4_GGA(T20, T21, X47, minus44_in_gga(T20, T21, X47))
MINUS44_IN_GGA(s(T20), s(T21), X47) → MINUS44_IN_GGA(T20, T21, X47)
DIV1_IN_GGA(T12, T14, s(T10)) → U2_GGA(T12, T14, T10, minus37_in_gga(T12, T14, T15))
U2_GGA(T12, T14, T10, minus37_out_gga(T12, T14, T15)) → U3_GGA(T12, T14, T10, div1_in_gga(T15, T14, T10))
U2_GGA(T12, T14, T10, minus37_out_gga(T12, T14, T15)) → DIV1_IN_GGA(T15, T14, T10)

The TRS R consists of the following rules:

div1_in_gga(0, T6, 0) → div1_out_gga(0, T6, 0)
div1_in_gga(T12, T14, s(T10)) → U1_gga(T12, T14, T10, minus37_in_gga(T12, T14, X15))
minus37_in_gga(s(0), s(T18), 0) → minus37_out_gga(s(0), s(T18), 0)
minus37_in_gga(s(T19), s(0), T19) → minus37_out_gga(s(T19), s(0), T19)
minus37_in_gga(s(s(T20)), s(s(T21)), X47) → U5_gga(T20, T21, X47, minus44_in_gga(T20, T21, X47))
minus44_in_gga(0, T18, 0) → minus44_out_gga(0, T18, 0)
minus44_in_gga(T19, 0, T19) → minus44_out_gga(T19, 0, T19)
minus44_in_gga(s(T20), s(T21), X47) → U4_gga(T20, T21, X47, minus44_in_gga(T20, T21, X47))
U4_gga(T20, T21, X47, minus44_out_gga(T20, T21, X47)) → minus44_out_gga(s(T20), s(T21), X47)
U5_gga(T20, T21, X47, minus44_out_gga(T20, T21, X47)) → minus37_out_gga(s(s(T20)), s(s(T21)), X47)
U1_gga(T12, T14, T10, minus37_out_gga(T12, T14, X15)) → div1_out_gga(T12, T14, s(T10))
div1_in_gga(T12, T14, s(T10)) → U2_gga(T12, T14, T10, minus37_in_gga(T12, T14, T15))
U2_gga(T12, T14, T10, minus37_out_gga(T12, T14, T15)) → U3_gga(T12, T14, T10, div1_in_gga(T15, T14, T10))
U3_gga(T12, T14, T10, div1_out_gga(T15, T14, T10)) → div1_out_gga(T12, T14, s(T10))

The argument filtering Pi contains the following mapping:
div1_in_gga(x1, x2, x3)  =  div1_in_gga(x1, x2)
0  =  0
div1_out_gga(x1, x2, x3)  =  div1_out_gga
U1_gga(x1, x2, x3, x4)  =  U1_gga(x4)
minus37_in_gga(x1, x2, x3)  =  minus37_in_gga(x1, x2)
s(x1)  =  s(x1)
minus37_out_gga(x1, x2, x3)  =  minus37_out_gga(x3)
U5_gga(x1, x2, x3, x4)  =  U5_gga(x4)
minus44_in_gga(x1, x2, x3)  =  minus44_in_gga(x1, x2)
minus44_out_gga(x1, x2, x3)  =  minus44_out_gga(x3)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x4)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x2, x4)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x4)
DIV1_IN_GGA(x1, x2, x3)  =  DIV1_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4)  =  U1_GGA(x4)
MINUS37_IN_GGA(x1, x2, x3)  =  MINUS37_IN_GGA(x1, x2)
U5_GGA(x1, x2, x3, x4)  =  U5_GGA(x4)
MINUS44_IN_GGA(x1, x2, x3)  =  MINUS44_IN_GGA(x1, x2)
U4_GGA(x1, x2, x3, x4)  =  U4_GGA(x4)
U2_GGA(x1, x2, x3, x4)  =  U2_GGA(x2, x4)
U3_GGA(x1, x2, x3, x4)  =  U3_GGA(x4)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 6 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

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

MINUS44_IN_GGA(s(T20), s(T21), X47) → MINUS44_IN_GGA(T20, T21, X47)

The TRS R consists of the following rules:

div1_in_gga(0, T6, 0) → div1_out_gga(0, T6, 0)
div1_in_gga(T12, T14, s(T10)) → U1_gga(T12, T14, T10, minus37_in_gga(T12, T14, X15))
minus37_in_gga(s(0), s(T18), 0) → minus37_out_gga(s(0), s(T18), 0)
minus37_in_gga(s(T19), s(0), T19) → minus37_out_gga(s(T19), s(0), T19)
minus37_in_gga(s(s(T20)), s(s(T21)), X47) → U5_gga(T20, T21, X47, minus44_in_gga(T20, T21, X47))
minus44_in_gga(0, T18, 0) → minus44_out_gga(0, T18, 0)
minus44_in_gga(T19, 0, T19) → minus44_out_gga(T19, 0, T19)
minus44_in_gga(s(T20), s(T21), X47) → U4_gga(T20, T21, X47, minus44_in_gga(T20, T21, X47))
U4_gga(T20, T21, X47, minus44_out_gga(T20, T21, X47)) → minus44_out_gga(s(T20), s(T21), X47)
U5_gga(T20, T21, X47, minus44_out_gga(T20, T21, X47)) → minus37_out_gga(s(s(T20)), s(s(T21)), X47)
U1_gga(T12, T14, T10, minus37_out_gga(T12, T14, X15)) → div1_out_gga(T12, T14, s(T10))
div1_in_gga(T12, T14, s(T10)) → U2_gga(T12, T14, T10, minus37_in_gga(T12, T14, T15))
U2_gga(T12, T14, T10, minus37_out_gga(T12, T14, T15)) → U3_gga(T12, T14, T10, div1_in_gga(T15, T14, T10))
U3_gga(T12, T14, T10, div1_out_gga(T15, T14, T10)) → div1_out_gga(T12, T14, s(T10))

The argument filtering Pi contains the following mapping:
div1_in_gga(x1, x2, x3)  =  div1_in_gga(x1, x2)
0  =  0
div1_out_gga(x1, x2, x3)  =  div1_out_gga
U1_gga(x1, x2, x3, x4)  =  U1_gga(x4)
minus37_in_gga(x1, x2, x3)  =  minus37_in_gga(x1, x2)
s(x1)  =  s(x1)
minus37_out_gga(x1, x2, x3)  =  minus37_out_gga(x3)
U5_gga(x1, x2, x3, x4)  =  U5_gga(x4)
minus44_in_gga(x1, x2, x3)  =  minus44_in_gga(x1, x2)
minus44_out_gga(x1, x2, x3)  =  minus44_out_gga(x3)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x4)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x2, x4)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x4)
MINUS44_IN_GGA(x1, x2, x3)  =  MINUS44_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:

MINUS44_IN_GGA(s(T20), s(T21), X47) → MINUS44_IN_GGA(T20, T21, X47)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
MINUS44_IN_GGA(x1, x2, x3)  =  MINUS44_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:

MINUS44_IN_GGA(s(T20), s(T21)) → MINUS44_IN_GGA(T20, T21)

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:

  • MINUS44_IN_GGA(s(T20), s(T21)) → MINUS44_IN_GGA(T20, T21)
    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:

DIV1_IN_GGA(T12, T14, s(T10)) → U2_GGA(T12, T14, T10, minus37_in_gga(T12, T14, T15))
U2_GGA(T12, T14, T10, minus37_out_gga(T12, T14, T15)) → DIV1_IN_GGA(T15, T14, T10)

The TRS R consists of the following rules:

div1_in_gga(0, T6, 0) → div1_out_gga(0, T6, 0)
div1_in_gga(T12, T14, s(T10)) → U1_gga(T12, T14, T10, minus37_in_gga(T12, T14, X15))
minus37_in_gga(s(0), s(T18), 0) → minus37_out_gga(s(0), s(T18), 0)
minus37_in_gga(s(T19), s(0), T19) → minus37_out_gga(s(T19), s(0), T19)
minus37_in_gga(s(s(T20)), s(s(T21)), X47) → U5_gga(T20, T21, X47, minus44_in_gga(T20, T21, X47))
minus44_in_gga(0, T18, 0) → minus44_out_gga(0, T18, 0)
minus44_in_gga(T19, 0, T19) → minus44_out_gga(T19, 0, T19)
minus44_in_gga(s(T20), s(T21), X47) → U4_gga(T20, T21, X47, minus44_in_gga(T20, T21, X47))
U4_gga(T20, T21, X47, minus44_out_gga(T20, T21, X47)) → minus44_out_gga(s(T20), s(T21), X47)
U5_gga(T20, T21, X47, minus44_out_gga(T20, T21, X47)) → minus37_out_gga(s(s(T20)), s(s(T21)), X47)
U1_gga(T12, T14, T10, minus37_out_gga(T12, T14, X15)) → div1_out_gga(T12, T14, s(T10))
div1_in_gga(T12, T14, s(T10)) → U2_gga(T12, T14, T10, minus37_in_gga(T12, T14, T15))
U2_gga(T12, T14, T10, minus37_out_gga(T12, T14, T15)) → U3_gga(T12, T14, T10, div1_in_gga(T15, T14, T10))
U3_gga(T12, T14, T10, div1_out_gga(T15, T14, T10)) → div1_out_gga(T12, T14, s(T10))

The argument filtering Pi contains the following mapping:
div1_in_gga(x1, x2, x3)  =  div1_in_gga(x1, x2)
0  =  0
div1_out_gga(x1, x2, x3)  =  div1_out_gga
U1_gga(x1, x2, x3, x4)  =  U1_gga(x4)
minus37_in_gga(x1, x2, x3)  =  minus37_in_gga(x1, x2)
s(x1)  =  s(x1)
minus37_out_gga(x1, x2, x3)  =  minus37_out_gga(x3)
U5_gga(x1, x2, x3, x4)  =  U5_gga(x4)
minus44_in_gga(x1, x2, x3)  =  minus44_in_gga(x1, x2)
minus44_out_gga(x1, x2, x3)  =  minus44_out_gga(x3)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x4)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x2, x4)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x4)
DIV1_IN_GGA(x1, x2, x3)  =  DIV1_IN_GGA(x1, x2)
U2_GGA(x1, x2, x3, x4)  =  U2_GGA(x2, x4)

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:

DIV1_IN_GGA(T12, T14, s(T10)) → U2_GGA(T12, T14, T10, minus37_in_gga(T12, T14, T15))
U2_GGA(T12, T14, T10, minus37_out_gga(T12, T14, T15)) → DIV1_IN_GGA(T15, T14, T10)

The TRS R consists of the following rules:

minus37_in_gga(s(0), s(T18), 0) → minus37_out_gga(s(0), s(T18), 0)
minus37_in_gga(s(T19), s(0), T19) → minus37_out_gga(s(T19), s(0), T19)
minus37_in_gga(s(s(T20)), s(s(T21)), X47) → U5_gga(T20, T21, X47, minus44_in_gga(T20, T21, X47))
U5_gga(T20, T21, X47, minus44_out_gga(T20, T21, X47)) → minus37_out_gga(s(s(T20)), s(s(T21)), X47)
minus44_in_gga(0, T18, 0) → minus44_out_gga(0, T18, 0)
minus44_in_gga(T19, 0, T19) → minus44_out_gga(T19, 0, T19)
minus44_in_gga(s(T20), s(T21), X47) → U4_gga(T20, T21, X47, minus44_in_gga(T20, T21, X47))
U4_gga(T20, T21, X47, minus44_out_gga(T20, T21, X47)) → minus44_out_gga(s(T20), s(T21), X47)

The argument filtering Pi contains the following mapping:
0  =  0
minus37_in_gga(x1, x2, x3)  =  minus37_in_gga(x1, x2)
s(x1)  =  s(x1)
minus37_out_gga(x1, x2, x3)  =  minus37_out_gga(x3)
U5_gga(x1, x2, x3, x4)  =  U5_gga(x4)
minus44_in_gga(x1, x2, x3)  =  minus44_in_gga(x1, x2)
minus44_out_gga(x1, x2, x3)  =  minus44_out_gga(x3)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x4)
DIV1_IN_GGA(x1, x2, x3)  =  DIV1_IN_GGA(x1, x2)
U2_GGA(x1, x2, x3, x4)  =  U2_GGA(x2, x4)

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:

DIV1_IN_GGA(T12, T14) → U2_GGA(T14, minus37_in_gga(T12, T14))
U2_GGA(T14, minus37_out_gga(T15)) → DIV1_IN_GGA(T15, T14)

The TRS R consists of the following rules:

minus37_in_gga(s(0), s(T18)) → minus37_out_gga(0)
minus37_in_gga(s(T19), s(0)) → minus37_out_gga(T19)
minus37_in_gga(s(s(T20)), s(s(T21))) → U5_gga(minus44_in_gga(T20, T21))
U5_gga(minus44_out_gga(X47)) → minus37_out_gga(X47)
minus44_in_gga(0, T18) → minus44_out_gga(0)
minus44_in_gga(T19, 0) → minus44_out_gga(T19)
minus44_in_gga(s(T20), s(T21)) → U4_gga(minus44_in_gga(T20, T21))
U4_gga(minus44_out_gga(X47)) → minus44_out_gga(X47)

The set Q consists of the following terms:

minus37_in_gga(x0, x1)
U5_gga(x0)
minus44_in_gga(x0, x1)
U4_gga(x0)

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

(21) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


U2_GGA(T14, minus37_out_gga(T15)) → DIV1_IN_GGA(T15, T14)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(DIV1_IN_GGA(x1, x2)) = x1   
POL(U2_GGA(x1, x2)) = x2   
POL(U4_gga(x1)) = 1 + x1   
POL(U5_gga(x1)) = x1   
POL(minus37_in_gga(x1, x2)) = x1   
POL(minus37_out_gga(x1)) = 1 + x1   
POL(minus44_in_gga(x1, x2)) = 1 + x1   
POL(minus44_out_gga(x1)) = 1 + x1   
POL(s(x1)) = 1 + x1   

The following usable rules [FROCOS05] were oriented:

minus37_in_gga(s(0), s(T18)) → minus37_out_gga(0)
minus37_in_gga(s(T19), s(0)) → minus37_out_gga(T19)
minus37_in_gga(s(s(T20)), s(s(T21))) → U5_gga(minus44_in_gga(T20, T21))
minus44_in_gga(0, T18) → minus44_out_gga(0)
minus44_in_gga(T19, 0) → minus44_out_gga(T19)
minus44_in_gga(s(T20), s(T21)) → U4_gga(minus44_in_gga(T20, T21))
U5_gga(minus44_out_gga(X47)) → minus37_out_gga(X47)
U4_gga(minus44_out_gga(X47)) → minus44_out_gga(X47)

(22) Obligation:

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

DIV1_IN_GGA(T12, T14) → U2_GGA(T14, minus37_in_gga(T12, T14))

The TRS R consists of the following rules:

minus37_in_gga(s(0), s(T18)) → minus37_out_gga(0)
minus37_in_gga(s(T19), s(0)) → minus37_out_gga(T19)
minus37_in_gga(s(s(T20)), s(s(T21))) → U5_gga(minus44_in_gga(T20, T21))
U5_gga(minus44_out_gga(X47)) → minus37_out_gga(X47)
minus44_in_gga(0, T18) → minus44_out_gga(0)
minus44_in_gga(T19, 0) → minus44_out_gga(T19)
minus44_in_gga(s(T20), s(T21)) → U4_gga(minus44_in_gga(T20, T21))
U4_gga(minus44_out_gga(X47)) → minus44_out_gga(X47)

The set Q consists of the following terms:

minus37_in_gga(x0, x1)
U5_gga(x0)
minus44_in_gga(x0, x1)
U4_gga(x0)

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

(23) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(24) TRUE