Left Termination proof of /tmp/tmp1w0CsY/short1.pl

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

0 Prolog

↳1 PrologToPrologProblemTransformerProof (⇐)

↳2 Prolog

↳3 PrologToPiTRSProof (⇐)

↳4 PiTRS

↳5 DependencyPairsProof (⇔)

↳6 PiDP

↳7 DependencyGraphProof (⇔)

↳8 TRUE

(0) Obligation:

Clauses:

p(X, Y, Z) :- ','(=(X, Y), ','(=(Z, 1), !)).
p(X, Y, Z) :- ','(=(Z, 1), ','(=(Y, X), p(X, Y, Z))).
=(X, X).

Queries:

p(a,a,a).

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: p(T1, T2, T3)\n\n", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: p(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | p(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | ?_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: ','(=(T7, T8), ','(=(T9, 1), !_1)) | p(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | ?_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: ','(=(T7, T8), ','(=(T9, 1), !_1)), SCOPE: 2, CLAUSE: 2 | p(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | ?_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: ','(=(T11, 1), !_1) | p(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | ?_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: p(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nX8 is free", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: ','(=(T11, 1), !_1), SCOPE: 3, CLAUSE: 2 | p(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | ?_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: !_1 | p(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | ?_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: p(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nX10 is free", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: ','(=(T16, 1), ','(=(T17, T18), p(T18, T17, T16)))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(=(T16, 1), ','(=(T17, T18), p(T18, T17, T16))), SCOPE: 4, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: ','(=(T20, T21), p(T21, T20, 1))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: \n\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: ','(=(T20, T21), p(T21, T20, 1)), SCOPE: 5, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: p(T23, T23, 1)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: \n\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: p(T23, T23, 1), SCOPE: 6, CLAUSE: 0 | p(T23, T23, 1), SCOPE: 6, CLAUSE: 1 | ?_6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: ','(=(T25, T25), ','(=(1, 1), !_6)) | p(T23, T23, 1), SCOPE: 6, CLAUSE: 1 | ?_6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: ','(=(T25, T25), ','(=(1, 1), !_6)), SCOPE: 7, CLAUSE: 2 | p(T23, T23, 1), SCOPE: 6, CLAUSE: 1 | ?_6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: ','(=(1, 1), !_6) | p(T23, T23, 1), SCOPE: 6, CLAUSE: 1 | ?_6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: ','(=(1, 1), !_6), SCOPE: 8, CLAUSE: 2 | p(T23, T23, 1), SCOPE: 6, CLAUSE: 1 | ?_6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: !_6 | p(T23, T23, 1), SCOPE: 6, CLAUSE: 1 | ?_6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 27 [arrowhead = none ];
27 -> 2;

28 [label="EVAL with clause\np(X4, X5, X6) :- ','(=(X4, X5), ','(=(X6, 1), !)).\nand substitution\nT1 -> T7\nX4 -> T7\nT2 -> T8\nX5 -> T8\nT3 -> T9\nX6 -> T9\nT4 -> T7\nT5 -> T8\nT6 -> T9", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 28 [arrowhead = none ];
28 -> 3;

29 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 29 [arrowhead = none ];
29 -> 4;

30 [label="EVAL with clause\n=(X8, X8).\nand substitution\nT7 -> T10\nX8 -> T10\nT8 -> T10\nT9 -> T11", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 30 [arrowhead = none ];
30 -> 5;

31 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 31 [arrowhead = none ];
31 -> 6;

32 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
5 -> 32 [arrowhead = none ];
32 -> 7;

33 [label="EVAL with clause\np(X17, X18, X19) :- ','(=(X19, 1), ','(=(X18, X17), p(X17, X18, X19))).\nand substitution\nT1 -> T18\nX17 -> T18\nT2 -> T17\nX18 -> T17\nT3 -> T16\nX19 -> T16\nT15 -> T16\nT14 -> T17\nT13 -> T18", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 33 [arrowhead = none ];
33 -> 12;

34 [label="EVAL with clause\n=(X10, X10).\nand substitution\nT11 -> 1\nX10 -> 1\nT12 -> 1", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 34 [arrowhead = none ];
34 -> 8;

35 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 35 [arrowhead = none ];
35 -> 9;

36 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
8 -> 36 [arrowhead = none ];
36 -> 10;

37 [label="INSTANCE with matching:\nX8 -> X10", fontsize=14, style = filled, fillcolor = lightgrey];
9 -> 37 [arrowhead = none , style=dashed];
37 -> 6[style=dashed];

38 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
10 -> 38 [arrowhead = none ];
38 -> 11;

39 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
12 -> 39 [arrowhead = none ];
39 -> 13;

40 [label="EVAL with clause\n=(X21, X21).\nand substitution\nT16 -> 1\nX21 -> 1\nT19 -> 1\nT17 -> T20\nT18 -> T21", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 40 [arrowhead = none ];
40 -> 14;

41 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 41 [arrowhead = none ];
41 -> 15;

42 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
14 -> 42 [arrowhead = none ];
42 -> 16;

43 [label="EVAL with clause\n=(X23, X23).\nand substitution\nT20 -> T23\nX23 -> T23\nT21 -> T23\nT22 -> T23", fontsize=14, style = filled, fillcolor = lightblue];
16 -> 43 [arrowhead = none ];
43 -> 17;

44 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
16 -> 44 [arrowhead = none ];
44 -> 18;

45 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
17 -> 45 [arrowhead = none ];
45 -> 19;

46 [label="EVAL with clause\np(X27, X28, X29) :- ','(=(X27, X28), ','(=(X29, 1), !)).\nand substitution\nT23 -> T25\nX27 -> T25\nX28 -> T25\nX29 -> 1\nT24 -> T25", fontsize=14, style = filled, fillcolor = lightblue];
19 -> 46 [arrowhead = none ];
46 -> 20;

47 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
20 -> 47 [arrowhead = none ];
47 -> 21;

48 [label="EVAL with clause\n=(X31, X31).\nand substitution\nT25 -> T26\nX31 -> T26", fontsize=14, style = filled, fillcolor = lightblue];
21 -> 48 [arrowhead = none ];
48 -> 22;

49 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
22 -> 49 [arrowhead = none ];
49 -> 23;

50 [label="EVAL with clause\n=(X33, X33).\nand substitution\nX33 -> 1", fontsize=14, style = filled, fillcolor = lightblue];
23 -> 50 [arrowhead = none ];
50 -> 24;

51 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
24 -> 51 [arrowhead = none ];
51 -> 25;

52 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
25 -> 52 [arrowhead = none ];
52 -> 26;

}

(2) Obligation:

Clauses:

p6(T26, T26, 1).
p1(T10, T10, 1).
p1(T1, T2, T3) :- p6(T1, T2, T3).
p1(T26, T26, 1).

Queries:

p1(a,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:
p1_in: (f,f,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

p1_in_aaa(T10, T10, 1) → p1_out_aaa(T10, T10, 1)
p1_in_aaa(T1, T2, T3) → U1_aaa(T1, T2, T3, p6_in_aaa(T1, T2, T3))
p6_in_aaa(T26, T26, 1) → p6_out_aaa(T26, T26, 1)
U1_aaa(T1, T2, T3, p6_out_aaa(T1, T2, T3)) → p1_out_aaa(T1, T2, T3)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

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

p1_in_aaa(T10, T10, 1) → p1_out_aaa(T10, T10, 1)
p1_in_aaa(T1, T2, T3) → U1_aaa(T1, T2, T3, p6_in_aaa(T1, T2, T3))
p6_in_aaa(T26, T26, 1) → p6_out_aaa(T26, T26, 1)
U1_aaa(T1, T2, T3, p6_out_aaa(T1, T2, T3)) → p1_out_aaa(T1, T2, T3)

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

P1_IN_AAA(T1, T2, T3) → U1_AAA(T1, T2, T3, p6_in_aaa(T1, T2, T3))
P1_IN_AAA(T1, T2, T3) → P6_IN_AAA(T1, T2, T3)

The TRS R consists of the following rules:

p1_in_aaa(T10, T10, 1) → p1_out_aaa(T10, T10, 1)
p1_in_aaa(T1, T2, T3) → U1_aaa(T1, T2, T3, p6_in_aaa(T1, T2, T3))
p6_in_aaa(T26, T26, 1) → p6_out_aaa(T26, T26, 1)
U1_aaa(T1, T2, T3, p6_out_aaa(T1, T2, T3)) → p1_out_aaa(T1, T2, T3)

The argument filtering Pi contains the following mapping:
p1_in_aaa(x1, x2, x3) = p1_in_aaa
p1_out_aaa(x1, x2, x3) = p1_out_aaa(x3)
U1_aaa(x1, x2, x3, x4) = U1_aaa(x4)
p6_in_aaa(x1, x2, x3) = p6_in_aaa
p6_out_aaa(x1, x2, x3) = p6_out_aaa(x3)
P1_IN_AAA(x1, x2, x3) = P1_IN_AAA
U1_AAA(x1, x2, x3, x4) = U1_AAA(x4)
P6_IN_AAA(x1, x2, x3) = P6_IN_AAA

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

(6) Obligation:

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

P1_IN_AAA(T1, T2, T3) → U1_AAA(T1, T2, T3, p6_in_aaa(T1, T2, T3))
P1_IN_AAA(T1, T2, T3) → P6_IN_AAA(T1, T2, T3)

The TRS R consists of the following rules:

p1_in_aaa(T10, T10, 1) → p1_out_aaa(T10, T10, 1)
p1_in_aaa(T1, T2, T3) → U1_aaa(T1, T2, T3, p6_in_aaa(T1, T2, T3))
p6_in_aaa(T26, T26, 1) → p6_out_aaa(T26, T26, 1)
U1_aaa(T1, T2, T3, p6_out_aaa(T1, T2, T3)) → p1_out_aaa(T1, T2, T3)

(7) DependencyGraphProof (EQUIVALENT transformation)

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

(0) Obligation:

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

(2) Obligation:

(3) PrologToPiTRSProof (SOUND transformation)

(4) Obligation:

(5) DependencyPairsProof (EQUIVALENT transformation)

(6) Obligation:

(7) DependencyGraphProof (EQUIVALENT transformation)

(8) TRUE