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

(0) Obligation:

Clauses:

p(a, b).
p(b, c).
tc(X, X).
tc(X, Y) :- ','(p(X, Z), tc(Z, Y)).

Query: tc(g,a)

(1) PrologToTRSTransformerProof (SOUND transformation)

Transformed Prolog program to TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
3 [label="3: tc(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
6 [label="6: tc(T1, T2), SCOPE: 1, CLAUSE: 2 | tc(T1, T2), SCOPE: 1, CLAUSE: 3\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: tc(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: tc(T1, T2), SCOPE: 1, CLAUSE: 3\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: ','(p(T14, X15), tc(X15, T16))\n\nT14 is ground\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: ','(p(T14, X15), tc(X15, T16)), SCOPE: 2, CLAUSE: 0 | ','(p(T14, X15), tc(X15, T16)), SCOPE: 2, CLAUSE: 1\n\nT14 is ground\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: ','(p(T14, X15), tc(X15, T16)), SCOPE: 2, CLAUSE: 0\n\nT14 is ground\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: ','(p(T14, X15), tc(X15, T16)), SCOPE: 2, CLAUSE: 1\n\nT14 is ground\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: tc(b, T16)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: tc(b, T16), SCOPE: 3, CLAUSE: 2 | tc(b, T16), SCOPE: 3, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: tc(b, T16), SCOPE: 3, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: tc(b, T16), SCOPE: 3, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: ','(p(b, X34), tc(X34, T23))\n\nX34 is free", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: ','(p(b, X34), tc(X34, T23)), SCOPE: 4, CLAUSE: 0 | ','(p(b, X34), tc(X34, T23)), SCOPE: 4, CLAUSE: 1\n\nX34 is free", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: ','(p(b, X34), tc(X34, T23)), SCOPE: 4, CLAUSE: 1\n\nX34 is free", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: tc(c, T23)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: tc(c, T23), SCOPE: 5, CLAUSE: 2 | tc(c, T23), SCOPE: 5, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: tc(c, T23), SCOPE: 5, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: tc(c, T23), SCOPE: 5, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: ','(p(c, X55), tc(X55, T30))\n\nX55 is free", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: ','(p(c, X55), tc(X55, T30)), SCOPE: 6, CLAUSE: 0 | ','(p(c, X55), tc(X55, T30)), SCOPE: 6, CLAUSE: 1\n\nX55 is free", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: ','(p(c, X55), tc(X55, T30)), SCOPE: 6, CLAUSE: 1\n\nX55 is free", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: tc(c, T16)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 102 [arrowhead = none ];
102 -> 6;

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

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

105 [label="EVAL with clause\ntc(X5, X5).\nand substitutionT1 -> T7,\nX5 -> T7,\nT2 -> T7", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 105 [arrowhead = none ];
105 -> 15;

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

107 [label="ONLY EVAL with clause\ntc(X13, X14) :- ','(p(X13, X15), tc(X15, X14)).\nand substitutionT1 -> T14,\nX13 -> T14,\nT2 -> T16,\nX14 -> T16,\nT15 -> T16", fontsize=14, style = filled, fillcolor = lightblue];
8 -> 107 [arrowhead = none ];
107 -> 23;

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

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

110 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
27 -> 110 [arrowhead = none ];
110 -> 29;

111 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
27 -> 111 [arrowhead = none ];
111 -> 31;

112 [label="EVAL with clause\np(a, b).\nand substitutionT14 -> a,\nX15 -> b", fontsize=14, style = filled, fillcolor = lightblue];
29 -> 112 [arrowhead = none ];
112 -> 32;

113 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
29 -> 113 [arrowhead = none ];
113 -> 35;

114 [label="EVAL with clause\np(b, c).\nand substitutionT14 -> b,\nX15 -> c", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 114 [arrowhead = none ];
114 -> 100;

115 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
31 -> 115 [arrowhead = none ];
115 -> 101;

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

117 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
42 -> 117 [arrowhead = none ];
117 -> 44;

118 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
42 -> 118 [arrowhead = none ];
118 -> 45;

119 [label="EVAL with clause\ntc(X24, X24).\nand substitutionX24 -> b,\nT16 -> b", fontsize=14, style = filled, fillcolor = lightblue];
44 -> 119 [arrowhead = none ];
119 -> 48;

120 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
44 -> 120 [arrowhead = none ];
120 -> 49;

121 [label="ONLY EVAL with clause\ntc(X32, X33) :- ','(p(X32, X34), tc(X34, X33)).\nand substitutionX32 -> b,\nT16 -> T23,\nX33 -> T23,\nT22 -> T23", fontsize=14, style = filled, fillcolor = lightblue];
45 -> 121 [arrowhead = none ];
121 -> 72;

122 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
48 -> 122 [arrowhead = none ];
122 -> 50;

123 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
72 -> 123 [arrowhead = none ];
123 -> 73;

124 [label="BACKTRACK\nfor clause: p(a, b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
73 -> 124 [arrowhead = none ];
124 -> 74;

125 [label="ONLY EVAL with clause\np(b, c).\nand substitutionX34 -> c", fontsize=14, style = filled, fillcolor = lightblue];
74 -> 125 [arrowhead = none ];
125 -> 75;

126 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
75 -> 126 [arrowhead = none ];
126 -> 79;

127 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
79 -> 127 [arrowhead = none ];
127 -> 80;

128 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
79 -> 128 [arrowhead = none ];
128 -> 81;

129 [label="EVAL with clause\ntc(X45, X45).\nand substitutionX45 -> c,\nT23 -> c", fontsize=14, style = filled, fillcolor = lightblue];
80 -> 129 [arrowhead = none ];
129 -> 85;

130 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
80 -> 130 [arrowhead = none ];
130 -> 86;

131 [label="ONLY EVAL with clause\ntc(X53, X54) :- ','(p(X53, X55), tc(X55, X54)).\nand substitutionX53 -> c,\nT23 -> T30,\nX54 -> T30,\nT29 -> T30", fontsize=14, style = filled, fillcolor = lightblue];
81 -> 131 [arrowhead = none ];
131 -> 96;

132 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
85 -> 132 [arrowhead = none ];
132 -> 87;

133 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
96 -> 133 [arrowhead = none ];
133 -> 97;

134 [label="BACKTRACK\nfor clause: p(a, b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
97 -> 134 [arrowhead = none ];
134 -> 98;

135 [label="BACKTRACK\nfor clause: p(b, c)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
98 -> 135 [arrowhead = none ];
135 -> 99;

136 [label="INSTANCE with matching:\nT23 -> T16", fontsize=14, style = filled, fillcolor = lightgrey];
100 -> 136 [arrowhead = none , style=dashed];
136 -> 75[style=dashed];

}

(2) Obligation:

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

f3_in(T7) → f3_out1(T7)
f3_in(a) → f3_out1(b)
f3_in(a) → U1(f75_in, a)
U1(f75_out1(T23), a) → f3_out1(T23)
f3_in(b) → U2(f75_in, b)
U2(f75_out1(T16), b) → f3_out1(T16)
f75_in → f75_out1(c)

Q is empty.

(3) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Knuth-Bendix order [KBO] with precedence:

b > a > c > f3_in1 > U1₂ > f75_out11 > U2₂ > f75_in > f3_out11

and weight map:

a=2
b=2
f75_in=3
c=1
f3_in_1=3
f3_out1_1=3
f75_out1_1=1
U1_2=0
U2_2=0

The variable weight is 1With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

f3_in(T7) → f3_out1(T7)
f3_in(a) → f3_out1(b)
f3_in(a) → U1(f75_in, a)
U1(f75_out1(T23), a) → f3_out1(T23)
f3_in(b) → U2(f75_in, b)
U2(f75_out1(T16), b) → f3_out1(T16)
f75_in → f75_out1(c)

(4) Obligation:

Q restricted rewrite system:
R is empty.
Q is empty.

(5) RisEmptyProof (EQUIVALENT transformation)

The TRS R is empty. Hence, termination is trivially proven.

(6) YES