Left Termination proof of /tmp/tmpUeMlUY/star2.pl

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

0 Prolog

↳1 PrologToTRSTransformerProof (⇒, 79 ms)

↳2 QTRS

↳3 Overlay + Local Confluence (⇔, 0 ms)

↳4 QTRS

↳5 DependencyPairsProof (⇔, 0 ms)

↳6 QDP

↳7 DependencyGraphProof (⇔, 0 ms)

↳8 AND

    ↳9 QDP

        ↳10 UsableRulesProof (⇔, 0 ms)

        ↳11 QDP

        ↳12 QReductionProof (⇔, 0 ms)

        ↳13 QDP

        ↳14 QDPSizeChangeProof (⇔, 0 ms)

        ↳15 YES

    ↳16 QDP

        ↳17 UsableRulesProof (⇔, 0 ms)

        ↳18 QDP

        ↳19 QReductionProof (⇔, 0 ms)

        ↳20 QDP

        ↳21 QDPSizeChangeProof (⇔, 0 ms)

        ↳22 YES

(0) Obligation:

Clauses:

star(X1, []).
star(.(X, U), .(X, W)) :- ','(app(U, V, W), star(.(X, U), W)).
app([], L, L).
app(.(X, L), M, .(X, N)) :- app(L, M, N).

Query: star(g,g)

(1) PrologToTRSTransformerProof (SOUND transformation)

Transformed Prolog program to TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: star(T1, T2)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: star(T1, T2), SCOPE: 1, CLAUSE: 0 | star(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: star(T1, T2), SCOPE: 1, CLAUSE: 0\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: star(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: ','(app(T15, X17, T16), star(.(T14, T15), T16))\n\nT14 is ground\nT15 is ground\nT16 is ground\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: app(T15, X17, T16)\n\nT15 is ground\nT16 is ground\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: star(.(T14, T15), T16)\n\nT14 is ground\nT15 is ground\nT16 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: app(T15, X17, T16), SCOPE: 2, CLAUSE: 2 | app(T15, X17, T16), SCOPE: 2, CLAUSE: 3\n\nT15 is ground\nT16 is ground\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: app(T15, X17, T16), SCOPE: 2, CLAUSE: 2\n\nT15 is ground\nT16 is ground\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: app(T15, X17, T16), SCOPE: 2, CLAUSE: 3\n\nT15 is ground\nT16 is ground\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: app(T34, X50, T35)\n\nT34 is ground\nT35 is ground\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 52 [arrowhead = none ];
52 -> 4;

53 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
4 -> 53 [arrowhead = none ];
53 -> 7;

54 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
4 -> 54 [arrowhead = none ];
54 -> 8;

55 [label="EVAL with clause\nstar(X6, []).\nand substitutionT1 -> T7,\nX6 -> T7,\nT2 -> []", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 55 [arrowhead = none ];
55 -> 13;

56 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
7 -> 56 [arrowhead = none ];
56 -> 14;

57 [label="EVAL with clause\nstar(.(X14, X15), .(X14, X16)) :- ','(app(X15, X17, X16), star(.(X14, X15), X16)).\nand substitutionX14 -> T14,\nX15 -> T15,\nT1 -> .(T14, T15),\nX16 -> T16,\nT2 -> .(T14, T16)", fontsize=14, style = filled, fillcolor = lightblue];
8 -> 57 [arrowhead = none ];
57 -> 20;

58 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
8 -> 58 [arrowhead = none ];
58 -> 21;

59 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
13 -> 59 [arrowhead = none ];
59 -> 15;

60 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
20 -> 60 [arrowhead = none ];
60 -> 36;

61 [label="SPLIT 2\nnew knowledge:\nT15 is ground\nT19 is ground\nT16 is ground\nreplacements:X17 -> T19", fontsize=14, style = filled, fillcolor = violet];
20 -> 61 [arrowhead = none ];
61 -> 37;

62 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
36 -> 62 [arrowhead = none ];
62 -> 38;

63 [label="INSTANCE with matching:\nT1 -> .(T14, T15)\nT2 -> T16", fontsize=14, style = filled, fillcolor = lightgrey];
37 -> 63 [arrowhead = none , style=dashed];
63 -> 1[style=dashed];

64 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
38 -> 64 [arrowhead = none ];
64 -> 39;

65 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
38 -> 65 [arrowhead = none ];
65 -> 40;

66 [label="EVAL with clause\napp([], X34, X34).\nand substitutionT15 -> [],\nX17 -> T26,\nX34 -> T26,\nT16 -> T26,\nX35 -> T26", fontsize=14, style = filled, fillcolor = lightblue];
39 -> 66 [arrowhead = none ];
66 -> 41;

67 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
39 -> 67 [arrowhead = none ];
67 -> 43;

68 [label="EVAL with clause\napp(.(X46, X47), X48, .(X46, X49)) :- app(X47, X48, X49).\nand substitutionX46 -> T33,\nX47 -> T34,\nT15 -> .(T33, T34),\nX17 -> X50,\nX48 -> X50,\nX49 -> T35,\nT16 -> .(T33, T35)", fontsize=14, style = filled, fillcolor = lightblue];
40 -> 68 [arrowhead = none ];
68 -> 50;

69 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
40 -> 69 [arrowhead = none ];
69 -> 51;

70 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
41 -> 70 [arrowhead = none ];
70 -> 44;

71 [label="INSTANCE with matching:\nT15 -> T34\nX17 -> X50\nT16 -> T35", fontsize=14, style = filled, fillcolor = lightgrey];
50 -> 71 [arrowhead = none , style=dashed];
71 -> 36[style=dashed];

}

(2) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

f1_in(T7, []) → f1_out1
f1_in(.(T14, T15), .(T14, T16)) → U1(f20_in(T15, T16, T14), .(T14, T15), .(T14, T16))
U1(f20_out1(X17), .(T14, T15), .(T14, T16)) → f1_out1
f36_in([], T26) → f36_out1(T26)
f36_in(.(T33, T34), .(T33, T35)) → U2(f36_in(T34, T35), .(T33, T34), .(T33, T35))
U2(f36_out1(X50), .(T33, T34), .(T33, T35)) → f36_out1(X50)
f20_in(T15, T16, T14) → U3(f36_in(T15, T16), T15, T16, T14)
U3(f36_out1(T19), T15, T16, T14) → U4(f1_in(.(T14, T15), T16), T15, T16, T14, T19)
U4(f1_out1, T15, T16, T14, T19) → f20_out1(T19)

Q is empty.

(3) Overlay + Local Confluence (EQUIVALENT transformation)

The TRS is overlay and locally confluent. By [NOC] we can switch to innermost.

(4) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

f1_in(T7, []) → f1_out1
f1_in(.(T14, T15), .(T14, T16)) → U1(f20_in(T15, T16, T14), .(T14, T15), .(T14, T16))
U1(f20_out1(X17), .(T14, T15), .(T14, T16)) → f1_out1
f36_in([], T26) → f36_out1(T26)
f36_in(.(T33, T34), .(T33, T35)) → U2(f36_in(T34, T35), .(T33, T34), .(T33, T35))
U2(f36_out1(X50), .(T33, T34), .(T33, T35)) → f36_out1(X50)
f20_in(T15, T16, T14) → U3(f36_in(T15, T16), T15, T16, T14)
U3(f36_out1(T19), T15, T16, T14) → U4(f1_in(.(T14, T15), T16), T15, T16, T14, T19)
U4(f1_out1, T15, T16, T14, T19) → f20_out1(T19)

The set Q consists of the following terms:

f1_in(x0, [])
f1_in(.(x0, x1), .(x0, x2))
U1(f20_out1(x0), .(x1, x2), .(x1, x3))
f36_in([], x0)
f36_in(.(x0, x1), .(x0, x2))
U2(f36_out1(x0), .(x1, x2), .(x1, x3))
f20_in(x0, x1, x2)
U3(f36_out1(x0), x1, x2, x3)
U4(f1_out1, x0, x1, x2, x3)

(5) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(6) Obligation:

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

F1_IN(.(T14, T15), .(T14, T16)) → U1¹(f20_in(T15, T16, T14), .(T14, T15), .(T14, T16))
F1_IN(.(T14, T15), .(T14, T16)) → F20_IN(T15, T16, T14)
F36_IN(.(T33, T34), .(T33, T35)) → U2¹(f36_in(T34, T35), .(T33, T34), .(T33, T35))
F36_IN(.(T33, T34), .(T33, T35)) → F36_IN(T34, T35)
F20_IN(T15, T16, T14) → U3¹(f36_in(T15, T16), T15, T16, T14)
F20_IN(T15, T16, T14) → F36_IN(T15, T16)
U3¹(f36_out1(T19), T15, T16, T14) → U4¹(f1_in(.(T14, T15), T16), T15, T16, T14, T19)
U3¹(f36_out1(T19), T15, T16, T14) → F1_IN(.(T14, T15), T16)

The TRS R consists of the following rules:

f1_in(T7, []) → f1_out1
f1_in(.(T14, T15), .(T14, T16)) → U1(f20_in(T15, T16, T14), .(T14, T15), .(T14, T16))
U1(f20_out1(X17), .(T14, T15), .(T14, T16)) → f1_out1
f36_in([], T26) → f36_out1(T26)
f36_in(.(T33, T34), .(T33, T35)) → U2(f36_in(T34, T35), .(T33, T34), .(T33, T35))
U2(f36_out1(X50), .(T33, T34), .(T33, T35)) → f36_out1(X50)
f20_in(T15, T16, T14) → U3(f36_in(T15, T16), T15, T16, T14)
U3(f36_out1(T19), T15, T16, T14) → U4(f1_in(.(T14, T15), T16), T15, T16, T14, T19)
U4(f1_out1, T15, T16, T14, T19) → f20_out1(T19)

The set Q consists of the following terms:

f1_in(x0, [])
f1_in(.(x0, x1), .(x0, x2))
U1(f20_out1(x0), .(x1, x2), .(x1, x3))
f36_in([], x0)
f36_in(.(x0, x1), .(x0, x2))
U2(f36_out1(x0), .(x1, x2), .(x1, x3))
f20_in(x0, x1, x2)
U3(f36_out1(x0), x1, x2, x3)
U4(f1_out1, x0, x1, x2, x3)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs with 4 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

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

F36_IN(.(T33, T34), .(T33, T35)) → F36_IN(T34, T35)

The TRS R consists of the following rules:

f1_in(T7, []) → f1_out1
f1_in(.(T14, T15), .(T14, T16)) → U1(f20_in(T15, T16, T14), .(T14, T15), .(T14, T16))
U1(f20_out1(X17), .(T14, T15), .(T14, T16)) → f1_out1
f36_in([], T26) → f36_out1(T26)
f36_in(.(T33, T34), .(T33, T35)) → U2(f36_in(T34, T35), .(T33, T34), .(T33, T35))
U2(f36_out1(X50), .(T33, T34), .(T33, T35)) → f36_out1(X50)
f20_in(T15, T16, T14) → U3(f36_in(T15, T16), T15, T16, T14)
U3(f36_out1(T19), T15, T16, T14) → U4(f1_in(.(T14, T15), T16), T15, T16, T14, T19)
U4(f1_out1, T15, T16, T14, T19) → f20_out1(T19)

The set Q consists of the following terms:

f1_in(x0, [])
f1_in(.(x0, x1), .(x0, x2))
U1(f20_out1(x0), .(x1, x2), .(x1, x3))
f36_in([], x0)
f36_in(.(x0, x1), .(x0, x2))
U2(f36_out1(x0), .(x1, x2), .(x1, x3))
f20_in(x0, x1, x2)
U3(f36_out1(x0), x1, x2, x3)
U4(f1_out1, x0, x1, x2, x3)

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

(10) 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.

(11) Obligation:

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

F36_IN(.(T33, T34), .(T33, T35)) → F36_IN(T34, T35)

R is empty.
The set Q consists of the following terms:

f1_in(x0, [])
f1_in(.(x0, x1), .(x0, x2))
U1(f20_out1(x0), .(x1, x2), .(x1, x3))
f36_in([], x0)
f36_in(.(x0, x1), .(x0, x2))
U2(f36_out1(x0), .(x1, x2), .(x1, x3))
f20_in(x0, x1, x2)
U3(f36_out1(x0), x1, x2, x3)
U4(f1_out1, x0, x1, x2, x3)

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

(12) 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].

f1_in(x0, [])
f1_in(.(x0, x1), .(x0, x2))
U1(f20_out1(x0), .(x1, x2), .(x1, x3))
f36_in([], x0)
f36_in(.(x0, x1), .(x0, x2))
U2(f36_out1(x0), .(x1, x2), .(x1, x3))
f20_in(x0, x1, x2)
U3(f36_out1(x0), x1, x2, x3)
U4(f1_out1, x0, x1, x2, x3)

(13) Obligation:

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

F36_IN(.(T33, T34), .(T33, T35)) → F36_IN(T34, T35)

R is empty.
Q is empty.
We have to consider all minimal (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:

F36_IN(.(T33, T34), .(T33, T35)) → F36_IN(T34, T35)
The graph contains the following edges 1 > 1, 2 > 2

(15) YES

(16) Obligation:

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

F1_IN(.(T14, T15), .(T14, T16)) → F20_IN(T15, T16, T14)
F20_IN(T15, T16, T14) → U3¹(f36_in(T15, T16), T15, T16, T14)
U3¹(f36_out1(T19), T15, T16, T14) → F1_IN(.(T14, T15), T16)

The TRS R consists of the following rules:

f1_in(T7, []) → f1_out1
f1_in(.(T14, T15), .(T14, T16)) → U1(f20_in(T15, T16, T14), .(T14, T15), .(T14, T16))
U1(f20_out1(X17), .(T14, T15), .(T14, T16)) → f1_out1
f36_in([], T26) → f36_out1(T26)
f36_in(.(T33, T34), .(T33, T35)) → U2(f36_in(T34, T35), .(T33, T34), .(T33, T35))
U2(f36_out1(X50), .(T33, T34), .(T33, T35)) → f36_out1(X50)
f20_in(T15, T16, T14) → U3(f36_in(T15, T16), T15, T16, T14)
U3(f36_out1(T19), T15, T16, T14) → U4(f1_in(.(T14, T15), T16), T15, T16, T14, T19)
U4(f1_out1, T15, T16, T14, T19) → f20_out1(T19)

The set Q consists of the following terms:

f1_in(x0, [])
f1_in(.(x0, x1), .(x0, x2))
U1(f20_out1(x0), .(x1, x2), .(x1, x3))
f36_in([], x0)
f36_in(.(x0, x1), .(x0, x2))
U2(f36_out1(x0), .(x1, x2), .(x1, x3))
f20_in(x0, x1, x2)
U3(f36_out1(x0), x1, x2, x3)
U4(f1_out1, x0, x1, x2, x3)

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

(17) 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.

(18) Obligation:

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

F1_IN(.(T14, T15), .(T14, T16)) → F20_IN(T15, T16, T14)
F20_IN(T15, T16, T14) → U3¹(f36_in(T15, T16), T15, T16, T14)
U3¹(f36_out1(T19), T15, T16, T14) → F1_IN(.(T14, T15), T16)

The TRS R consists of the following rules:

f36_in([], T26) → f36_out1(T26)
f36_in(.(T33, T34), .(T33, T35)) → U2(f36_in(T34, T35), .(T33, T34), .(T33, T35))
U2(f36_out1(X50), .(T33, T34), .(T33, T35)) → f36_out1(X50)

The set Q consists of the following terms:

f1_in(x0, [])
f1_in(.(x0, x1), .(x0, x2))
U1(f20_out1(x0), .(x1, x2), .(x1, x3))
f36_in([], x0)
f36_in(.(x0, x1), .(x0, x2))
U2(f36_out1(x0), .(x1, x2), .(x1, x3))
f20_in(x0, x1, x2)
U3(f36_out1(x0), x1, x2, x3)
U4(f1_out1, x0, x1, x2, x3)

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

(19) 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].

f1_in(x0, [])
f1_in(.(x0, x1), .(x0, x2))
U1(f20_out1(x0), .(x1, x2), .(x1, x3))
f20_in(x0, x1, x2)
U3(f36_out1(x0), x1, x2, x3)
U4(f1_out1, x0, x1, x2, x3)

(20) Obligation:

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

F1_IN(.(T14, T15), .(T14, T16)) → F20_IN(T15, T16, T14)
F20_IN(T15, T16, T14) → U3¹(f36_in(T15, T16), T15, T16, T14)
U3¹(f36_out1(T19), T15, T16, T14) → F1_IN(.(T14, T15), T16)

The TRS R consists of the following rules:

f36_in([], T26) → f36_out1(T26)
f36_in(.(T33, T34), .(T33, T35)) → U2(f36_in(T34, T35), .(T33, T34), .(T33, T35))
U2(f36_out1(X50), .(T33, T34), .(T33, T35)) → f36_out1(X50)

The set Q consists of the following terms:

f36_in([], x0)
f36_in(.(x0, x1), .(x0, x2))
U2(f36_out1(x0), .(x1, x2), .(x1, x3))

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

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

F20_IN(T15, T16, T14) → U3¹(f36_in(T15, T16), T15, T16, T14)
The graph contains the following edges 1 >= 2, 2 >= 3, 3 >= 4
U3¹(f36_out1(T19), T15, T16, T14) → F1_IN(.(T14, T15), T16)
The graph contains the following edges 3 >= 2
F1_IN(.(T14, T15), .(T14, T16)) → F20_IN(T15, T16, T14)
The graph contains the following edges 1 > 1, 2 > 2, 1 > 3, 2 > 3

(0) Obligation:

(1) PrologToTRSTransformerProof (SOUND transformation)

(2) Obligation:

(3) Overlay + Local Confluence (EQUIVALENT transformation)

(4) Obligation:

(5) DependencyPairsProof (EQUIVALENT transformation)

(6) Obligation:

(7) DependencyGraphProof (EQUIVALENT transformation)

(8) Complex Obligation (AND)

(9) Obligation:

(10) UsableRulesProof (EQUIVALENT transformation)

(11) Obligation:

(12) QReductionProof (EQUIVALENT transformation)

(13) Obligation:

(14) QDPSizeChangeProof (EQUIVALENT transformation)

(15) YES

(16) Obligation:

(17) UsableRulesProof (EQUIVALENT transformation)

(18) Obligation:

(19) QReductionProof (EQUIVALENT transformation)

(20) Obligation:

(21) QDPSizeChangeProof (EQUIVALENT transformation)

(22) YES