Left Termination proof of /tmp/tmpRVKVl1/fold1.pl

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

0 Prolog

↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 51 ms)

↳2 PiTRS

↳3 DependencyPairsProof (⇔, 0 ms)

↳4 PiDP

↳5 PisEmptyProof (⇔, 0 ms)

↳6 YES

(0) Obligation:

Clauses:

fold(X, [], Z) :- ','(!, eq(X, Z)).
fold(X, Y, Z) :- ','(head(Y, H), ','(tail(Y, T), ','(myop(X, H, V), fold(V, T, Z)))).
myop(a, b, c).
head([], X1).
head(.(H, X2), H).
tail([], []).
tail(.(X3, T), T).
eq(X, X).

Query: fold(g,g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
3 [label="A: fold(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
5 [label="5: fold(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | fold(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: ','(!_1, eq(T6, T8)) | fold(T6, [], T3), SCOPE: 1, CLAUSE: 1\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: fold(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nT2 is ground\nX6 is free\nX7 is free\nfold(T1, T2, T3) !=? fold(X6, [], X7)", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: eq(T6, T8)\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: eq(T6, T8), SCOPE: 2, CLAUSE: 7\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: ','(head(T16, X17), ','(tail(T16, X18), ','(myop(T15, X17, X19), fold(X19, X18, T18))))\n\nT15 is ground\nT16 is ground\nX6 is free\nX7 is free\nX17 is free\nX18 is free\nX19 is free\nfold(T15, T16, T3) !=? fold(X6, [], X7)", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: ','(head(T16, X17), ','(tail(T16, X18), ','(myop(T15, X17, X19), fold(X19, X18, T18)))), SCOPE: 3, CLAUSE: 3 | ','(head(T16, X17), ','(tail(T16, X18), ','(myop(T15, X17, X19), fold(X19, X18, T18)))), SCOPE: 3, CLAUSE: 4\n\nT15 is ground\nT16 is ground\nX6 is free\nX7 is free\nX17 is free\nX18 is free\nX19 is free\nfold(T15, T16, T3) !=? fold(X6, [], X7)", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: ','(head(T16, X17), ','(tail(T16, X18), ','(myop(T15, X17, X19), fold(X19, X18, T18)))), SCOPE: 3, CLAUSE: 4\n\nT15 is ground\nT16 is ground\nX6 is free\nX7 is free\nX17 is free\nX18 is free\nX19 is free\nfold(T15, T16, T3) !=? fold(X6, [], X7)", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: ','(tail(.(T23, T24), X18), ','(myop(T15, T23, X19), fold(X19, X18, T18)))\n\nT15 is ground\nT23 is ground\nT24 is ground\nX18 is free\nX19 is free", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: ','(tail(.(T23, T24), X18), ','(myop(T15, T23, X19), fold(X19, X18, T18))), SCOPE: 4, CLAUSE: 5 | ','(tail(.(T23, T24), X18), ','(myop(T15, T23, X19), fold(X19, X18, T18))), SCOPE: 4, CLAUSE: 6\n\nT15 is ground\nT23 is ground\nT24 is ground\nX18 is free\nX19 is free", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: ','(tail(.(T23, T24), X18), ','(myop(T15, T23, X19), fold(X19, X18, T18))), SCOPE: 4, CLAUSE: 6\n\nT15 is ground\nT23 is ground\nT24 is ground\nX18 is free\nX19 is free", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: ','(myop(T15, T31, X19), fold(X19, T32, T18))\n\nT15 is ground\nT31 is ground\nT32 is ground\nX19 is free", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: ','(myop(T15, T31, X19), fold(X19, T32, T18)), SCOPE: 5, CLAUSE: 2\n\nT15 is ground\nT31 is ground\nT32 is ground\nX19 is free", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: fold(c, T32, T18)\n\nT32 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: fold(c, T32, T18), SCOPE: 6, CLAUSE: 0 | fold(c, T32, T18), SCOPE: 6, CLAUSE: 1\n\nT32 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: ','(!_6, eq(c, T38)) | fold(c, [], T18), SCOPE: 6, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: fold(c, T32, T18), SCOPE: 6, CLAUSE: 1\n\nT32 is ground\nX49 is free\nX50 is free\nfold(c, T32, T18) !=? fold(X49, [], X50)", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: eq(c, T38)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: eq(c, T38), SCOPE: 7, CLAUSE: 7\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: ','(head(T45, X69), ','(tail(T45, X70), ','(myop(c, X69, X71), fold(X71, X70, T47))))\n\nT45 is ground\nX49 is free\nX50 is free\nX69 is free\nX70 is free\nX71 is free\nfold(c, T45, T18) !=? fold(X49, [], X50)", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: ','(head(T45, X69), ','(tail(T45, X70), ','(myop(c, X69, X71), fold(X71, X70, T47)))), SCOPE: 8, CLAUSE: 3 | ','(head(T45, X69), ','(tail(T45, X70), ','(myop(c, X69, X71), fold(X71, X70, T47)))), SCOPE: 8, CLAUSE: 4\n\nT45 is ground\nX49 is free\nX50 is free\nX69 is free\nX70 is free\nX71 is free\nfold(c, T45, T18) !=? fold(X49, [], X50)", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: ','(head(T45, X69), ','(tail(T45, X70), ','(myop(c, X69, X71), fold(X71, X70, T47)))), SCOPE: 8, CLAUSE: 4\n\nT45 is ground\nX49 is free\nX50 is free\nX69 is free\nX70 is free\nX71 is free\nfold(c, T45, T18) !=? fold(X49, [], X50)", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: ','(tail(.(T53, T54), X70), ','(myop(c, T53, X71), fold(X71, X70, T47)))\n\nT53 is ground\nT54 is ground\nX70 is free\nX71 is free", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: ','(tail(.(T53, T54), X70), ','(myop(c, T53, X71), fold(X71, X70, T47))), SCOPE: 9, CLAUSE: 5 | ','(tail(.(T53, T54), X70), ','(myop(c, T53, X71), fold(X71, X70, T47))), SCOPE: 9, CLAUSE: 6\n\nT53 is ground\nT54 is ground\nX70 is free\nX71 is free", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: ','(tail(.(T53, T54), X70), ','(myop(c, T53, X71), fold(X71, X70, T47))), SCOPE: 9, CLAUSE: 6\n\nT53 is ground\nT54 is ground\nX70 is free\nX71 is free", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: ','(myop(c, T61, X71), fold(X71, T62, T47))\n\nT61 is ground\nT62 is ground\nX71 is free", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: ','(myop(c, T61, X71), fold(X71, T62, T47)), SCOPE: 10, CLAUSE: 2\n\nT61 is ground\nT62 is ground\nX71 is free", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 115 [arrowhead = none ];
115 -> 5;

116 [label="EVAL with clause\nfold(X6, [], X7) :- ','(!_1, eq(X6, X7)).\nand substitutionT1 -> T6,\nX6 -> T6,\nT2 -> [],\nT3 -> T8,\nX7 -> T8,\nT7 -> T8", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 116 [arrowhead = none ];
116 -> 8;

117 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
5 -> 117 [arrowhead = none ];
117 -> 12;

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

119 [label="ONLY EVAL with clause\nfold(X14, X15, X16) :- ','(head(X15, X17), ','(tail(X15, X18), ','(myop(X14, X17, X19), fold(X19, X18, X16)))).\nand substitutionT1 -> T15,\nX14 -> T15,\nT2 -> T16,\nX15 -> T16,\nT3 -> T18,\nX16 -> T18,\nT17 -> T18", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 119 [arrowhead = none ];
119 -> 29;

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

121 [label="EVAL with clause\neq(X10, X10).\nand substitutionT6 -> T11,\nX10 -> T11,\nT8 -> T11", fontsize=14, style = filled, fillcolor = lightblue];
17 -> 121 [arrowhead = none ];
121 -> 20;

122 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
17 -> 122 [arrowhead = none ];
122 -> 24;

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

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

125 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (fold(T15, T16, T3), fold(X6, [], X7))", fontsize=14, style = filled, fillcolor = lightgreen];
33 -> 125 [arrowhead = none ];
125 -> 34;

126 [label="EVAL with clause\nhead(.(X26, X27), X26).\nand substitutionX26 -> T23,\nX27 -> T24,\nT16 -> .(T23, T24),\nX17 -> T23", fontsize=14, style = filled, fillcolor = lightblue];
34 -> 126 [arrowhead = none ];
126 -> 46;

127 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
34 -> 127 [arrowhead = none ];
127 -> 48;

128 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
46 -> 128 [arrowhead = none ];
128 -> 51;

129 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
51 -> 129 [arrowhead = none ];
129 -> 52;

130 [label="ONLY EVAL with clause\ntail(.(X38, X39), X39).\nand substitutionT23 -> T31,\nX38 -> T31,\nT24 -> T32,\nX39 -> T32,\nX18 -> T32", fontsize=14, style = filled, fillcolor = lightblue];
52 -> 130 [arrowhead = none ];
130 -> 57;

131 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
57 -> 131 [arrowhead = none ];
131 -> 59;

132 [label="EVAL with clause\nmyop(a, b, c).\nand substitutionT15 -> a,\nT31 -> b,\nX19 -> c", fontsize=14, style = filled, fillcolor = lightblue];
59 -> 132 [arrowhead = none ];
132 -> 61;

133 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
59 -> 133 [arrowhead = none ];
133 -> 62;

134 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
61 -> 134 [arrowhead = none ];
134 -> 66;

135 [label="EVAL with clause\nfold(X49, [], X50) :- ','(!_6, eq(X49, X50)).\nand substitutionX49 -> c,\nT32 -> [],\nT18 -> T38,\nX50 -> T38,\nT37 -> T38", fontsize=14, style = filled, fillcolor = lightblue];
66 -> 135 [arrowhead = none ];
135 -> 82;

136 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
66 -> 136 [arrowhead = none ];
136 -> 83;

137 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
82 -> 137 [arrowhead = none ];
137 -> 85;

138 [label="ONLY EVAL with clause\nfold(X66, X67, X68) :- ','(head(X67, X69), ','(tail(X67, X70), ','(myop(X66, X69, X71), fold(X71, X70, X68)))).\nand substitutionX66 -> c,\nT32 -> T45,\nX67 -> T45,\nT18 -> T47,\nX68 -> T47,\nT46 -> T47", fontsize=14, style = filled, fillcolor = lightblue];
83 -> 138 [arrowhead = none ];
138 -> 105;

139 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
85 -> 139 [arrowhead = none ];
139 -> 86;

140 [label="EVAL with clause\neq(X53, X53).\nand substitutionX53 -> c,\nT38 -> c", fontsize=14, style = filled, fillcolor = lightblue];
86 -> 140 [arrowhead = none ];
140 -> 88;

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

142 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
88 -> 142 [arrowhead = none ];
142 -> 91;

143 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
105 -> 143 [arrowhead = none ];
143 -> 106;

144 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (fold(c, T45, T18), fold(X49, [], X50))", fontsize=14, style = filled, fillcolor = lightgreen];
106 -> 144 [arrowhead = none ];
144 -> 107;

145 [label="EVAL with clause\nhead(.(X81, X82), X81).\nand substitutionX81 -> T53,\nX82 -> T54,\nT45 -> .(T53, T54),\nX69 -> T53", fontsize=14, style = filled, fillcolor = lightblue];
107 -> 145 [arrowhead = none ];
145 -> 108;

146 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
107 -> 146 [arrowhead = none ];
146 -> 109;

147 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
108 -> 147 [arrowhead = none ];
147 -> 110;

148 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
110 -> 148 [arrowhead = none ];
148 -> 111;

149 [label="ONLY EVAL with clause\ntail(.(X93, X94), X94).\nand substitutionT53 -> T61,\nX93 -> T61,\nT54 -> T62,\nX94 -> T62,\nX70 -> T62", fontsize=14, style = filled, fillcolor = lightblue];
111 -> 149 [arrowhead = none ];
149 -> 112;

150 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
112 -> 150 [arrowhead = none ];
150 -> 113;

151 [label="BACKTRACK\nfor clause: myop(a, b, c)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
113 -> 151 [arrowhead = none ];
151 -> 114;

}

(2) Obligation:

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

foldA_in_gga(T11, [], T11) → foldA_out_gga(T11, [], T11)
foldA_in_gga(a, .(b, []), c) → foldA_out_gga(a, .(b, []), c)

The argument filtering Pi contains the following mapping:
foldA_in_gga(x1, x2, x3) = foldA_in_gga(x1, x2)
[] = []
foldA_out_gga(x1, x2, x3) = foldA_out_gga(x1, x2, x3)
a = a
.(x1, x2) = .(x1, x2)
b = b

(3) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
P is empty.
The TRS R consists of the following rules:

foldA_in_gga(T11, [], T11) → foldA_out_gga(T11, [], T11)
foldA_in_gga(a, .(b, []), c) → foldA_out_gga(a, .(b, []), c)

(4) Obligation:

Pi DP problem:
P is empty.
The TRS R consists of the following rules:

foldA_in_gga(T11, [], T11) → foldA_out_gga(T11, [], T11)
foldA_in_gga(a, .(b, []), c) → foldA_out_gga(a, .(b, []), c)

(5) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,R,Pi) chain.

(0) Obligation:

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

(2) Obligation:

(3) DependencyPairsProof (EQUIVALENT transformation)

(4) Obligation:

(5) PisEmptyProof (EQUIVALENT transformation)

(6) YES