Left Termination proof of /tmp/tmp3HFOlb/delete-bbf.pl

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

0 Prolog

↳1 PrologToTRSTransformerProof (⇒, 153 ms)

↳2 QTRS

↳3 DependencyPairsProof (⇔, 32 ms)

↳4 QDP

↳5 DependencyGraphProof (⇔, 0 ms)

↳6 AND

    ↳7 QDP

        ↳8 UsableRulesProof (⇔, 0 ms)

        ↳9 QDP

        ↳10 QDPSizeChangeProof (⇔, 0 ms)

        ↳11 YES

    ↳12 QDP

        ↳13 UsableRulesProof (⇔, 0 ms)

        ↳14 QDP

        ↳15 QDPSizeChangeProof (⇔, 0 ms)

        ↳16 YES

    ↳17 QDP

        ↳18 QDPSizeChangeProof (⇔, 0 ms)

        ↳19 YES

(0) Obligation:

Clauses:

delete(X, tree(X, void, Right), Right).
delete(X, tree(X, Left, void), Left).
delete(X, tree(X, Left, Right), tree(Y, Left, Right1)) :- delmin(Right, Y, Right1).
delete(X, tree(Y, Left, Right), tree(Y, Left1, Right)) :- ','(less(X, Y), delete(X, Left, Left1)).
delete(X, tree(Y, Left, Right), tree(Y, Left, Right1)) :- ','(less(Y, X), delete(X, Right, Right1)).
delmin(tree(Y, void, Right), Y, Right).
delmin(tree(X, Left, X1), Y, tree(X, Left1, X2)) :- delmin(Left, Y, Left1).
less(0, s(X3)).
less(s(X), s(Y)) :- less(X, Y).

Query: delete(g,g,a)

(1) PrologToTRSTransformerProof (SOUND transformation)

Transformed Prolog program to TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="2: delete(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 0\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: delmin(T46, T49, T50)\n\nT46 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: delmin(T46, T49, T50), SCOPE: 2, CLAUSE: 5 | delmin(T46, T49, T50), SCOPE: 2, CLAUSE: 6\n\nT46 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: delmin(T46, T49, T50), SCOPE: 2, CLAUSE: 5\n\nT46 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: delmin(T46, T49, T50), SCOPE: 2, CLAUSE: 6\n\nT46 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: delmin(T78, T83, T84)\n\nT78 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: ','(less(T109, T110), delete(T109, T111, T114))\n\nT109 is ground\nT110 is ground\nT111 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: less(T109, T110)\n\nT109 is ground\nT110 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: delete(T109, T111, T114)\n\nT109 is ground\nT111 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: less(T109, T110), SCOPE: 3, CLAUSE: 7 | less(T109, T110), SCOPE: 3, CLAUSE: 8\n\nT109 is ground\nT110 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: less(T109, T110), SCOPE: 3, CLAUSE: 7\n\nT109 is ground\nT110 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: less(T109, T110), SCOPE: 3, CLAUSE: 8\n\nT109 is ground\nT110 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: less(T128, T129)\n\nT128 is ground\nT129 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: ','(less(T147, T146), delete(T146, T149, T151))\n\nT146 is ground\nT147 is ground\nT149 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: less(T147, T146)\n\nT146 is ground\nT147 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: delete(T146, T149, T151)\n\nT146 is ground\nT149 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 109 [arrowhead = none ];
109 -> 4;

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

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

112 [label="EVAL with clause\ndelete(X12, tree(X12, void, X13), X13).\nand substitutionT1 -> T12,\nX12 -> T12,\nX13 -> T13,\nT2 -> tree(T12, void, T13),\nT3 -> T13", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 112 [arrowhead = none ];
112 -> 11;

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

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

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

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

117 [label="EVAL with clause\ndelete(X22, tree(X22, X23, void), X23).\nand substitutionT1 -> T22,\nX22 -> T22,\nX23 -> T23,\nT2 -> tree(T22, T23, void),\nT3 -> T23", fontsize=14, style = filled, fillcolor = lightblue];
18 -> 117 [arrowhead = none ];
117 -> 26;

118 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
18 -> 118 [arrowhead = none ];
118 -> 27;

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

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

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

122 [label="EVAL with clause\ndelete(X44, tree(X44, X45, X46), tree(X47, X45, X48)) :- delmin(X46, X47, X48).\nand substitutionT1 -> T44,\nX44 -> T44,\nX45 -> T45,\nX46 -> T46,\nT2 -> tree(T44, T45, T46),\nX47 -> T49,\nX48 -> T50,\nT3 -> tree(T49, T45, T50),\nT47 -> T49,\nT48 -> T50", fontsize=14, style = filled, fillcolor = lightblue];
39 -> 122 [arrowhead = none ];
122 -> 51;

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

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

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

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

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

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

129 [label="EVAL with clause\ndelmin(tree(X61, void, X62), X61, X62).\nand substitutionX61 -> T63,\nX62 -> T64,\nT46 -> tree(T63, void, T64),\nT49 -> T63,\nT50 -> T64", fontsize=14, style = filled, fillcolor = lightblue];
56 -> 129 [arrowhead = none ];
129 -> 63;

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

131 [label="EVAL with clause\ndelmin(tree(X75, X76, X77), X78, tree(X75, X79, X80)) :- delmin(X76, X78, X79).\nand substitutionX75 -> T77,\nX76 -> T78,\nX77 -> T79,\nT46 -> tree(T77, T78, T79),\nT49 -> T83,\nX78 -> T83,\nX79 -> T84,\nX80 -> T82,\nT50 -> tree(T77, T84, T82),\nT80 -> T83,\nT81 -> T84", fontsize=14, style = filled, fillcolor = lightblue];
57 -> 131 [arrowhead = none ];
131 -> 69;

132 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
57 -> 132 [arrowhead = none ];
132 -> 71;

133 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
63 -> 133 [arrowhead = none ];
133 -> 67;

134 [label="INSTANCE with matching:\nT46 -> T78\nT49 -> T83\nT50 -> T84", fontsize=14, style = filled, fillcolor = lightgrey];
69 -> 134 [arrowhead = none , style=dashed];
134 -> 51[style=dashed];

135 [label="EVAL with clause\ndelete(X105, tree(X106, X107, X108), tree(X106, X109, X108)) :- ','(less(X105, X106), delete(X105, X107, X109)).\nand substitutionT1 -> T109,\nX105 -> T109,\nX106 -> T110,\nX107 -> T111,\nX108 -> T112,\nT2 -> tree(T110, T111, T112),\nX109 -> T114,\nT3 -> tree(T110, T114, T112),\nT113 -> T114", fontsize=14, style = filled, fillcolor = lightblue];
75 -> 135 [arrowhead = none ];
135 -> 81;

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

137 [label="EVAL with clause\ndelete(X141, tree(X142, X143, X144), tree(X142, X143, X145)) :- ','(less(X142, X141), delete(X141, X144, X145)).\nand substitutionT1 -> T146,\nX141 -> T146,\nX142 -> T147,\nX143 -> T148,\nX144 -> T149,\nT2 -> tree(T147, T148, T149),\nX145 -> T151,\nT3 -> tree(T147, T148, T151),\nT150 -> T151", fontsize=14, style = filled, fillcolor = lightblue];
76 -> 137 [arrowhead = none ];
137 -> 105;

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

139 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
81 -> 139 [arrowhead = none ];
139 -> 85;

140 [label="SPLIT 2\nnew knowledge:\nT109 is ground\nT110 is ground", fontsize=14, style = filled, fillcolor = violet];
81 -> 140 [arrowhead = none ];
140 -> 86;

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

142 [label="INSTANCE with matching:\nT1 -> T109\nT2 -> T111\nT3 -> T114", fontsize=14, style = filled, fillcolor = lightgrey];
86 -> 142 [arrowhead = none , style=dashed];
142 -> 2[style=dashed];

143 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
88 -> 143 [arrowhead = none ];
143 -> 89;

144 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
88 -> 144 [arrowhead = none ];
144 -> 90;

145 [label="EVAL with clause\nless(0, s(X118)).\nand substitutionT109 -> 0,\nX118 -> T123,\nT110 -> s(T123)", fontsize=14, style = filled, fillcolor = lightblue];
89 -> 145 [arrowhead = none ];
145 -> 93;

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

147 [label="EVAL with clause\nless(s(X123), s(X124)) :- less(X123, X124).\nand substitutionX123 -> T128,\nT109 -> s(T128),\nX124 -> T129,\nT110 -> s(T129)", fontsize=14, style = filled, fillcolor = lightblue];
90 -> 147 [arrowhead = none ];
147 -> 97;

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

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

150 [label="INSTANCE with matching:\nT109 -> T128\nT110 -> T129", fontsize=14, style = filled, fillcolor = lightgrey];
97 -> 150 [arrowhead = none , style=dashed];
150 -> 85[style=dashed];

151 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
105 -> 151 [arrowhead = none ];
151 -> 107;

152 [label="SPLIT 2\nnew knowledge:\nT147 is ground\nT146 is ground", fontsize=14, style = filled, fillcolor = violet];
105 -> 152 [arrowhead = none ];
152 -> 108;

153 [label="INSTANCE with matching:\nT109 -> T147\nT110 -> T146", fontsize=14, style = filled, fillcolor = lightgrey];
107 -> 153 [arrowhead = none , style=dashed];
153 -> 85[style=dashed];

154 [label="INSTANCE with matching:\nT1 -> T146\nT2 -> T149\nT3 -> T151", fontsize=14, style = filled, fillcolor = lightgrey];
108 -> 154 [arrowhead = none , style=dashed];
154 -> 2[style=dashed];

}

(2) Obligation:

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

f2_in(T12, tree(T12, void, T13)) → f2_out1
f2_in(T22, tree(T22, T23, void)) → f2_out1
f2_in(T44, tree(T44, T45, T46)) → U1(f51_in(T46), T44, tree(T44, T45, T46))
U1(f51_out1(T49), T44, tree(T44, T45, T46)) → f2_out1
f2_in(T109, tree(T110, T111, T112)) → U2(f81_in(T109, T110, T111), T109, tree(T110, T111, T112))
U2(f81_out1, T109, tree(T110, T111, T112)) → f2_out1
f2_in(T146, tree(T147, T148, T149)) → U3(f105_in(T147, T146, T149), T146, tree(T147, T148, T149))
U3(f105_out1, T146, tree(T147, T148, T149)) → f2_out1
f51_in(tree(T63, void, T64)) → f51_out1(T63)
f51_in(tree(T77, T78, T79)) → U4(f51_in(T78), tree(T77, T78, T79))
U4(f51_out1(T83), tree(T77, T78, T79)) → f51_out1(T83)
f85_in(0, s(T123)) → f85_out1
f85_in(s(T128), s(T129)) → U5(f85_in(T128, T129), s(T128), s(T129))
U5(f85_out1, s(T128), s(T129)) → f85_out1
f81_in(T109, T110, T111) → U6(f85_in(T109, T110), T109, T110, T111)
U6(f85_out1, T109, T110, T111) → U7(f2_in(T109, T111), T109, T110, T111)
U7(f2_out1, T109, T110, T111) → f81_out1
f105_in(T147, T146, T149) → U8(f85_in(T147, T146), T147, T146, T149)
U8(f85_out1, T147, T146, T149) → U9(f2_in(T146, T149), T147, T146, T149)
U9(f2_out1, T147, T146, T149) → f105_out1

Q is empty.

(3) DependencyPairsProof (EQUIVALENT transformation)

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

(4) Obligation:

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

F2_IN(T44, tree(T44, T45, T46)) → U1¹(f51_in(T46), T44, tree(T44, T45, T46))
F2_IN(T44, tree(T44, T45, T46)) → F51_IN(T46)
F2_IN(T109, tree(T110, T111, T112)) → U2¹(f81_in(T109, T110, T111), T109, tree(T110, T111, T112))
F2_IN(T109, tree(T110, T111, T112)) → F81_IN(T109, T110, T111)
F2_IN(T146, tree(T147, T148, T149)) → U3¹(f105_in(T147, T146, T149), T146, tree(T147, T148, T149))
F2_IN(T146, tree(T147, T148, T149)) → F105_IN(T147, T146, T149)
F51_IN(tree(T77, T78, T79)) → U4¹(f51_in(T78), tree(T77, T78, T79))
F51_IN(tree(T77, T78, T79)) → F51_IN(T78)
F85_IN(s(T128), s(T129)) → U5¹(f85_in(T128, T129), s(T128), s(T129))
F85_IN(s(T128), s(T129)) → F85_IN(T128, T129)
F81_IN(T109, T110, T111) → U6¹(f85_in(T109, T110), T109, T110, T111)
F81_IN(T109, T110, T111) → F85_IN(T109, T110)
U6¹(f85_out1, T109, T110, T111) → U7¹(f2_in(T109, T111), T109, T110, T111)
U6¹(f85_out1, T109, T110, T111) → F2_IN(T109, T111)
F105_IN(T147, T146, T149) → U8¹(f85_in(T147, T146), T147, T146, T149)
F105_IN(T147, T146, T149) → F85_IN(T147, T146)
U8¹(f85_out1, T147, T146, T149) → U9¹(f2_in(T146, T149), T147, T146, T149)
U8¹(f85_out1, T147, T146, T149) → F2_IN(T146, T149)

The TRS R consists of the following rules:

f2_in(T12, tree(T12, void, T13)) → f2_out1
f2_in(T22, tree(T22, T23, void)) → f2_out1
f2_in(T44, tree(T44, T45, T46)) → U1(f51_in(T46), T44, tree(T44, T45, T46))
U1(f51_out1(T49), T44, tree(T44, T45, T46)) → f2_out1
f2_in(T109, tree(T110, T111, T112)) → U2(f81_in(T109, T110, T111), T109, tree(T110, T111, T112))
U2(f81_out1, T109, tree(T110, T111, T112)) → f2_out1
f2_in(T146, tree(T147, T148, T149)) → U3(f105_in(T147, T146, T149), T146, tree(T147, T148, T149))
U3(f105_out1, T146, tree(T147, T148, T149)) → f2_out1
f51_in(tree(T63, void, T64)) → f51_out1(T63)
f51_in(tree(T77, T78, T79)) → U4(f51_in(T78), tree(T77, T78, T79))
U4(f51_out1(T83), tree(T77, T78, T79)) → f51_out1(T83)
f85_in(0, s(T123)) → f85_out1
f85_in(s(T128), s(T129)) → U5(f85_in(T128, T129), s(T128), s(T129))
U5(f85_out1, s(T128), s(T129)) → f85_out1
f81_in(T109, T110, T111) → U6(f85_in(T109, T110), T109, T110, T111)
U6(f85_out1, T109, T110, T111) → U7(f2_in(T109, T111), T109, T110, T111)
U7(f2_out1, T109, T110, T111) → f81_out1
f105_in(T147, T146, T149) → U8(f85_in(T147, T146), T147, T146, T149)
U8(f85_out1, T147, T146, T149) → U9(f2_in(T146, T149), T147, T146, T149)
U9(f2_out1, T147, T146, T149) → f105_out1

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

F85_IN(s(T128), s(T129)) → F85_IN(T128, T129)

The TRS R consists of the following rules:

f2_in(T12, tree(T12, void, T13)) → f2_out1
f2_in(T22, tree(T22, T23, void)) → f2_out1
f2_in(T44, tree(T44, T45, T46)) → U1(f51_in(T46), T44, tree(T44, T45, T46))
U1(f51_out1(T49), T44, tree(T44, T45, T46)) → f2_out1
f2_in(T109, tree(T110, T111, T112)) → U2(f81_in(T109, T110, T111), T109, tree(T110, T111, T112))
U2(f81_out1, T109, tree(T110, T111, T112)) → f2_out1
f2_in(T146, tree(T147, T148, T149)) → U3(f105_in(T147, T146, T149), T146, tree(T147, T148, T149))
U3(f105_out1, T146, tree(T147, T148, T149)) → f2_out1
f51_in(tree(T63, void, T64)) → f51_out1(T63)
f51_in(tree(T77, T78, T79)) → U4(f51_in(T78), tree(T77, T78, T79))
U4(f51_out1(T83), tree(T77, T78, T79)) → f51_out1(T83)
f85_in(0, s(T123)) → f85_out1
f85_in(s(T128), s(T129)) → U5(f85_in(T128, T129), s(T128), s(T129))
U5(f85_out1, s(T128), s(T129)) → f85_out1
f81_in(T109, T110, T111) → U6(f85_in(T109, T110), T109, T110, T111)
U6(f85_out1, T109, T110, T111) → U7(f2_in(T109, T111), T109, T110, T111)
U7(f2_out1, T109, T110, T111) → f81_out1
f105_in(T147, T146, T149) → U8(f85_in(T147, T146), T147, T146, T149)
U8(f85_out1, T147, T146, T149) → U9(f2_in(T146, T149), T147, T146, T149)
U9(f2_out1, T147, T146, T149) → f105_out1

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

(8) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(9) Obligation:

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

F85_IN(s(T128), s(T129)) → F85_IN(T128, T129)

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

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

F85_IN(s(T128), s(T129)) → F85_IN(T128, T129)
The graph contains the following edges 1 > 1, 2 > 2

(11) YES

(12) Obligation:

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

F51_IN(tree(T77, T78, T79)) → F51_IN(T78)

The TRS R consists of the following rules:

f2_in(T12, tree(T12, void, T13)) → f2_out1
f2_in(T22, tree(T22, T23, void)) → f2_out1
f2_in(T44, tree(T44, T45, T46)) → U1(f51_in(T46), T44, tree(T44, T45, T46))
U1(f51_out1(T49), T44, tree(T44, T45, T46)) → f2_out1
f2_in(T109, tree(T110, T111, T112)) → U2(f81_in(T109, T110, T111), T109, tree(T110, T111, T112))
U2(f81_out1, T109, tree(T110, T111, T112)) → f2_out1
f2_in(T146, tree(T147, T148, T149)) → U3(f105_in(T147, T146, T149), T146, tree(T147, T148, T149))
U3(f105_out1, T146, tree(T147, T148, T149)) → f2_out1
f51_in(tree(T63, void, T64)) → f51_out1(T63)
f51_in(tree(T77, T78, T79)) → U4(f51_in(T78), tree(T77, T78, T79))
U4(f51_out1(T83), tree(T77, T78, T79)) → f51_out1(T83)
f85_in(0, s(T123)) → f85_out1
f85_in(s(T128), s(T129)) → U5(f85_in(T128, T129), s(T128), s(T129))
U5(f85_out1, s(T128), s(T129)) → f85_out1
f81_in(T109, T110, T111) → U6(f85_in(T109, T110), T109, T110, T111)
U6(f85_out1, T109, T110, T111) → U7(f2_in(T109, T111), T109, T110, T111)
U7(f2_out1, T109, T110, T111) → f81_out1
f105_in(T147, T146, T149) → U8(f85_in(T147, T146), T147, T146, T149)
U8(f85_out1, T147, T146, T149) → U9(f2_in(T146, T149), T147, T146, T149)
U9(f2_out1, T147, T146, T149) → f105_out1

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

(13) UsableRulesProof (EQUIVALENT transformation)

(14) Obligation:

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

F51_IN(tree(T77, T78, T79)) → F51_IN(T78)

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

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

F51_IN(tree(T77, T78, T79)) → F51_IN(T78)
The graph contains the following edges 1 > 1

(16) YES

(17) Obligation:

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

F2_IN(T109, tree(T110, T111, T112)) → F81_IN(T109, T110, T111)
F81_IN(T109, T110, T111) → U6¹(f85_in(T109, T110), T109, T110, T111)
U6¹(f85_out1, T109, T110, T111) → F2_IN(T109, T111)
F2_IN(T146, tree(T147, T148, T149)) → F105_IN(T147, T146, T149)
F105_IN(T147, T146, T149) → U8¹(f85_in(T147, T146), T147, T146, T149)
U8¹(f85_out1, T147, T146, T149) → F2_IN(T146, T149)

The TRS R consists of the following rules:

f2_in(T12, tree(T12, void, T13)) → f2_out1
f2_in(T22, tree(T22, T23, void)) → f2_out1
f2_in(T44, tree(T44, T45, T46)) → U1(f51_in(T46), T44, tree(T44, T45, T46))
U1(f51_out1(T49), T44, tree(T44, T45, T46)) → f2_out1
f2_in(T109, tree(T110, T111, T112)) → U2(f81_in(T109, T110, T111), T109, tree(T110, T111, T112))
U2(f81_out1, T109, tree(T110, T111, T112)) → f2_out1
f2_in(T146, tree(T147, T148, T149)) → U3(f105_in(T147, T146, T149), T146, tree(T147, T148, T149))
U3(f105_out1, T146, tree(T147, T148, T149)) → f2_out1
f51_in(tree(T63, void, T64)) → f51_out1(T63)
f51_in(tree(T77, T78, T79)) → U4(f51_in(T78), tree(T77, T78, T79))
U4(f51_out1(T83), tree(T77, T78, T79)) → f51_out1(T83)
f85_in(0, s(T123)) → f85_out1
f85_in(s(T128), s(T129)) → U5(f85_in(T128, T129), s(T128), s(T129))
U5(f85_out1, s(T128), s(T129)) → f85_out1
f81_in(T109, T110, T111) → U6(f85_in(T109, T110), T109, T110, T111)
U6(f85_out1, T109, T110, T111) → U7(f2_in(T109, T111), T109, T110, T111)
U7(f2_out1, T109, T110, T111) → f81_out1
f105_in(T147, T146, T149) → U8(f85_in(T147, T146), T147, T146, T149)
U8(f85_out1, T147, T146, T149) → U9(f2_in(T146, T149), T147, T146, T149)
U9(f2_out1, T147, T146, T149) → f105_out1

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

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

F81_IN(T109, T110, T111) → U6¹(f85_in(T109, T110), T109, T110, T111)
The graph contains the following edges 1 >= 2, 2 >= 3, 3 >= 4
U6¹(f85_out1, T109, T110, T111) → F2_IN(T109, T111)
The graph contains the following edges 2 >= 1, 4 >= 2
U8¹(f85_out1, T147, T146, T149) → F2_IN(T146, T149)
The graph contains the following edges 3 >= 1, 4 >= 2
F2_IN(T109, tree(T110, T111, T112)) → F81_IN(T109, T110, T111)
The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3
F2_IN(T146, tree(T147, T148, T149)) → F105_IN(T147, T146, T149)
The graph contains the following edges 2 > 1, 1 >= 2, 2 > 3
F105_IN(T147, T146, T149) → U8¹(f85_in(T147, T146), T147, T146, T149)
The graph contains the following edges 1 >= 2, 2 >= 3, 3 >= 4

(0) Obligation:

(1) PrologToTRSTransformerProof (SOUND transformation)

(2) Obligation:

(3) DependencyPairsProof (EQUIVALENT transformation)

(4) Obligation:

(5) DependencyGraphProof (EQUIVALENT transformation)

(6) Complex Obligation (AND)

(7) Obligation:

(8) UsableRulesProof (EQUIVALENT transformation)

(9) Obligation:

(10) QDPSizeChangeProof (EQUIVALENT transformation)

(11) YES

(12) Obligation:

(13) UsableRulesProof (EQUIVALENT transformation)

(14) Obligation:

(15) QDPSizeChangeProof (EQUIVALENT transformation)

(16) YES

(17) Obligation:

(18) QDPSizeChangeProof (EQUIVALENT transformation)

(19) YES