Left Termination proof of /tmp/tmp61LTN7/duplicate2.pl

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

0 Prolog

↳1 PrologToTRSTransformerProof (⇒, 75 ms)

↳2 QTRS

↳3 QTRSRRRProof (⇔, 35 ms)

↳4 QTRS

↳5 QTRSRRRProof (⇔, 19 ms)

↳6 QTRS

↳7 RisEmptyProof (⇔, 0 ms)

↳8 YES

(0) Obligation:

Clauses:

duplicate([], []).
duplicate(X, .(H, .(H, Z))) :- ','(no(empty(X)), ','(head(X, H), ','(tail(X, T), duplicate(T, Z)))).
head([], X1).
head(.(H, X2), H).
tail([], []).
tail(.(X3, T), T).
empty([]).
no(X) :- ','(X, ','(!, failure(a))).
no(X4).
failure(b).

Query: duplicate(g,a)

(1) PrologToTRSTransformerProof (SOUND transformation)

Transformed Prolog program to TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
3 [label="3: duplicate(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: duplicate(T1, T2), SCOPE: 1, CLAUSE: 0 | duplicate(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: true | duplicate([], T2), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: duplicate(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nduplicate(T1, T2) !=? duplicate([], [])", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: duplicate([], T2), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ','(no(empty([])), ','(head([], T7), ','(tail([], X11), duplicate(X11, T8))))\n\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: ','(no(empty([])), ','(head([], T7), ','(tail([], X11), duplicate(X11, T8)))), SCOPE: 2, CLAUSE: 7 | ','(no(empty([])), ','(head([], T7), ','(tail([], X11), duplicate(X11, T8)))), SCOPE: 2, CLAUSE: 8\n\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: ','(','(call(empty([])), ','(!_2, failure(a))), ','(head([], T7), ','(tail([], X11), duplicate(X11, T8)))) | ','(no(empty([])), ','(head([], T7), ','(tail([], X11), duplicate(X11, T8)))), SCOPE: 2, CLAUSE: 8\n\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: ','(empty([]), ','(','(!_2, failure(a)), ','(head([], T7), ','(tail([], X11), duplicate(X11, T8))))) | ?_3 | ','(no(empty([])), ','(head([], T7), ','(tail([], X11), duplicate(X11, T8)))), SCOPE: 2, CLAUSE: 8\n\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: ','(empty([]), ','(','(!_2, failure(a)), ','(head([], T7), ','(tail([], X11), duplicate(X11, T8))))), SCOPE: 4, CLAUSE: 6 | ?_4 | ?_3 | ','(no(empty([])), ','(head([], T7), ','(tail([], X11), duplicate(X11, T8)))), SCOPE: 2, CLAUSE: 8\n\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: ','(','(!_2, failure(a)), ','(head([], T7), ','(tail([], X11), duplicate(X11, T8)))) | ?_4 | ?_3 | ','(no(empty([])), ','(head([], T7), ','(tail([], X11), duplicate(X11, T8)))), SCOPE: 2, CLAUSE: 8\n\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: ','(failure(a), ','(head([], T7), ','(tail([], X11), duplicate(X11, T8))))\n\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: ','(failure(a), ','(head([], T7), ','(tail([], X11), duplicate(X11, T8)))), SCOPE: 5, CLAUSE: 9\n\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: ','(no(empty(T12)), ','(head(T12, T15), ','(tail(T12, X21), duplicate(X21, T16))))\n\nT12 is ground\nX21 is free\nduplicate(T12, T2) !=? duplicate([], [])", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: ','(no(empty(T12)), ','(head(T12, T15), ','(tail(T12, X21), duplicate(X21, T16)))), SCOPE: 6, CLAUSE: 7 | ','(no(empty(T12)), ','(head(T12, T15), ','(tail(T12, X21), duplicate(X21, T16)))), SCOPE: 6, CLAUSE: 8\n\nT12 is ground\nX21 is free\nduplicate(T12, T2) !=? duplicate([], [])", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: ','(','(call(empty(T19)), ','(!_6, failure(a))), ','(head(T19, T15), ','(tail(T19, X21), duplicate(X21, T16)))) | ','(no(empty(T19)), ','(head(T19, T15), ','(tail(T19, X21), duplicate(X21, T16)))), SCOPE: 6, CLAUSE: 8\n\nT19 is ground\nX21 is free\nduplicate(T19, T2) !=? duplicate([], [])", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: ','(empty(T19), ','(','(!_6, failure(a)), ','(head(T19, T15), ','(tail(T19, X21), duplicate(X21, T16))))) | ?_7 | ','(no(empty(T19)), ','(head(T19, T15), ','(tail(T19, X21), duplicate(X21, T16)))), SCOPE: 6, CLAUSE: 8\n\nT19 is ground\nX21 is free\nduplicate(T19, T2) !=? duplicate([], [])", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: ','(empty(T19), ','(','(!_6, failure(a)), ','(head(T19, T15), ','(tail(T19, X21), duplicate(X21, T16))))), SCOPE: 8, CLAUSE: 6 | ?_8 | ?_7 | ','(no(empty(T19)), ','(head(T19, T15), ','(tail(T19, X21), duplicate(X21, T16)))), SCOPE: 6, CLAUSE: 8\n\nT19 is ground\nX21 is free\nduplicate(T19, T2) !=? duplicate([], [])", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: ','(','(!_6, failure(a)), ','(head([], T15), ','(tail([], X21), duplicate(X21, T16)))) | ?_8 | ?_7 | ','(no(empty([])), ','(head([], T15), ','(tail([], X21), duplicate(X21, T16)))), SCOPE: 6, CLAUSE: 8\n\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: ?_8 | ?_7 | ','(no(empty(T19)), ','(head(T19, T15), ','(tail(T19, X21), duplicate(X21, T16)))), SCOPE: 6, CLAUSE: 8\n\nT19 is ground\nX21 is free\nduplicate(T19, T2) !=? duplicate([], [])\nempty(T19) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: ','(failure(a), ','(head([], T15), ','(tail([], X21), duplicate(X21, T16))))\n\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: ','(failure(a), ','(head([], T15), ','(tail([], X21), duplicate(X21, T16)))), SCOPE: 9, CLAUSE: 9\n\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: ?_7 | ','(no(empty(T19)), ','(head(T19, T15), ','(tail(T19, X21), duplicate(X21, T16)))), SCOPE: 6, CLAUSE: 8\n\nT19 is ground\nX21 is free\nduplicate(T19, T2) !=? duplicate([], [])\nempty(T19) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: ','(no(empty(T19)), ','(head(T19, T15), ','(tail(T19, X21), duplicate(X21, T16)))), SCOPE: 6, CLAUSE: 8\n\nT19 is ground\nX21 is free\nduplicate(T19, T2) !=? duplicate([], [])\nempty(T19) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: ','(head(T22, T15), ','(tail(T22, X21), duplicate(X21, T16)))\n\nT22 is ground\nX21 is free\nduplicate(T22, T2) !=? duplicate([], [])\nempty(T22) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: ','(head(T22, T15), ','(tail(T22, X21), duplicate(X21, T16))), SCOPE: 10, CLAUSE: 2 | ','(head(T22, T15), ','(tail(T22, X21), duplicate(X21, T16))), SCOPE: 10, CLAUSE: 3\n\nT22 is ground\nX21 is free\nduplicate(T22, T2) !=? duplicate([], [])\nempty(T22) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: ','(head(T22, T15), ','(tail(T22, X21), duplicate(X21, T16))), SCOPE: 10, CLAUSE: 3\n\nT22 is ground\nX21 is free\nduplicate(T22, T2) !=? duplicate([], [])\nempty(T22) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: ','(tail(.(T28, T29), X21), duplicate(X21, T30))\n\nT28 is ground\nT29 is ground\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: ','(tail(.(T28, T29), X21), duplicate(X21, T30)), SCOPE: 11, CLAUSE: 4 | ','(tail(.(T28, T29), X21), duplicate(X21, T30)), SCOPE: 11, CLAUSE: 5\n\nT28 is ground\nT29 is ground\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: ','(tail(.(T28, T29), X21), duplicate(X21, T30)), SCOPE: 11, CLAUSE: 5\n\nT28 is ground\nT29 is ground\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: duplicate(T36, T30)\n\nT36 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 93 [arrowhead = none ];
93 -> 4;

94 [label="EVAL with clause\nduplicate([], []).\nand substitutionT1 -> [],\nT2 -> []", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 94 [arrowhead = none ];
94 -> 9;

95 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
4 -> 95 [arrowhead = none ];
95 -> 10;

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

97 [label="EVAL with clause\nduplicate(X18, .(X19, .(X19, X20))) :- ','(no(empty(X18)), ','(head(X18, X19), ','(tail(X18, X21), duplicate(X21, X20)))).\nand substitutionT1 -> T12,\nX18 -> T12,\nX19 -> T15,\nX20 -> T16,\nT2 -> .(T15, .(T15, T16)),\nT13 -> T15,\nT14 -> T16", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 97 [arrowhead = none ];
97 -> 46;

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

99 [label="EVAL with clause\nduplicate(X8, .(X9, .(X9, X10))) :- ','(no(empty(X8)), ','(head(X8, X9), ','(tail(X8, X11), duplicate(X11, X10)))).\nand substitutionX8 -> [],\nX9 -> T7,\nX10 -> T8,\nT2 -> .(T7, .(T7, T8)),\nT5 -> T7,\nT6 -> T8", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 99 [arrowhead = none ];
99 -> 19;

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

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

102 [label="ONLY EVAL with clause\nno(X14) :- ','(call(X14), ','(!_2, failure(a))).\nand substitutionX14 -> empty([])", fontsize=14, style = filled, fillcolor = lightblue];
22 -> 102 [arrowhead = none ];
102 -> 23;

103 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
23 -> 103 [arrowhead = none ];
103 -> 26;

104 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
26 -> 104 [arrowhead = none ];
104 -> 28;

105 [label="ONLY EVAL with clause\nempty([]).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
28 -> 105 [arrowhead = none ];
105 -> 30;

106 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
30 -> 106 [arrowhead = none ];
106 -> 32;

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

108 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
35 -> 108 [arrowhead = none ];
108 -> 36;

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

110 [label="ONLY EVAL with clause\nno(X24) :- ','(call(X24), ','(!_6, failure(a))).\nand substitutionT12 -> T19,\nX24 -> empty(T19)", fontsize=14, style = filled, fillcolor = lightblue];
51 -> 110 [arrowhead = none ];
110 -> 57;

111 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
57 -> 111 [arrowhead = none ];
111 -> 58;

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

113 [label="EVAL with clause\nempty([]).\nand substitutionT19 -> []", fontsize=14, style = filled, fillcolor = lightblue];
59 -> 113 [arrowhead = none ];
113 -> 62;

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

115 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
62 -> 115 [arrowhead = none ];
115 -> 67;

116 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
65 -> 116 [arrowhead = none ];
116 -> 72;

117 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
67 -> 117 [arrowhead = none ];
117 -> 70;

118 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
70 -> 118 [arrowhead = none ];
118 -> 71;

119 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
72 -> 119 [arrowhead = none ];
119 -> 73;

120 [label="ONLY EVAL with clause\nno(X27).\nand substitutionT19 -> T22,\nX27 -> empty(T22)", fontsize=14, style = filled, fillcolor = lightblue];
73 -> 120 [arrowhead = none ];
120 -> 75;

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

122 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (empty(T22), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
76 -> 122 [arrowhead = none ];
122 -> 77;

123 [label="EVAL with clause\nhead(.(X33, X34), X33).\nand substitutionX33 -> T28,\nX34 -> T29,\nT22 -> .(T28, T29),\nT15 -> T28,\nT16 -> T30", fontsize=14, style = filled, fillcolor = lightblue];
77 -> 123 [arrowhead = none ];
123 -> 82;

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

125 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
82 -> 125 [arrowhead = none ];
125 -> 84;

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

127 [label="ONLY EVAL with clause\ntail(.(X39, X40), X40).\nand substitutionT28 -> T35,\nX39 -> T35,\nT29 -> T36,\nX40 -> T36,\nX21 -> T36", fontsize=14, style = filled, fillcolor = lightblue];
85 -> 127 [arrowhead = none ];
127 -> 92;

128 [label="INSTANCE with matching:\nT1 -> T36\nT2 -> T30", fontsize=14, style = filled, fillcolor = lightgrey];
92 -> 128 [arrowhead = none , style=dashed];
128 -> 3[style=dashed];

}

(2) Obligation:

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

f3_in([]) → f3_out1
f3_in(.(T35, T36)) → U1(f3_in(T36), .(T35, T36))
U1(f3_out1, .(T35, T36)) → f3_out1

Q is empty.

(3) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(.(x₁, x₂)) = x₁ + 2·x₂
POL(U1(x₁, x₂)) = x₁ + x₂
POL([]) = 2
POL(f3_in(x₁)) = 2·x₁
POL(f3_out1) = 1

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

f3_in([]) → f3_out1

(4) Obligation:

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

f3_in(.(T35, T36)) → U1(f3_in(T36), .(T35, T36))
U1(f3_out1, .(T35, T36)) → f3_out1

Q is empty.

(5) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(.(x₁, x₂)) = 1 + x₁ + 2·x₂
POL(U1(x₁, x₂)) = x₁ + x₂
POL(f3_in(x₁)) = 2 + 2·x₁
POL(f3_out1) = 0