Left Termination of the query pattern div_in_4(g, g, a, a) w.r.t. the given Prolog program could successfully be proven:

0 Prolog
↳1 PrologToDTProblemTransformerProof (⇐)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇐)
↳4 PiDP
↳5 DependencyGraphProof (⇔)
↳6 AND
    ↳7 PiDP
        ↳8 UsableRulesProof (⇔)
        ↳9 PiDP
        ↳10 PiDPToQDPProof (⇐)
        ↳11 QDP
        ↳12 QDPSizeChangeProof (⇔)
        ↳13 YES
    ↳14 PiDP
        ↳15 PiDPToQDPProof (⇐)
        ↳16 QDP
        ↳17 QDPOrderProof (⇔)
        ↳18 QDP
        ↳19 DependencyGraphProof (⇔)
        ↳20 TRUE

(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) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

minus26(s(T61), s(T62), X91) :- minus26(T61, T62, X91).
div1(s(T45), s(T46), s(T34), T35) :- minus26(T45, T46, X66).
div1(s(T45), s(T46), s(T34), T35) :- ','(minusc26(T45, T46, T49), div1(T49, s(T46), T34, T35)).

Clauses:

minusc26(T56, 0, T56).
minusc26(s(T61), s(T62), X91) :- minusc26(T61, T62, X91).
divc1(0, T14, 0, 0).
divc1(s(T45), s(T46), s(T34), T35) :- ','(minusc26(T45, T46, T49), divc1(T49, s(T46), T34, T35)).
divc1(T75, T76, T77, T75).
divc1(T81, T82, T83, T81).

Afs:

div1(x1, x2, x3, x4)  =  div1(x1, x2)

(3) TriplesToPiDPProof (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,f)
minus26_in: (b,b,f)
minusc26_in: (b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

DIV1_IN_GGAA(s(T45), s(T46), s(T34), T35) → U2_GGAA(T45, T46, T34, T35, minus26_in_gga(T45, T46, X66))
DIV1_IN_GGAA(s(T45), s(T46), s(T34), T35) → MINUS26_IN_GGA(T45, T46, X66)
MINUS26_IN_GGA(s(T61), s(T62), X91) → U1_GGA(T61, T62, X91, minus26_in_gga(T61, T62, X91))
MINUS26_IN_GGA(s(T61), s(T62), X91) → MINUS26_IN_GGA(T61, T62, X91)
DIV1_IN_GGAA(s(T45), s(T46), s(T34), T35) → U3_GGAA(T45, T46, T34, T35, minusc26_in_gga(T45, T46, T49))
U3_GGAA(T45, T46, T34, T35, minusc26_out_gga(T45, T46, T49)) → U4_GGAA(T45, T46, T34, T35, div1_in_ggaa(T49, s(T46), T34, T35))
U3_GGAA(T45, T46, T34, T35, minusc26_out_gga(T45, T46, T49)) → DIV1_IN_GGAA(T49, s(T46), T34, T35)

The TRS R consists of the following rules:

minusc26_in_gga(T56, 0, T56) → minusc26_out_gga(T56, 0, T56)
minusc26_in_gga(s(T61), s(T62), X91) → U6_gga(T61, T62, X91, minusc26_in_gga(T61, T62, X91))
U6_gga(T61, T62, X91, minusc26_out_gga(T61, T62, X91)) → minusc26_out_gga(s(T61), s(T62), X91)

The argument filtering Pi contains the following mapping:
div1_in_ggaa(x1, x2, x3, x4)  =  div1_in_ggaa(x1, x2)
s(x1)  =  s(x1)
minus26_in_gga(x1, x2, x3)  =  minus26_in_gga(x1, x2)
minusc26_in_gga(x1, x2, x3)  =  minusc26_in_gga(x1, x2)
0  =  0
minusc26_out_gga(x1, x2, x3)  =  minusc26_out_gga(x1, x2, x3)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
DIV1_IN_GGAA(x1, x2, x3, x4)  =  DIV1_IN_GGAA(x1, x2)
U2_GGAA(x1, x2, x3, x4, x5)  =  U2_GGAA(x1, x2, x5)
MINUS26_IN_GGA(x1, x2, x3)  =  MINUS26_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4)  =  U1_GGA(x1, x2, x4)
U3_GGAA(x1, x2, x3, x4, x5)  =  U3_GGAA(x1, x2, x5)
U4_GGAA(x1, x2, x3, x4, x5)  =  U4_GGAA(x1, x2, x5)

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

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

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

DIV1_IN_GGAA(s(T45), s(T46), s(T34), T35) → U2_GGAA(T45, T46, T34, T35, minus26_in_gga(T45, T46, X66))
DIV1_IN_GGAA(s(T45), s(T46), s(T34), T35) → MINUS26_IN_GGA(T45, T46, X66)
MINUS26_IN_GGA(s(T61), s(T62), X91) → U1_GGA(T61, T62, X91, minus26_in_gga(T61, T62, X91))
MINUS26_IN_GGA(s(T61), s(T62), X91) → MINUS26_IN_GGA(T61, T62, X91)
DIV1_IN_GGAA(s(T45), s(T46), s(T34), T35) → U3_GGAA(T45, T46, T34, T35, minusc26_in_gga(T45, T46, T49))
U3_GGAA(T45, T46, T34, T35, minusc26_out_gga(T45, T46, T49)) → U4_GGAA(T45, T46, T34, T35, div1_in_ggaa(T49, s(T46), T34, T35))
U3_GGAA(T45, T46, T34, T35, minusc26_out_gga(T45, T46, T49)) → DIV1_IN_GGAA(T49, s(T46), T34, T35)

The TRS R consists of the following rules:

minusc26_in_gga(T56, 0, T56) → minusc26_out_gga(T56, 0, T56)
minusc26_in_gga(s(T61), s(T62), X91) → U6_gga(T61, T62, X91, minusc26_in_gga(T61, T62, X91))
U6_gga(T61, T62, X91, minusc26_out_gga(T61, T62, X91)) → minusc26_out_gga(s(T61), s(T62), X91)

The argument filtering Pi contains the following mapping:
div1_in_ggaa(x1, x2, x3, x4)  =  div1_in_ggaa(x1, x2)
s(x1)  =  s(x1)
minus26_in_gga(x1, x2, x3)  =  minus26_in_gga(x1, x2)
minusc26_in_gga(x1, x2, x3)  =  minusc26_in_gga(x1, x2)
0  =  0
minusc26_out_gga(x1, x2, x3)  =  minusc26_out_gga(x1, x2, x3)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
DIV1_IN_GGAA(x1, x2, x3, x4)  =  DIV1_IN_GGAA(x1, x2)
U2_GGAA(x1, x2, x3, x4, x5)  =  U2_GGAA(x1, x2, x5)
MINUS26_IN_GGA(x1, x2, x3)  =  MINUS26_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4)  =  U1_GGA(x1, x2, x4)
U3_GGAA(x1, x2, x3, x4, x5)  =  U3_GGAA(x1, x2, x5)
U4_GGAA(x1, x2, x3, x4, x5)  =  U4_GGAA(x1, x2, x5)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

MINUS26_IN_GGA(s(T61), s(T62), X91) → MINUS26_IN_GGA(T61, T62, X91)

The TRS R consists of the following rules:

minusc26_in_gga(T56, 0, T56) → minusc26_out_gga(T56, 0, T56)
minusc26_in_gga(s(T61), s(T62), X91) → U6_gga(T61, T62, X91, minusc26_in_gga(T61, T62, X91))
U6_gga(T61, T62, X91, minusc26_out_gga(T61, T62, X91)) → minusc26_out_gga(s(T61), s(T62), X91)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
minusc26_in_gga(x1, x2, x3)  =  minusc26_in_gga(x1, x2)
0  =  0
minusc26_out_gga(x1, x2, x3)  =  minusc26_out_gga(x1, x2, x3)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
MINUS26_IN_GGA(x1, x2, x3)  =  MINUS26_IN_GGA(x1, x2)

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

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

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

MINUS26_IN_GGA(s(T61), s(T62), X91) → MINUS26_IN_GGA(T61, T62, X91)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
MINUS26_IN_GGA(x1, x2, x3)  =  MINUS26_IN_GGA(x1, x2)

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

(10) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

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

MINUS26_IN_GGA(s(T61), s(T62)) → MINUS26_IN_GGA(T61, T62)

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

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • MINUS26_IN_GGA(s(T61), s(T62)) → MINUS26_IN_GGA(T61, T62)
    The graph contains the following edges 1 > 1, 2 > 2

(13) YES

(14) Obligation:

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

DIV1_IN_GGAA(s(T45), s(T46), s(T34), T35) → U3_GGAA(T45, T46, T34, T35, minusc26_in_gga(T45, T46, T49))
U3_GGAA(T45, T46, T34, T35, minusc26_out_gga(T45, T46, T49)) → DIV1_IN_GGAA(T49, s(T46), T34, T35)

The TRS R consists of the following rules:

minusc26_in_gga(T56, 0, T56) → minusc26_out_gga(T56, 0, T56)
minusc26_in_gga(s(T61), s(T62), X91) → U6_gga(T61, T62, X91, minusc26_in_gga(T61, T62, X91))
U6_gga(T61, T62, X91, minusc26_out_gga(T61, T62, X91)) → minusc26_out_gga(s(T61), s(T62), X91)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
minusc26_in_gga(x1, x2, x3)  =  minusc26_in_gga(x1, x2)
0  =  0
minusc26_out_gga(x1, x2, x3)  =  minusc26_out_gga(x1, x2, x3)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
DIV1_IN_GGAA(x1, x2, x3, x4)  =  DIV1_IN_GGAA(x1, x2)
U3_GGAA(x1, x2, x3, x4, x5)  =  U3_GGAA(x1, x2, x5)

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

(15) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(16) Obligation:

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

DIV1_IN_GGAA(s(T45), s(T46)) → U3_GGAA(T45, T46, minusc26_in_gga(T45, T46))
U3_GGAA(T45, T46, minusc26_out_gga(T45, T46, T49)) → DIV1_IN_GGAA(T49, s(T46))

The TRS R consists of the following rules:

minusc26_in_gga(T56, 0) → minusc26_out_gga(T56, 0, T56)
minusc26_in_gga(s(T61), s(T62)) → U6_gga(T61, T62, minusc26_in_gga(T61, T62))
U6_gga(T61, T62, minusc26_out_gga(T61, T62, X91)) → minusc26_out_gga(s(T61), s(T62), X91)

The set Q consists of the following terms:

minusc26_in_gga(x0, x1)
U6_gga(x0, x1, x2)

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

(17) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


DIV1_IN_GGAA(s(T45), s(T46)) → U3_GGAA(T45, T46, minusc26_in_gga(T45, T46))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(DIV1_IN_GGAA(x1, x2)) = x1   
POL(U3_GGAA(x1, x2, x3)) = x3   
POL(U6_gga(x1, x2, x3)) = x3   
POL(minusc26_in_gga(x1, x2)) = x1   
POL(minusc26_out_gga(x1, x2, x3)) = x3   
POL(s(x1)) = 1 + x1   

The following usable rules [FROCOS05] were oriented:

minusc26_in_gga(T56, 0) → minusc26_out_gga(T56, 0, T56)
minusc26_in_gga(s(T61), s(T62)) → U6_gga(T61, T62, minusc26_in_gga(T61, T62))
U6_gga(T61, T62, minusc26_out_gga(T61, T62, X91)) → minusc26_out_gga(s(T61), s(T62), X91)

(18) Obligation:

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

U3_GGAA(T45, T46, minusc26_out_gga(T45, T46, T49)) → DIV1_IN_GGAA(T49, s(T46))

The TRS R consists of the following rules:

minusc26_in_gga(T56, 0) → minusc26_out_gga(T56, 0, T56)
minusc26_in_gga(s(T61), s(T62)) → U6_gga(T61, T62, minusc26_in_gga(T61, T62))
U6_gga(T61, T62, minusc26_out_gga(T61, T62, X91)) → minusc26_out_gga(s(T61), s(T62), X91)

The set Q consists of the following terms:

minusc26_in_gga(x0, x1)
U6_gga(x0, x1, x2)

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

(19) DependencyGraphProof (EQUIVALENT transformation)

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

(20) TRUE