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

(0) Obligation:

Clauses:

in(X, tree(X, X1, X2)).
in(X, tree(Y, Left, X3)) :- ','(less(X, Y), in(X, Left)).
in(X, tree(Y, X4, Right)) :- ','(less(Y, X), in(X, Right)).
less(0, s(X5)).
less(s(X), s(Y)) :- less(X, Y).

Queries:

in(a,g).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: in(T1, T2)\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: in(T1, T2), SCOPE: 1, CLAUSE: 0 | in(T1, T2), SCOPE: 1, CLAUSE: 1 | in(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: true | in(T1, tree(T6, T7, T8)), SCOPE: 1, CLAUSE: 1 | in(T1, tree(T6, T7, T8)), SCOPE: 1, CLAUSE: 2\n\nT6 is ground\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: in(T1, T2), SCOPE: 1, CLAUSE: 1 | in(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT2 is ground\nin(T1, T2) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: in(T1, tree(T6, T7, T8)), SCOPE: 1, CLAUSE: 1 | in(T1, tree(T6, T7, T8)), SCOPE: 1, CLAUSE: 2\n\nT6 is ground\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: ','(less(T17, T14), in(T17, T15)) | in(T1, tree(T14, T15, T16)), SCOPE: 1, CLAUSE: 2\n\nT14 is ground\nT15 is ground\nT16 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: ','(less(T17, T14), in(T17, T15)), SCOPE: 2, CLAUSE: 3 | ','(less(T17, T14), in(T17, T15)), SCOPE: 2, CLAUSE: 4 | ?_2 | in(T1, tree(T14, T15, T16)), SCOPE: 1, CLAUSE: 2\n\nT14 is ground\nT15 is ground\nT16 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: ','(less(T17, T14), in(T17, T15)), SCOPE: 2, CLAUSE: 3\n\nT14 is ground\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: ','(less(T17, T14), in(T17, T15)), SCOPE: 2, CLAUSE: 4 | ?_2 | in(T1, tree(T14, T15, T16)), SCOPE: 1, CLAUSE: 2\n\nT14 is ground\nT15 is ground\nT16 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: in(0, T15)\n\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: in(0, T15), SCOPE: 3, CLAUSE: 0 | in(0, T15), SCOPE: 3, CLAUSE: 1 | in(0, T15), SCOPE: 3, CLAUSE: 2\n\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: in(0, T15), SCOPE: 3, CLAUSE: 0\n\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: in(0, T15), SCOPE: 3, CLAUSE: 1 | in(0, T15), SCOPE: 3, CLAUSE: 2\n\nT15 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];
18 [label="18: in(0, T15), SCOPE: 3, CLAUSE: 1\n\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: in(0, T15), SCOPE: 3, CLAUSE: 2\n\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: ','(less(0, T49), in(0, T50))\n\nT49 is ground\nT50 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: less(0, T49)\n\nT49 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: in(0, T50)\n\nT50 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: less(0, T49), SCOPE: 4, CLAUSE: 3 | less(0, T49), SCOPE: 4, CLAUSE: 4\n\nT49 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: less(0, T49), SCOPE: 4, CLAUSE: 3\n\nT49 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: less(0, T49), SCOPE: 4, CLAUSE: 4\n\nT49 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: ','(less(T71, 0), in(0, T73))\n\nT71 is ground\nT73 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: less(T71, 0)\n\nT71 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: in(0, T73)\n\nT73 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: less(T71, 0), SCOPE: 5, CLAUSE: 3 | less(T71, 0), SCOPE: 5, CLAUSE: 4\n\nT71 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: less(T71, 0), SCOPE: 5, CLAUSE: 4\n\nT71 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: ','(less(T17, T14), in(T17, T15)), SCOPE: 2, CLAUSE: 4\n\nT14 is ground\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: ?_2 | in(T1, tree(T14, T15, T16)), SCOPE: 1, CLAUSE: 2\n\nT14 is ground\nT15 is ground\nT16 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: ','(less(T91, T90), in(s(T91), T15))\n\nT15 is ground\nT90 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: less(T91, T90)\n\nT90 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: in(s(T94), T15)\n\nT15 is ground\nT94 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: less(T91, T90), SCOPE: 6, CLAUSE: 3 | less(T91, T90), SCOPE: 6, CLAUSE: 4\n\nT90 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: less(T91, T90), SCOPE: 6, CLAUSE: 3\n\nT90 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: less(T91, T90), SCOPE: 6, CLAUSE: 4\n\nT90 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: less(T108, T107)\n\nT107 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: in(T1, tree(T14, T15, T16)), SCOPE: 1, CLAUSE: 2\n\nT14 is ground\nT15 is ground\nT16 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: ','(less(T129, T132), in(T132, T131))\n\nT129 is ground\nT131 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: less(T129, T132)\n\nT129 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: in(T135, T131)\n\nT131 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: less(T129, T132), SCOPE: 7, CLAUSE: 3 | less(T129, T132), SCOPE: 7, CLAUSE: 4\n\nT129 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: less(T129, T132), SCOPE: 7, CLAUSE: 3\n\nT129 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: less(T129, T132), SCOPE: 7, CLAUSE: 4\n\nT129 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: less(T147, T149)\n\nT147 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: ','(less(T166, T163), in(T166, T164)) | in(T1, tree(T163, T164, T165)), SCOPE: 1, CLAUSE: 2\n\nT163 is ground\nT164 is ground\nT165 is ground\nin(T1, tree(T163, T164, T165)) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: in(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT2 is ground\nin(T1, T2) !=? in(X9, tree(X9, X10, X11))\nin(T1, T2) !=? in(X210, tree(X211, X212, X213))", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: ','(less(T166, T163), in(T166, T164)), SCOPE: 8, CLAUSE: 3 | ','(less(T166, T163), in(T166, T164)), SCOPE: 8, CLAUSE: 4 | ?_8 | in(T1, tree(T163, T164, T165)), SCOPE: 1, CLAUSE: 2\n\nT163 is ground\nT164 is ground\nT165 is ground\nin(T1, tree(T163, T164, T165)) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: ','(less(T166, T163), in(T166, T164)), SCOPE: 8, CLAUSE: 3\n\nT163 is ground\nT164 is ground\nin(T1, tree(T163, T164, T165)) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: ','(less(T166, T163), in(T166, T164)), SCOPE: 8, CLAUSE: 4 | ?_8 | in(T1, tree(T163, T164, T165)), SCOPE: 1, CLAUSE: 2\n\nT163 is ground\nT164 is ground\nT165 is ground\nin(T1, tree(T163, T164, T165)) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: in(0, T164)\n\nT164 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: ','(less(T166, T163), in(T166, T164)), SCOPE: 8, CLAUSE: 4\n\nT163 is ground\nT164 is ground\nin(T1, tree(T163, T164, T165)) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: ?_8 | in(T1, tree(T163, T164, T165)), SCOPE: 1, CLAUSE: 2\n\nT163 is ground\nT164 is ground\nT165 is ground\nin(T1, tree(T163, T164, T165)) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: ','(less(T186, T185), in(s(T186), T164))\n\nT164 is ground\nT185 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: in(T1, tree(T163, T164, T165)), SCOPE: 1, CLAUSE: 2\n\nT163 is ground\nT164 is ground\nT165 is ground\nin(T1, tree(T163, T164, T165)) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: ','(less(T201, T204), in(T204, T203))\n\nT201 is ground\nT203 is ground\nin(T1, tree(T201, T202, T203)) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 78 [arrowhead = none ];
78 -> 2;

79 [label="EVAL with clause\nin(X9, tree(X9, X10, X11)).\nand substitution\nT1 -> T6\nX9 -> T6\nX10 -> T7\nX11 -> T8\nT2 -> tree(T6, T7, T8)", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 79 [arrowhead = none ];
79 -> 3;

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

81 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
3 -> 81 [arrowhead = none ];
81 -> 5;

82 [label="EVAL with clause\nin(X210, tree(X211, X212, X213)) :- ','(less(X210, X211), in(X210, X212)).\nand substitution\nT1 -> T166\nX210 -> T166\nX211 -> T163\nX212 -> T164\nX213 -> T165\nT2 -> tree(T163, T164, T165)\nT162 -> T166", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 82 [arrowhead = none ];
82 -> 64;

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

84 [label="ONLY EVAL with clause\nin(X19, tree(X20, X21, X22)) :- ','(less(X19, X20), in(X19, X21)).\nand substitution\nT1 -> T17\nX19 -> T17\nT6 -> T14\nX20 -> T14\nT7 -> T15\nX21 -> T15\nT8 -> T16\nX22 -> T16\nT13 -> T17", fontsize=14, style = filled, fillcolor = white];
5 -> 84 [arrowhead = none ];
84 -> 6;

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

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

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

88 [label="EVAL with clause\nless(0, s(X27)).\nand substitution\nT17 -> 0\nX27 -> T22\nT14 -> s(T22)", fontsize=14, style = filled, fillcolor = lightblue];
8 -> 88 [arrowhead = none ];
88 -> 10;

89 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
8 -> 89 [arrowhead = none ];
89 -> 11;

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

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

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

93 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
12 -> 93 [arrowhead = none ];
93 -> 13;

94 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
12 -> 94 [arrowhead = none ];
94 -> 14;

95 [label="EVAL with clause\nin(X47, tree(X47, X48, X49)).\nand substitution\nX47 -> 0\nX48 -> T35\nX49 -> T36\nT15 -> tree(0, T35, T36)", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 95 [arrowhead = none ];
95 -> 15;

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

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

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

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

100 [label="EVAL with clause\nin(X69, tree(X70, X71, X72)) :- ','(less(X69, X70), in(X69, X71)).\nand substitution\nX69 -> 0\nX70 -> T49\nX71 -> T50\nX72 -> T51\nT15 -> tree(T49, T50, T51)", fontsize=14, style = filled, fillcolor = lightblue];
18 -> 100 [arrowhead = none ];
100 -> 20;

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

102 [label="EVAL with clause\nin(X103, tree(X104, X105, X106)) :- ','(less(X104, X103), in(X103, X106)).\nand substitution\nX103 -> 0\nX104 -> T71\nX105 -> T72\nX106 -> T73\nT15 -> tree(T71, T72, T73)", fontsize=14, style = filled, fillcolor = lightblue];
19 -> 102 [arrowhead = none ];
102 -> 31;

103 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
19 -> 103 [arrowhead = none ];
103 -> 32;

104 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
20 -> 104 [arrowhead = none ];
104 -> 22;

105 [label="SPLIT 2", fontsize=14, style = filled, fillcolor = violet];
20 -> 105 [arrowhead = none ];
105 -> 23;

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

107 [label="INSTANCE with matching:\nT15 -> T50", fontsize=14, style = filled, fillcolor = lightgrey];
23 -> 107 [arrowhead = none , style=dashed];
107 -> 10[style=dashed];

108 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
24 -> 108 [arrowhead = none ];
108 -> 25;

109 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
24 -> 109 [arrowhead = none ];
109 -> 26;

110 [label="EVAL with clause\nless(0, s(X85)).\nand substitution\nX85 -> T60\nT49 -> s(T60)", fontsize=14, style = filled, fillcolor = lightblue];
25 -> 110 [arrowhead = none ];
110 -> 27;

111 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
25 -> 111 [arrowhead = none ];
111 -> 28;

112 [label="BACKTRACK\nfor clause: less(s(X), s(Y)) :- less(X, Y)because of non-unification", fontsize=14, style = filled, fillcolor = white];
26 -> 112 [arrowhead = none ];
112 -> 30;

113 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
27 -> 113 [arrowhead = none ];
113 -> 29;

114 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
31 -> 114 [arrowhead = none ];
114 -> 33;

115 [label="SPLIT 2", fontsize=14, style = filled, fillcolor = violet];
31 -> 115 [arrowhead = none ];
115 -> 34;

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

117 [label="INSTANCE with matching:\nT15 -> T73", fontsize=14, style = filled, fillcolor = lightgrey];
34 -> 117 [arrowhead = none , style=dashed];
117 -> 10[style=dashed];

118 [label="BACKTRACK\nfor clause: less(0, s(X5))because of non-unification", fontsize=14, style = filled, fillcolor = white];
35 -> 118 [arrowhead = none ];
118 -> 36;

119 [label="BACKTRACK\nfor clause: less(s(X), s(Y)) :- less(X, Y)because of non-unification", fontsize=14, style = filled, fillcolor = white];
36 -> 119 [arrowhead = none ];
119 -> 37;

120 [label="EVAL with clause\nless(s(X136), s(X137)) :- less(X136, X137).\nand substitution\nX136 -> T91\nT17 -> s(T91)\nX137 -> T90\nT14 -> s(T90)\nT89 -> T91", fontsize=14, style = filled, fillcolor = lightblue];
38 -> 120 [arrowhead = none ];
120 -> 40;

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

122 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
39 -> 122 [arrowhead = none ];
122 -> 52;

123 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
40 -> 123 [arrowhead = none ];
123 -> 42;

124 [label="SPLIT 2\nnew knowledge:\nT94 is ground\nreplacements:\nT91 -> T94", fontsize=14, style = filled, fillcolor = violet];
40 -> 124 [arrowhead = none ];
124 -> 43;

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

126 [label="INSTANCE with matching:\nT1 -> s(T94)\nT2 -> T15", fontsize=14, style = filled, fillcolor = lightgrey];
43 -> 126 [arrowhead = none , style=dashed];
126 -> 1[style=dashed];

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

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

129 [label="EVAL with clause\nless(0, s(X148)).\nand substitution\nT91 -> 0\nX148 -> T101\nT90 -> s(T101)", fontsize=14, style = filled, fillcolor = lightblue];
45 -> 129 [arrowhead = none ];
129 -> 47;

130 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
45 -> 130 [arrowhead = none ];
130 -> 48;

131 [label="EVAL with clause\nless(s(X154), s(X155)) :- less(X154, X155).\nand substitution\nX154 -> T108\nT91 -> s(T108)\nX155 -> T107\nT90 -> s(T107)\nT106 -> T108", fontsize=14, style = filled, fillcolor = lightblue];
46 -> 131 [arrowhead = none ];
131 -> 50;

132 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
46 -> 132 [arrowhead = none ];
132 -> 51;

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

134 [label="INSTANCE with matching:\nT91 -> T108\nT90 -> T107", fontsize=14, style = filled, fillcolor = lightgrey];
50 -> 134 [arrowhead = none , style=dashed];
134 -> 42[style=dashed];

135 [label="ONLY EVAL with clause\nin(X176, tree(X177, X178, X179)) :- ','(less(X177, X176), in(X176, X179)).\nand substitution\nT1 -> T132\nX176 -> T132\nT14 -> T129\nX177 -> T129\nT15 -> T130\nX178 -> T130\nT16 -> T131\nX179 -> T131\nT128 -> T132", fontsize=14, style = filled, fillcolor = white];
52 -> 135 [arrowhead = none ];
135 -> 53;

136 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
53 -> 136 [arrowhead = none ];
136 -> 54;

137 [label="SPLIT 2\nreplacements:\nT132 -> T135", fontsize=14, style = filled, fillcolor = violet];
53 -> 137 [arrowhead = none ];
137 -> 55;

138 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
54 -> 138 [arrowhead = none ];
138 -> 56;

139 [label="INSTANCE with matching:\nT1 -> T135\nT2 -> T131", fontsize=14, style = filled, fillcolor = lightgrey];
55 -> 139 [arrowhead = none , style=dashed];
139 -> 1[style=dashed];

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

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

142 [label="EVAL with clause\nless(0, s(X188)).\nand substitution\nT129 -> 0\nX188 -> T142\nT132 -> s(T142)", fontsize=14, style = filled, fillcolor = lightblue];
57 -> 142 [arrowhead = none ];
142 -> 59;

143 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
57 -> 143 [arrowhead = none ];
143 -> 60;

144 [label="EVAL with clause\nless(s(X194), s(X195)) :- less(X194, X195).\nand substitution\nX194 -> T147\nT129 -> s(T147)\nX195 -> T149\nT132 -> s(T149)\nT148 -> T149", fontsize=14, style = filled, fillcolor = lightblue];
58 -> 144 [arrowhead = none ];
144 -> 62;

145 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
58 -> 145 [arrowhead = none ];
145 -> 63;

146 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
59 -> 146 [arrowhead = none ];
146 -> 61;

147 [label="INSTANCE with matching:\nT129 -> T147\nT132 -> T149", fontsize=14, style = filled, fillcolor = lightgrey];
62 -> 147 [arrowhead = none , style=dashed];
147 -> 54[style=dashed];

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

149 [label="BACKTRACK\nfor clause: in(X, tree(Y, X4, Right)) :- ','(less(Y, X), in(X, Right))\nwith clash: (in(T1, T2), in(X210, tree(X211, X212, X213)))", fontsize=14, style = filled, fillcolor = white];
65 -> 149 [arrowhead = none ];
149 -> 77;

150 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
66 -> 150 [arrowhead = none ];
150 -> 67;

151 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
66 -> 151 [arrowhead = none ];
151 -> 68;

152 [label="EVAL with clause\nless(0, s(X222)).\nand substitution\nT166 -> 0\nX222 -> T171\nT163 -> s(T171)", fontsize=14, style = filled, fillcolor = lightblue];
67 -> 152 [arrowhead = none ];
152 -> 69;

153 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
67 -> 153 [arrowhead = none ];
153 -> 70;

154 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
68 -> 154 [arrowhead = none ];
154 -> 71;

155 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
68 -> 155 [arrowhead = none ];
155 -> 72;

156 [label="INSTANCE with matching:\nT15 -> T164", fontsize=14, style = filled, fillcolor = lightgrey];
69 -> 156 [arrowhead = none , style=dashed];
156 -> 10[style=dashed];

157 [label="EVAL with clause\nless(s(X238), s(X239)) :- less(X238, X239).\nand substitution\nX238 -> T186\nT166 -> s(T186)\nX239 -> T185\nT163 -> s(T185)\nT184 -> T186", fontsize=14, style = filled, fillcolor = lightblue];
71 -> 157 [arrowhead = none ];
157 -> 73;

158 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
71 -> 158 [arrowhead = none ];
158 -> 74;

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

160 [label="INSTANCE with matching:\nT91 -> T186\nT90 -> T185\nT15 -> T164", fontsize=14, style = filled, fillcolor = lightgrey];
73 -> 160 [arrowhead = none , style=dashed];
160 -> 40[style=dashed];

161 [label="ONLY EVAL with clause\nin(X254, tree(X255, X256, X257)) :- ','(less(X255, X254), in(X254, X257)).\nand substitution\nT1 -> T204\nX254 -> T204\nT163 -> T201\nX255 -> T201\nT164 -> T202\nX256 -> T202\nT165 -> T203\nX257 -> T203\nT200 -> T204", fontsize=14, style = filled, fillcolor = white];
75 -> 161 [arrowhead = none ];
161 -> 76;

162 [label="INSTANCE with matching:\nT129 -> T201\nT132 -> T204\nT131 -> T203", fontsize=14, style = filled, fillcolor = lightgrey];
76 -> 162 [arrowhead = none , style=dashed];
162 -> 53[style=dashed];

}

(2) Obligation:

Triples:

in10(tree(T49, T50, T51)) :- ','(lessc22(T49), in10(T50)).
in10(tree(T71, T72, T73)) :- ','(lessc33(T71), in10(T73)).
less42(s(T108), s(T107)) :- less42(T108, T107).
less54(s(T147), s(T149)) :- less54(T147, T149).
p40(T91, T90, T15) :- less42(T91, T90).
p40(T94, T90, T15) :- ','(lessc42(T94, T90), in1(s(T94), T15)).
p53(T129, T132, T131) :- less54(T129, T132).
p53(T129, T135, T131) :- ','(lessc54(T129, T135), in1(T135, T131)).
in1(0, tree(s(T22), T15, T16)) :- in10(T15).
in1(s(T91), tree(s(T90), T15, T16)) :- p40(T91, T90, T15).
in1(T132, tree(T129, T130, T131)) :- p53(T129, T132, T131).
in1(0, tree(s(T171), T164, T165)) :- in10(T164).
in1(s(T186), tree(s(T185), T164, T165)) :- p40(T186, T185, T164).
in1(T204, tree(T201, T202, T203)) :- p53(T201, T204, T203).

Clauses:

inc10(tree(0, T35, T36)).
inc10(tree(T49, T50, T51)) :- ','(lessc22(T49), inc10(T50)).
inc10(tree(T71, T72, T73)) :- ','(lessc33(T71), inc10(T73)).
inc1(T6, tree(T6, T7, T8)).
inc1(0, tree(s(T22), T15, T16)) :- inc10(T15).
inc1(s(T91), tree(s(T90), T15, T16)) :- qc40(T91, T90, T15).
inc1(T132, tree(T129, T130, T131)) :- qc53(T129, T132, T131).
inc1(0, tree(s(T171), T164, T165)) :- inc10(T164).
inc1(s(T186), tree(s(T185), T164, T165)) :- qc40(T186, T185, T164).
inc1(T204, tree(T201, T202, T203)) :- qc53(T201, T204, T203).
lessc42(0, s(T101)).
lessc42(s(T108), s(T107)) :- lessc42(T108, T107).
lessc54(0, s(T142)).
lessc54(s(T147), s(T149)) :- lessc54(T147, T149).
qc40(T94, T90, T15) :- ','(lessc42(T94, T90), inc1(s(T94), T15)).
qc53(T129, T135, T131) :- ','(lessc54(T129, T135), inc1(T135, T131)).
lessc22(s(T60)).

Afs:

in1(x1, x2)  =  in1(x2)

(3) UndefinedPredicateInTriplesTransformerProof (SOUND transformation)

Deleted triples and predicates having undefined goals [UNKNOWN].

(4) Obligation:

Triples:

in10(tree(T49, T50, T51)) :- ','(lessc22(T49), in10(T50)).
less42(s(T108), s(T107)) :- less42(T108, T107).
less54(s(T147), s(T149)) :- less54(T147, T149).
p40(T91, T90, T15) :- less42(T91, T90).
p40(T94, T90, T15) :- ','(lessc42(T94, T90), in1(s(T94), T15)).
p53(T129, T132, T131) :- less54(T129, T132).
p53(T129, T135, T131) :- ','(lessc54(T129, T135), in1(T135, T131)).
in1(0, tree(s(T22), T15, T16)) :- in10(T15).
in1(s(T91), tree(s(T90), T15, T16)) :- p40(T91, T90, T15).
in1(T132, tree(T129, T130, T131)) :- p53(T129, T132, T131).
in1(0, tree(s(T171), T164, T165)) :- in10(T164).
in1(s(T186), tree(s(T185), T164, T165)) :- p40(T186, T185, T164).
in1(T204, tree(T201, T202, T203)) :- p53(T201, T204, T203).

Clauses:

inc10(tree(0, T35, T36)).
inc10(tree(T49, T50, T51)) :- ','(lessc22(T49), inc10(T50)).
inc1(T6, tree(T6, T7, T8)).
inc1(0, tree(s(T22), T15, T16)) :- inc10(T15).
inc1(s(T91), tree(s(T90), T15, T16)) :- qc40(T91, T90, T15).
inc1(T132, tree(T129, T130, T131)) :- qc53(T129, T132, T131).
inc1(0, tree(s(T171), T164, T165)) :- inc10(T164).
inc1(s(T186), tree(s(T185), T164, T165)) :- qc40(T186, T185, T164).
inc1(T204, tree(T201, T202, T203)) :- qc53(T201, T204, T203).
lessc42(0, s(T101)).
lessc42(s(T108), s(T107)) :- lessc42(T108, T107).
lessc54(0, s(T142)).
lessc54(s(T147), s(T149)) :- lessc54(T147, T149).
qc40(T94, T90, T15) :- ','(lessc42(T94, T90), inc1(s(T94), T15)).
qc53(T129, T135, T131) :- ','(lessc54(T129, T135), inc1(T135, T131)).
lessc22(s(T60)).

Afs:

in1(x1, x2)  =  in1(x2)

(5) TriplesToPiDPProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
in1_in: (f,b) (b,b)
in10_in: (b)
p40_in: (f,b,b) (b,b,b)
less42_in: (f,b) (b,b)
lessc42_in: (f,b) (b,b)
p53_in: (b,b,b) (b,f,b)
less54_in: (b,b) (b,f)
lessc54_in: (b,b) (b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

IN1_IN_AG(0, tree(s(T22), T15, T16)) → U11_AG(T22, T15, T16, in10_in_g(T15))
IN1_IN_AG(0, tree(s(T22), T15, T16)) → IN10_IN_G(T15)
IN10_IN_G(tree(T49, T50, T51)) → U1_G(T49, T50, T51, lessc22_in_g(T49))
U1_G(T49, T50, T51, lessc22_out_g(T49)) → U2_G(T49, T50, T51, in10_in_g(T50))
U1_G(T49, T50, T51, lessc22_out_g(T49)) → IN10_IN_G(T50)
IN1_IN_AG(s(T91), tree(s(T90), T15, T16)) → U12_AG(T91, T90, T15, T16, p40_in_agg(T91, T90, T15))
IN1_IN_AG(s(T91), tree(s(T90), T15, T16)) → P40_IN_AGG(T91, T90, T15)
P40_IN_AGG(T91, T90, T15) → U5_AGG(T91, T90, T15, less42_in_ag(T91, T90))
P40_IN_AGG(T91, T90, T15) → LESS42_IN_AG(T91, T90)
LESS42_IN_AG(s(T108), s(T107)) → U3_AG(T108, T107, less42_in_ag(T108, T107))
LESS42_IN_AG(s(T108), s(T107)) → LESS42_IN_AG(T108, T107)
P40_IN_AGG(T94, T90, T15) → U6_AGG(T94, T90, T15, lessc42_in_ag(T94, T90))
U6_AGG(T94, T90, T15, lessc42_out_ag(T94, T90)) → U7_AGG(T94, T90, T15, in1_in_gg(s(T94), T15))
U6_AGG(T94, T90, T15, lessc42_out_ag(T94, T90)) → IN1_IN_GG(s(T94), T15)
IN1_IN_GG(0, tree(s(T22), T15, T16)) → U11_GG(T22, T15, T16, in10_in_g(T15))
IN1_IN_GG(0, tree(s(T22), T15, T16)) → IN10_IN_G(T15)
IN1_IN_GG(s(T91), tree(s(T90), T15, T16)) → U12_GG(T91, T90, T15, T16, p40_in_ggg(T91, T90, T15))
IN1_IN_GG(s(T91), tree(s(T90), T15, T16)) → P40_IN_GGG(T91, T90, T15)
P40_IN_GGG(T91, T90, T15) → U5_GGG(T91, T90, T15, less42_in_gg(T91, T90))
P40_IN_GGG(T91, T90, T15) → LESS42_IN_GG(T91, T90)
LESS42_IN_GG(s(T108), s(T107)) → U3_GG(T108, T107, less42_in_gg(T108, T107))
LESS42_IN_GG(s(T108), s(T107)) → LESS42_IN_GG(T108, T107)
P40_IN_GGG(T94, T90, T15) → U6_GGG(T94, T90, T15, lessc42_in_gg(T94, T90))
U6_GGG(T94, T90, T15, lessc42_out_gg(T94, T90)) → U7_GGG(T94, T90, T15, in1_in_gg(s(T94), T15))
U6_GGG(T94, T90, T15, lessc42_out_gg(T94, T90)) → IN1_IN_GG(s(T94), T15)
IN1_IN_GG(T132, tree(T129, T130, T131)) → U13_GG(T132, T129, T130, T131, p53_in_ggg(T129, T132, T131))
IN1_IN_GG(T132, tree(T129, T130, T131)) → P53_IN_GGG(T129, T132, T131)
P53_IN_GGG(T129, T132, T131) → U8_GGG(T129, T132, T131, less54_in_gg(T129, T132))
P53_IN_GGG(T129, T132, T131) → LESS54_IN_GG(T129, T132)
LESS54_IN_GG(s(T147), s(T149)) → U4_GG(T147, T149, less54_in_gg(T147, T149))
LESS54_IN_GG(s(T147), s(T149)) → LESS54_IN_GG(T147, T149)
P53_IN_GGG(T129, T135, T131) → U9_GGG(T129, T135, T131, lessc54_in_gg(T129, T135))
U9_GGG(T129, T135, T131, lessc54_out_gg(T129, T135)) → U10_GGG(T129, T135, T131, in1_in_gg(T135, T131))
U9_GGG(T129, T135, T131, lessc54_out_gg(T129, T135)) → IN1_IN_GG(T135, T131)
IN1_IN_GG(0, tree(s(T171), T164, T165)) → U14_GG(T171, T164, T165, in10_in_g(T164))
IN1_IN_GG(s(T186), tree(s(T185), T164, T165)) → U15_GG(T186, T185, T164, T165, p40_in_ggg(T186, T185, T164))
IN1_IN_GG(T204, tree(T201, T202, T203)) → U16_GG(T204, T201, T202, T203, p53_in_ggg(T201, T204, T203))
IN1_IN_AG(T132, tree(T129, T130, T131)) → U13_AG(T132, T129, T130, T131, p53_in_gag(T129, T132, T131))
IN1_IN_AG(T132, tree(T129, T130, T131)) → P53_IN_GAG(T129, T132, T131)
P53_IN_GAG(T129, T132, T131) → U8_GAG(T129, T132, T131, less54_in_ga(T129, T132))
P53_IN_GAG(T129, T132, T131) → LESS54_IN_GA(T129, T132)
LESS54_IN_GA(s(T147), s(T149)) → U4_GA(T147, T149, less54_in_ga(T147, T149))
LESS54_IN_GA(s(T147), s(T149)) → LESS54_IN_GA(T147, T149)
P53_IN_GAG(T129, T135, T131) → U9_GAG(T129, T135, T131, lessc54_in_ga(T129, T135))
U9_GAG(T129, T135, T131, lessc54_out_ga(T129, T135)) → U10_GAG(T129, T135, T131, in1_in_ag(T135, T131))
U9_GAG(T129, T135, T131, lessc54_out_ga(T129, T135)) → IN1_IN_AG(T135, T131)
IN1_IN_AG(0, tree(s(T171), T164, T165)) → U14_AG(T171, T164, T165, in10_in_g(T164))
IN1_IN_AG(s(T186), tree(s(T185), T164, T165)) → U15_AG(T186, T185, T164, T165, p40_in_agg(T186, T185, T164))
IN1_IN_AG(T204, tree(T201, T202, T203)) → U16_AG(T204, T201, T202, T203, p53_in_gag(T201, T204, T203))

The TRS R consists of the following rules:

lessc22_in_g(s(T60)) → lessc22_out_g(s(T60))
lessc42_in_ag(0, s(T101)) → lessc42_out_ag(0, s(T101))
lessc42_in_ag(s(T108), s(T107)) → U26_ag(T108, T107, lessc42_in_ag(T108, T107))
U26_ag(T108, T107, lessc42_out_ag(T108, T107)) → lessc42_out_ag(s(T108), s(T107))
lessc42_in_gg(0, s(T101)) → lessc42_out_gg(0, s(T101))
lessc42_in_gg(s(T108), s(T107)) → U26_gg(T108, T107, lessc42_in_gg(T108, T107))
U26_gg(T108, T107, lessc42_out_gg(T108, T107)) → lessc42_out_gg(s(T108), s(T107))
lessc54_in_gg(0, s(T142)) → lessc54_out_gg(0, s(T142))
lessc54_in_gg(s(T147), s(T149)) → U27_gg(T147, T149, lessc54_in_gg(T147, T149))
U27_gg(T147, T149, lessc54_out_gg(T147, T149)) → lessc54_out_gg(s(T147), s(T149))
lessc54_in_ga(0, s(T142)) → lessc54_out_ga(0, s(T142))
lessc54_in_ga(s(T147), s(T149)) → U27_ga(T147, T149, lessc54_in_ga(T147, T149))
U27_ga(T147, T149, lessc54_out_ga(T147, T149)) → lessc54_out_ga(s(T147), s(T149))

The argument filtering Pi contains the following mapping:
in1_in_ag(x1, x2)  =  in1_in_ag(x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
s(x1)  =  s(x1)
in10_in_g(x1)  =  in10_in_g(x1)
lessc22_in_g(x1)  =  lessc22_in_g(x1)
lessc22_out_g(x1)  =  lessc22_out_g(x1)
p40_in_agg(x1, x2, x3)  =  p40_in_agg(x2, x3)
less42_in_ag(x1, x2)  =  less42_in_ag(x2)
lessc42_in_ag(x1, x2)  =  lessc42_in_ag(x2)
lessc42_out_ag(x1, x2)  =  lessc42_out_ag(x1, x2)
U26_ag(x1, x2, x3)  =  U26_ag(x2, x3)
in1_in_gg(x1, x2)  =  in1_in_gg(x1, x2)
0  =  0
p40_in_ggg(x1, x2, x3)  =  p40_in_ggg(x1, x2, x3)
less42_in_gg(x1, x2)  =  less42_in_gg(x1, x2)
lessc42_in_gg(x1, x2)  =  lessc42_in_gg(x1, x2)
lessc42_out_gg(x1, x2)  =  lessc42_out_gg(x1, x2)
U26_gg(x1, x2, x3)  =  U26_gg(x1, x2, x3)
p53_in_ggg(x1, x2, x3)  =  p53_in_ggg(x1, x2, x3)
less54_in_gg(x1, x2)  =  less54_in_gg(x1, x2)
lessc54_in_gg(x1, x2)  =  lessc54_in_gg(x1, x2)
lessc54_out_gg(x1, x2)  =  lessc54_out_gg(x1, x2)
U27_gg(x1, x2, x3)  =  U27_gg(x1, x2, x3)
p53_in_gag(x1, x2, x3)  =  p53_in_gag(x1, x3)
less54_in_ga(x1, x2)  =  less54_in_ga(x1)
lessc54_in_ga(x1, x2)  =  lessc54_in_ga(x1)
lessc54_out_ga(x1, x2)  =  lessc54_out_ga(x1)
U27_ga(x1, x2, x3)  =  U27_ga(x1, x3)
IN1_IN_AG(x1, x2)  =  IN1_IN_AG(x2)
U11_AG(x1, x2, x3, x4)  =  U11_AG(x1, x2, x3, x4)
IN10_IN_G(x1)  =  IN10_IN_G(x1)
U1_G(x1, x2, x3, x4)  =  U1_G(x1, x2, x3, x4)
U2_G(x1, x2, x3, x4)  =  U2_G(x1, x2, x3, x4)
U12_AG(x1, x2, x3, x4, x5)  =  U12_AG(x2, x3, x4, x5)
P40_IN_AGG(x1, x2, x3)  =  P40_IN_AGG(x2, x3)
U5_AGG(x1, x2, x3, x4)  =  U5_AGG(x2, x3, x4)
LESS42_IN_AG(x1, x2)  =  LESS42_IN_AG(x2)
U3_AG(x1, x2, x3)  =  U3_AG(x2, x3)
U6_AGG(x1, x2, x3, x4)  =  U6_AGG(x2, x3, x4)
U7_AGG(x1, x2, x3, x4)  =  U7_AGG(x1, x2, x3, x4)
IN1_IN_GG(x1, x2)  =  IN1_IN_GG(x1, x2)
U11_GG(x1, x2, x3, x4)  =  U11_GG(x1, x2, x3, x4)
U12_GG(x1, x2, x3, x4, x5)  =  U12_GG(x1, x2, x3, x4, x5)
P40_IN_GGG(x1, x2, x3)  =  P40_IN_GGG(x1, x2, x3)
U5_GGG(x1, x2, x3, x4)  =  U5_GGG(x1, x2, x3, x4)
LESS42_IN_GG(x1, x2)  =  LESS42_IN_GG(x1, x2)
U3_GG(x1, x2, x3)  =  U3_GG(x1, x2, x3)
U6_GGG(x1, x2, x3, x4)  =  U6_GGG(x1, x2, x3, x4)
U7_GGG(x1, x2, x3, x4)  =  U7_GGG(x1, x2, x3, x4)
U13_GG(x1, x2, x3, x4, x5)  =  U13_GG(x1, x2, x3, x4, x5)
P53_IN_GGG(x1, x2, x3)  =  P53_IN_GGG(x1, x2, x3)
U8_GGG(x1, x2, x3, x4)  =  U8_GGG(x1, x2, x3, x4)
LESS54_IN_GG(x1, x2)  =  LESS54_IN_GG(x1, x2)
U4_GG(x1, x2, x3)  =  U4_GG(x1, x2, x3)
U9_GGG(x1, x2, x3, x4)  =  U9_GGG(x1, x2, x3, x4)
U10_GGG(x1, x2, x3, x4)  =  U10_GGG(x1, x2, x3, x4)
U14_GG(x1, x2, x3, x4)  =  U14_GG(x1, x2, x3, x4)
U15_GG(x1, x2, x3, x4, x5)  =  U15_GG(x1, x2, x3, x4, x5)
U16_GG(x1, x2, x3, x4, x5)  =  U16_GG(x1, x2, x3, x4, x5)
U13_AG(x1, x2, x3, x4, x5)  =  U13_AG(x2, x3, x4, x5)
P53_IN_GAG(x1, x2, x3)  =  P53_IN_GAG(x1, x3)
U8_GAG(x1, x2, x3, x4)  =  U8_GAG(x1, x3, x4)
LESS54_IN_GA(x1, x2)  =  LESS54_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
U9_GAG(x1, x2, x3, x4)  =  U9_GAG(x1, x3, x4)
U10_GAG(x1, x2, x3, x4)  =  U10_GAG(x1, x3, x4)
U14_AG(x1, x2, x3, x4)  =  U14_AG(x1, x2, x3, x4)
U15_AG(x1, x2, x3, x4, x5)  =  U15_AG(x2, x3, x4, x5)
U16_AG(x1, x2, x3, x4, x5)  =  U16_AG(x2, x3, x4, x5)

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

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(6) Obligation:

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

IN1_IN_AG(0, tree(s(T22), T15, T16)) → U11_AG(T22, T15, T16, in10_in_g(T15))
IN1_IN_AG(0, tree(s(T22), T15, T16)) → IN10_IN_G(T15)
IN10_IN_G(tree(T49, T50, T51)) → U1_G(T49, T50, T51, lessc22_in_g(T49))
U1_G(T49, T50, T51, lessc22_out_g(T49)) → U2_G(T49, T50, T51, in10_in_g(T50))
U1_G(T49, T50, T51, lessc22_out_g(T49)) → IN10_IN_G(T50)
IN1_IN_AG(s(T91), tree(s(T90), T15, T16)) → U12_AG(T91, T90, T15, T16, p40_in_agg(T91, T90, T15))
IN1_IN_AG(s(T91), tree(s(T90), T15, T16)) → P40_IN_AGG(T91, T90, T15)
P40_IN_AGG(T91, T90, T15) → U5_AGG(T91, T90, T15, less42_in_ag(T91, T90))
P40_IN_AGG(T91, T90, T15) → LESS42_IN_AG(T91, T90)
LESS42_IN_AG(s(T108), s(T107)) → U3_AG(T108, T107, less42_in_ag(T108, T107))
LESS42_IN_AG(s(T108), s(T107)) → LESS42_IN_AG(T108, T107)
P40_IN_AGG(T94, T90, T15) → U6_AGG(T94, T90, T15, lessc42_in_ag(T94, T90))
U6_AGG(T94, T90, T15, lessc42_out_ag(T94, T90)) → U7_AGG(T94, T90, T15, in1_in_gg(s(T94), T15))
U6_AGG(T94, T90, T15, lessc42_out_ag(T94, T90)) → IN1_IN_GG(s(T94), T15)
IN1_IN_GG(0, tree(s(T22), T15, T16)) → U11_GG(T22, T15, T16, in10_in_g(T15))
IN1_IN_GG(0, tree(s(T22), T15, T16)) → IN10_IN_G(T15)
IN1_IN_GG(s(T91), tree(s(T90), T15, T16)) → U12_GG(T91, T90, T15, T16, p40_in_ggg(T91, T90, T15))
IN1_IN_GG(s(T91), tree(s(T90), T15, T16)) → P40_IN_GGG(T91, T90, T15)
P40_IN_GGG(T91, T90, T15) → U5_GGG(T91, T90, T15, less42_in_gg(T91, T90))
P40_IN_GGG(T91, T90, T15) → LESS42_IN_GG(T91, T90)
LESS42_IN_GG(s(T108), s(T107)) → U3_GG(T108, T107, less42_in_gg(T108, T107))
LESS42_IN_GG(s(T108), s(T107)) → LESS42_IN_GG(T108, T107)
P40_IN_GGG(T94, T90, T15) → U6_GGG(T94, T90, T15, lessc42_in_gg(T94, T90))
U6_GGG(T94, T90, T15, lessc42_out_gg(T94, T90)) → U7_GGG(T94, T90, T15, in1_in_gg(s(T94), T15))
U6_GGG(T94, T90, T15, lessc42_out_gg(T94, T90)) → IN1_IN_GG(s(T94), T15)
IN1_IN_GG(T132, tree(T129, T130, T131)) → U13_GG(T132, T129, T130, T131, p53_in_ggg(T129, T132, T131))
IN1_IN_GG(T132, tree(T129, T130, T131)) → P53_IN_GGG(T129, T132, T131)
P53_IN_GGG(T129, T132, T131) → U8_GGG(T129, T132, T131, less54_in_gg(T129, T132))
P53_IN_GGG(T129, T132, T131) → LESS54_IN_GG(T129, T132)
LESS54_IN_GG(s(T147), s(T149)) → U4_GG(T147, T149, less54_in_gg(T147, T149))
LESS54_IN_GG(s(T147), s(T149)) → LESS54_IN_GG(T147, T149)
P53_IN_GGG(T129, T135, T131) → U9_GGG(T129, T135, T131, lessc54_in_gg(T129, T135))
U9_GGG(T129, T135, T131, lessc54_out_gg(T129, T135)) → U10_GGG(T129, T135, T131, in1_in_gg(T135, T131))
U9_GGG(T129, T135, T131, lessc54_out_gg(T129, T135)) → IN1_IN_GG(T135, T131)
IN1_IN_GG(0, tree(s(T171), T164, T165)) → U14_GG(T171, T164, T165, in10_in_g(T164))
IN1_IN_GG(s(T186), tree(s(T185), T164, T165)) → U15_GG(T186, T185, T164, T165, p40_in_ggg(T186, T185, T164))
IN1_IN_GG(T204, tree(T201, T202, T203)) → U16_GG(T204, T201, T202, T203, p53_in_ggg(T201, T204, T203))
IN1_IN_AG(T132, tree(T129, T130, T131)) → U13_AG(T132, T129, T130, T131, p53_in_gag(T129, T132, T131))
IN1_IN_AG(T132, tree(T129, T130, T131)) → P53_IN_GAG(T129, T132, T131)
P53_IN_GAG(T129, T132, T131) → U8_GAG(T129, T132, T131, less54_in_ga(T129, T132))
P53_IN_GAG(T129, T132, T131) → LESS54_IN_GA(T129, T132)
LESS54_IN_GA(s(T147), s(T149)) → U4_GA(T147, T149, less54_in_ga(T147, T149))
LESS54_IN_GA(s(T147), s(T149)) → LESS54_IN_GA(T147, T149)
P53_IN_GAG(T129, T135, T131) → U9_GAG(T129, T135, T131, lessc54_in_ga(T129, T135))
U9_GAG(T129, T135, T131, lessc54_out_ga(T129, T135)) → U10_GAG(T129, T135, T131, in1_in_ag(T135, T131))
U9_GAG(T129, T135, T131, lessc54_out_ga(T129, T135)) → IN1_IN_AG(T135, T131)
IN1_IN_AG(0, tree(s(T171), T164, T165)) → U14_AG(T171, T164, T165, in10_in_g(T164))
IN1_IN_AG(s(T186), tree(s(T185), T164, T165)) → U15_AG(T186, T185, T164, T165, p40_in_agg(T186, T185, T164))
IN1_IN_AG(T204, tree(T201, T202, T203)) → U16_AG(T204, T201, T202, T203, p53_in_gag(T201, T204, T203))

The TRS R consists of the following rules:

lessc22_in_g(s(T60)) → lessc22_out_g(s(T60))
lessc42_in_ag(0, s(T101)) → lessc42_out_ag(0, s(T101))
lessc42_in_ag(s(T108), s(T107)) → U26_ag(T108, T107, lessc42_in_ag(T108, T107))
U26_ag(T108, T107, lessc42_out_ag(T108, T107)) → lessc42_out_ag(s(T108), s(T107))
lessc42_in_gg(0, s(T101)) → lessc42_out_gg(0, s(T101))
lessc42_in_gg(s(T108), s(T107)) → U26_gg(T108, T107, lessc42_in_gg(T108, T107))
U26_gg(T108, T107, lessc42_out_gg(T108, T107)) → lessc42_out_gg(s(T108), s(T107))
lessc54_in_gg(0, s(T142)) → lessc54_out_gg(0, s(T142))
lessc54_in_gg(s(T147), s(T149)) → U27_gg(T147, T149, lessc54_in_gg(T147, T149))
U27_gg(T147, T149, lessc54_out_gg(T147, T149)) → lessc54_out_gg(s(T147), s(T149))
lessc54_in_ga(0, s(T142)) → lessc54_out_ga(0, s(T142))
lessc54_in_ga(s(T147), s(T149)) → U27_ga(T147, T149, lessc54_in_ga(T147, T149))
U27_ga(T147, T149, lessc54_out_ga(T147, T149)) → lessc54_out_ga(s(T147), s(T149))

The argument filtering Pi contains the following mapping:
in1_in_ag(x1, x2)  =  in1_in_ag(x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
s(x1)  =  s(x1)
in10_in_g(x1)  =  in10_in_g(x1)
lessc22_in_g(x1)  =  lessc22_in_g(x1)
lessc22_out_g(x1)  =  lessc22_out_g(x1)
p40_in_agg(x1, x2, x3)  =  p40_in_agg(x2, x3)
less42_in_ag(x1, x2)  =  less42_in_ag(x2)
lessc42_in_ag(x1, x2)  =  lessc42_in_ag(x2)
lessc42_out_ag(x1, x2)  =  lessc42_out_ag(x1, x2)
U26_ag(x1, x2, x3)  =  U26_ag(x2, x3)
in1_in_gg(x1, x2)  =  in1_in_gg(x1, x2)
0  =  0
p40_in_ggg(x1, x2, x3)  =  p40_in_ggg(x1, x2, x3)
less42_in_gg(x1, x2)  =  less42_in_gg(x1, x2)
lessc42_in_gg(x1, x2)  =  lessc42_in_gg(x1, x2)
lessc42_out_gg(x1, x2)  =  lessc42_out_gg(x1, x2)
U26_gg(x1, x2, x3)  =  U26_gg(x1, x2, x3)
p53_in_ggg(x1, x2, x3)  =  p53_in_ggg(x1, x2, x3)
less54_in_gg(x1, x2)  =  less54_in_gg(x1, x2)
lessc54_in_gg(x1, x2)  =  lessc54_in_gg(x1, x2)
lessc54_out_gg(x1, x2)  =  lessc54_out_gg(x1, x2)
U27_gg(x1, x2, x3)  =  U27_gg(x1, x2, x3)
p53_in_gag(x1, x2, x3)  =  p53_in_gag(x1, x3)
less54_in_ga(x1, x2)  =  less54_in_ga(x1)
lessc54_in_ga(x1, x2)  =  lessc54_in_ga(x1)
lessc54_out_ga(x1, x2)  =  lessc54_out_ga(x1)
U27_ga(x1, x2, x3)  =  U27_ga(x1, x3)
IN1_IN_AG(x1, x2)  =  IN1_IN_AG(x2)
U11_AG(x1, x2, x3, x4)  =  U11_AG(x1, x2, x3, x4)
IN10_IN_G(x1)  =  IN10_IN_G(x1)
U1_G(x1, x2, x3, x4)  =  U1_G(x1, x2, x3, x4)
U2_G(x1, x2, x3, x4)  =  U2_G(x1, x2, x3, x4)
U12_AG(x1, x2, x3, x4, x5)  =  U12_AG(x2, x3, x4, x5)
P40_IN_AGG(x1, x2, x3)  =  P40_IN_AGG(x2, x3)
U5_AGG(x1, x2, x3, x4)  =  U5_AGG(x2, x3, x4)
LESS42_IN_AG(x1, x2)  =  LESS42_IN_AG(x2)
U3_AG(x1, x2, x3)  =  U3_AG(x2, x3)
U6_AGG(x1, x2, x3, x4)  =  U6_AGG(x2, x3, x4)
U7_AGG(x1, x2, x3, x4)  =  U7_AGG(x1, x2, x3, x4)
IN1_IN_GG(x1, x2)  =  IN1_IN_GG(x1, x2)
U11_GG(x1, x2, x3, x4)  =  U11_GG(x1, x2, x3, x4)
U12_GG(x1, x2, x3, x4, x5)  =  U12_GG(x1, x2, x3, x4, x5)
P40_IN_GGG(x1, x2, x3)  =  P40_IN_GGG(x1, x2, x3)
U5_GGG(x1, x2, x3, x4)  =  U5_GGG(x1, x2, x3, x4)
LESS42_IN_GG(x1, x2)  =  LESS42_IN_GG(x1, x2)
U3_GG(x1, x2, x3)  =  U3_GG(x1, x2, x3)
U6_GGG(x1, x2, x3, x4)  =  U6_GGG(x1, x2, x3, x4)
U7_GGG(x1, x2, x3, x4)  =  U7_GGG(x1, x2, x3, x4)
U13_GG(x1, x2, x3, x4, x5)  =  U13_GG(x1, x2, x3, x4, x5)
P53_IN_GGG(x1, x2, x3)  =  P53_IN_GGG(x1, x2, x3)
U8_GGG(x1, x2, x3, x4)  =  U8_GGG(x1, x2, x3, x4)
LESS54_IN_GG(x1, x2)  =  LESS54_IN_GG(x1, x2)
U4_GG(x1, x2, x3)  =  U4_GG(x1, x2, x3)
U9_GGG(x1, x2, x3, x4)  =  U9_GGG(x1, x2, x3, x4)
U10_GGG(x1, x2, x3, x4)  =  U10_GGG(x1, x2, x3, x4)
U14_GG(x1, x2, x3, x4)  =  U14_GG(x1, x2, x3, x4)
U15_GG(x1, x2, x3, x4, x5)  =  U15_GG(x1, x2, x3, x4, x5)
U16_GG(x1, x2, x3, x4, x5)  =  U16_GG(x1, x2, x3, x4, x5)
U13_AG(x1, x2, x3, x4, x5)  =  U13_AG(x2, x3, x4, x5)
P53_IN_GAG(x1, x2, x3)  =  P53_IN_GAG(x1, x3)
U8_GAG(x1, x2, x3, x4)  =  U8_GAG(x1, x3, x4)
LESS54_IN_GA(x1, x2)  =  LESS54_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
U9_GAG(x1, x2, x3, x4)  =  U9_GAG(x1, x3, x4)
U10_GAG(x1, x2, x3, x4)  =  U10_GAG(x1, x3, x4)
U14_AG(x1, x2, x3, x4)  =  U14_AG(x1, x2, x3, x4)
U15_AG(x1, x2, x3, x4, x5)  =  U15_AG(x2, x3, x4, x5)
U16_AG(x1, x2, x3, x4, x5)  =  U16_AG(x2, x3, x4, x5)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 7 SCCs with 34 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

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

LESS54_IN_GA(s(T147), s(T149)) → LESS54_IN_GA(T147, T149)

The TRS R consists of the following rules:

lessc22_in_g(s(T60)) → lessc22_out_g(s(T60))
lessc42_in_ag(0, s(T101)) → lessc42_out_ag(0, s(T101))
lessc42_in_ag(s(T108), s(T107)) → U26_ag(T108, T107, lessc42_in_ag(T108, T107))
U26_ag(T108, T107, lessc42_out_ag(T108, T107)) → lessc42_out_ag(s(T108), s(T107))
lessc42_in_gg(0, s(T101)) → lessc42_out_gg(0, s(T101))
lessc42_in_gg(s(T108), s(T107)) → U26_gg(T108, T107, lessc42_in_gg(T108, T107))
U26_gg(T108, T107, lessc42_out_gg(T108, T107)) → lessc42_out_gg(s(T108), s(T107))
lessc54_in_gg(0, s(T142)) → lessc54_out_gg(0, s(T142))
lessc54_in_gg(s(T147), s(T149)) → U27_gg(T147, T149, lessc54_in_gg(T147, T149))
U27_gg(T147, T149, lessc54_out_gg(T147, T149)) → lessc54_out_gg(s(T147), s(T149))
lessc54_in_ga(0, s(T142)) → lessc54_out_ga(0, s(T142))
lessc54_in_ga(s(T147), s(T149)) → U27_ga(T147, T149, lessc54_in_ga(T147, T149))
U27_ga(T147, T149, lessc54_out_ga(T147, T149)) → lessc54_out_ga(s(T147), s(T149))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
lessc22_in_g(x1)  =  lessc22_in_g(x1)
lessc22_out_g(x1)  =  lessc22_out_g(x1)
lessc42_in_ag(x1, x2)  =  lessc42_in_ag(x2)
lessc42_out_ag(x1, x2)  =  lessc42_out_ag(x1, x2)
U26_ag(x1, x2, x3)  =  U26_ag(x2, x3)
0  =  0
lessc42_in_gg(x1, x2)  =  lessc42_in_gg(x1, x2)
lessc42_out_gg(x1, x2)  =  lessc42_out_gg(x1, x2)
U26_gg(x1, x2, x3)  =  U26_gg(x1, x2, x3)
lessc54_in_gg(x1, x2)  =  lessc54_in_gg(x1, x2)
lessc54_out_gg(x1, x2)  =  lessc54_out_gg(x1, x2)
U27_gg(x1, x2, x3)  =  U27_gg(x1, x2, x3)
lessc54_in_ga(x1, x2)  =  lessc54_in_ga(x1)
lessc54_out_ga(x1, x2)  =  lessc54_out_ga(x1)
U27_ga(x1, x2, x3)  =  U27_ga(x1, x3)
LESS54_IN_GA(x1, x2)  =  LESS54_IN_GA(x1)

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

(10) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(11) Obligation:

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

LESS54_IN_GA(s(T147), s(T149)) → LESS54_IN_GA(T147, T149)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
LESS54_IN_GA(x1, x2)  =  LESS54_IN_GA(x1)

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

(12) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(13) Obligation:

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

LESS54_IN_GA(s(T147)) → LESS54_IN_GA(T147)

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

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

• LESS54_IN_GA(s(T147)) → LESS54_IN_GA(T147)
  The graph contains the following edges 1 > 1

(15) YES

(16) Obligation:

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

LESS54_IN_GG(s(T147), s(T149)) → LESS54_IN_GG(T147, T149)

The TRS R consists of the following rules:

lessc22_in_g(s(T60)) → lessc22_out_g(s(T60))
lessc42_in_ag(0, s(T101)) → lessc42_out_ag(0, s(T101))
lessc42_in_ag(s(T108), s(T107)) → U26_ag(T108, T107, lessc42_in_ag(T108, T107))
U26_ag(T108, T107, lessc42_out_ag(T108, T107)) → lessc42_out_ag(s(T108), s(T107))
lessc42_in_gg(0, s(T101)) → lessc42_out_gg(0, s(T101))
lessc42_in_gg(s(T108), s(T107)) → U26_gg(T108, T107, lessc42_in_gg(T108, T107))
U26_gg(T108, T107, lessc42_out_gg(T108, T107)) → lessc42_out_gg(s(T108), s(T107))
lessc54_in_gg(0, s(T142)) → lessc54_out_gg(0, s(T142))
lessc54_in_gg(s(T147), s(T149)) → U27_gg(T147, T149, lessc54_in_gg(T147, T149))
U27_gg(T147, T149, lessc54_out_gg(T147, T149)) → lessc54_out_gg(s(T147), s(T149))
lessc54_in_ga(0, s(T142)) → lessc54_out_ga(0, s(T142))
lessc54_in_ga(s(T147), s(T149)) → U27_ga(T147, T149, lessc54_in_ga(T147, T149))
U27_ga(T147, T149, lessc54_out_ga(T147, T149)) → lessc54_out_ga(s(T147), s(T149))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
lessc22_in_g(x1)  =  lessc22_in_g(x1)
lessc22_out_g(x1)  =  lessc22_out_g(x1)
lessc42_in_ag(x1, x2)  =  lessc42_in_ag(x2)
lessc42_out_ag(x1, x2)  =  lessc42_out_ag(x1, x2)
U26_ag(x1, x2, x3)  =  U26_ag(x2, x3)
0  =  0
lessc42_in_gg(x1, x2)  =  lessc42_in_gg(x1, x2)
lessc42_out_gg(x1, x2)  =  lessc42_out_gg(x1, x2)
U26_gg(x1, x2, x3)  =  U26_gg(x1, x2, x3)
lessc54_in_gg(x1, x2)  =  lessc54_in_gg(x1, x2)
lessc54_out_gg(x1, x2)  =  lessc54_out_gg(x1, x2)
U27_gg(x1, x2, x3)  =  U27_gg(x1, x2, x3)
lessc54_in_ga(x1, x2)  =  lessc54_in_ga(x1)
lessc54_out_ga(x1, x2)  =  lessc54_out_ga(x1)
U27_ga(x1, x2, x3)  =  U27_ga(x1, x3)
LESS54_IN_GG(x1, x2)  =  LESS54_IN_GG(x1, x2)

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

(17) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(18) Obligation:

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

LESS54_IN_GG(s(T147), s(T149)) → LESS54_IN_GG(T147, T149)

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

(19) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(20) Obligation:

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

LESS54_IN_GG(s(T147), s(T149)) → LESS54_IN_GG(T147, T149)

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

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

• LESS54_IN_GG(s(T147), s(T149)) → LESS54_IN_GG(T147, T149)
  The graph contains the following edges 1 > 1, 2 > 2

(22) YES

(23) Obligation:

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

LESS42_IN_GG(s(T108), s(T107)) → LESS42_IN_GG(T108, T107)

The TRS R consists of the following rules:

lessc22_in_g(s(T60)) → lessc22_out_g(s(T60))
lessc42_in_ag(0, s(T101)) → lessc42_out_ag(0, s(T101))
lessc42_in_ag(s(T108), s(T107)) → U26_ag(T108, T107, lessc42_in_ag(T108, T107))
U26_ag(T108, T107, lessc42_out_ag(T108, T107)) → lessc42_out_ag(s(T108), s(T107))
lessc42_in_gg(0, s(T101)) → lessc42_out_gg(0, s(T101))
lessc42_in_gg(s(T108), s(T107)) → U26_gg(T108, T107, lessc42_in_gg(T108, T107))
U26_gg(T108, T107, lessc42_out_gg(T108, T107)) → lessc42_out_gg(s(T108), s(T107))
lessc54_in_gg(0, s(T142)) → lessc54_out_gg(0, s(T142))
lessc54_in_gg(s(T147), s(T149)) → U27_gg(T147, T149, lessc54_in_gg(T147, T149))
U27_gg(T147, T149, lessc54_out_gg(T147, T149)) → lessc54_out_gg(s(T147), s(T149))
lessc54_in_ga(0, s(T142)) → lessc54_out_ga(0, s(T142))
lessc54_in_ga(s(T147), s(T149)) → U27_ga(T147, T149, lessc54_in_ga(T147, T149))
U27_ga(T147, T149, lessc54_out_ga(T147, T149)) → lessc54_out_ga(s(T147), s(T149))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
lessc22_in_g(x1)  =  lessc22_in_g(x1)
lessc22_out_g(x1)  =  lessc22_out_g(x1)
lessc42_in_ag(x1, x2)  =  lessc42_in_ag(x2)
lessc42_out_ag(x1, x2)  =  lessc42_out_ag(x1, x2)
U26_ag(x1, x2, x3)  =  U26_ag(x2, x3)
0  =  0
lessc42_in_gg(x1, x2)  =  lessc42_in_gg(x1, x2)
lessc42_out_gg(x1, x2)  =  lessc42_out_gg(x1, x2)
U26_gg(x1, x2, x3)  =  U26_gg(x1, x2, x3)
lessc54_in_gg(x1, x2)  =  lessc54_in_gg(x1, x2)
lessc54_out_gg(x1, x2)  =  lessc54_out_gg(x1, x2)
U27_gg(x1, x2, x3)  =  U27_gg(x1, x2, x3)
lessc54_in_ga(x1, x2)  =  lessc54_in_ga(x1)
lessc54_out_ga(x1, x2)  =  lessc54_out_ga(x1)
U27_ga(x1, x2, x3)  =  U27_ga(x1, x3)
LESS42_IN_GG(x1, x2)  =  LESS42_IN_GG(x1, x2)

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

(24) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(25) Obligation:

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

LESS42_IN_GG(s(T108), s(T107)) → LESS42_IN_GG(T108, T107)

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

(26) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(27) Obligation:

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

LESS42_IN_GG(s(T108), s(T107)) → LESS42_IN_GG(T108, T107)

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

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

• LESS42_IN_GG(s(T108), s(T107)) → LESS42_IN_GG(T108, T107)
  The graph contains the following edges 1 > 1, 2 > 2

(29) YES

(30) Obligation:

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

LESS42_IN_AG(s(T108), s(T107)) → LESS42_IN_AG(T108, T107)

The TRS R consists of the following rules:

lessc22_in_g(s(T60)) → lessc22_out_g(s(T60))
lessc42_in_ag(0, s(T101)) → lessc42_out_ag(0, s(T101))
lessc42_in_ag(s(T108), s(T107)) → U26_ag(T108, T107, lessc42_in_ag(T108, T107))
U26_ag(T108, T107, lessc42_out_ag(T108, T107)) → lessc42_out_ag(s(T108), s(T107))
lessc42_in_gg(0, s(T101)) → lessc42_out_gg(0, s(T101))
lessc42_in_gg(s(T108), s(T107)) → U26_gg(T108, T107, lessc42_in_gg(T108, T107))
U26_gg(T108, T107, lessc42_out_gg(T108, T107)) → lessc42_out_gg(s(T108), s(T107))
lessc54_in_gg(0, s(T142)) → lessc54_out_gg(0, s(T142))
lessc54_in_gg(s(T147), s(T149)) → U27_gg(T147, T149, lessc54_in_gg(T147, T149))
U27_gg(T147, T149, lessc54_out_gg(T147, T149)) → lessc54_out_gg(s(T147), s(T149))
lessc54_in_ga(0, s(T142)) → lessc54_out_ga(0, s(T142))
lessc54_in_ga(s(T147), s(T149)) → U27_ga(T147, T149, lessc54_in_ga(T147, T149))
U27_ga(T147, T149, lessc54_out_ga(T147, T149)) → lessc54_out_ga(s(T147), s(T149))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
lessc22_in_g(x1)  =  lessc22_in_g(x1)
lessc22_out_g(x1)  =  lessc22_out_g(x1)
lessc42_in_ag(x1, x2)  =  lessc42_in_ag(x2)
lessc42_out_ag(x1, x2)  =  lessc42_out_ag(x1, x2)
U26_ag(x1, x2, x3)  =  U26_ag(x2, x3)
0  =  0
lessc42_in_gg(x1, x2)  =  lessc42_in_gg(x1, x2)
lessc42_out_gg(x1, x2)  =  lessc42_out_gg(x1, x2)
U26_gg(x1, x2, x3)  =  U26_gg(x1, x2, x3)
lessc54_in_gg(x1, x2)  =  lessc54_in_gg(x1, x2)
lessc54_out_gg(x1, x2)  =  lessc54_out_gg(x1, x2)
U27_gg(x1, x2, x3)  =  U27_gg(x1, x2, x3)
lessc54_in_ga(x1, x2)  =  lessc54_in_ga(x1)
lessc54_out_ga(x1, x2)  =  lessc54_out_ga(x1)
U27_ga(x1, x2, x3)  =  U27_ga(x1, x3)
LESS42_IN_AG(x1, x2)  =  LESS42_IN_AG(x2)

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

(31) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(32) Obligation:

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

LESS42_IN_AG(s(T108), s(T107)) → LESS42_IN_AG(T108, T107)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
LESS42_IN_AG(x1, x2)  =  LESS42_IN_AG(x2)

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

(33) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(34) Obligation:

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

LESS42_IN_AG(s(T107)) → LESS42_IN_AG(T107)

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

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

• LESS42_IN_AG(s(T107)) → LESS42_IN_AG(T107)
  The graph contains the following edges 1 > 1

(36) YES

(37) Obligation:

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

U1_G(T49, T50, T51, lessc22_out_g(T49)) → IN10_IN_G(T50)
IN10_IN_G(tree(T49, T50, T51)) → U1_G(T49, T50, T51, lessc22_in_g(T49))

The TRS R consists of the following rules:

lessc22_in_g(s(T60)) → lessc22_out_g(s(T60))
lessc42_in_ag(0, s(T101)) → lessc42_out_ag(0, s(T101))
lessc42_in_ag(s(T108), s(T107)) → U26_ag(T108, T107, lessc42_in_ag(T108, T107))
U26_ag(T108, T107, lessc42_out_ag(T108, T107)) → lessc42_out_ag(s(T108), s(T107))
lessc42_in_gg(0, s(T101)) → lessc42_out_gg(0, s(T101))
lessc42_in_gg(s(T108), s(T107)) → U26_gg(T108, T107, lessc42_in_gg(T108, T107))
U26_gg(T108, T107, lessc42_out_gg(T108, T107)) → lessc42_out_gg(s(T108), s(T107))
lessc54_in_gg(0, s(T142)) → lessc54_out_gg(0, s(T142))
lessc54_in_gg(s(T147), s(T149)) → U27_gg(T147, T149, lessc54_in_gg(T147, T149))
U27_gg(T147, T149, lessc54_out_gg(T147, T149)) → lessc54_out_gg(s(T147), s(T149))
lessc54_in_ga(0, s(T142)) → lessc54_out_ga(0, s(T142))
lessc54_in_ga(s(T147), s(T149)) → U27_ga(T147, T149, lessc54_in_ga(T147, T149))
U27_ga(T147, T149, lessc54_out_ga(T147, T149)) → lessc54_out_ga(s(T147), s(T149))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
s(x1)  =  s(x1)
lessc22_in_g(x1)  =  lessc22_in_g(x1)
lessc22_out_g(x1)  =  lessc22_out_g(x1)
lessc42_in_ag(x1, x2)  =  lessc42_in_ag(x2)
lessc42_out_ag(x1, x2)  =  lessc42_out_ag(x1, x2)
U26_ag(x1, x2, x3)  =  U26_ag(x2, x3)
0  =  0
lessc42_in_gg(x1, x2)  =  lessc42_in_gg(x1, x2)
lessc42_out_gg(x1, x2)  =  lessc42_out_gg(x1, x2)
U26_gg(x1, x2, x3)  =  U26_gg(x1, x2, x3)
lessc54_in_gg(x1, x2)  =  lessc54_in_gg(x1, x2)
lessc54_out_gg(x1, x2)  =  lessc54_out_gg(x1, x2)
U27_gg(x1, x2, x3)  =  U27_gg(x1, x2, x3)
lessc54_in_ga(x1, x2)  =  lessc54_in_ga(x1)
lessc54_out_ga(x1, x2)  =  lessc54_out_ga(x1)
U27_ga(x1, x2, x3)  =  U27_ga(x1, x3)
IN10_IN_G(x1)  =  IN10_IN_G(x1)
U1_G(x1, x2, x3, x4)  =  U1_G(x1, x2, x3, x4)

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

(38) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(39) Obligation:

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

U1_G(T49, T50, T51, lessc22_out_g(T49)) → IN10_IN_G(T50)
IN10_IN_G(tree(T49, T50, T51)) → U1_G(T49, T50, T51, lessc22_in_g(T49))

The TRS R consists of the following rules:

lessc22_in_g(s(T60)) → lessc22_out_g(s(T60))

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

(40) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(41) Obligation:

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

U1_G(T49, T50, T51, lessc22_out_g(T49)) → IN10_IN_G(T50)
IN10_IN_G(tree(T49, T50, T51)) → U1_G(T49, T50, T51, lessc22_in_g(T49))

The TRS R consists of the following rules:

lessc22_in_g(s(T60)) → lessc22_out_g(s(T60))

The set Q consists of the following terms:

lessc22_in_g(x0)

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

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

• IN10_IN_G(tree(T49, T50, T51)) → U1_G(T49, T50, T51, lessc22_in_g(T49))
  The graph contains the following edges 1 > 1, 1 > 2, 1 > 3

• U1_G(T49, T50, T51, lessc22_out_g(T49)) → IN10_IN_G(T50)
  The graph contains the following edges 2 >= 1

(43) YES

(44) Obligation:

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

IN1_IN_GG(s(T91), tree(s(T90), T15, T16)) → P40_IN_GGG(T91, T90, T15)
P40_IN_GGG(T94, T90, T15) → U6_GGG(T94, T90, T15, lessc42_in_gg(T94, T90))
U6_GGG(T94, T90, T15, lessc42_out_gg(T94, T90)) → IN1_IN_GG(s(T94), T15)
IN1_IN_GG(T132, tree(T129, T130, T131)) → P53_IN_GGG(T129, T132, T131)
P53_IN_GGG(T129, T135, T131) → U9_GGG(T129, T135, T131, lessc54_in_gg(T129, T135))
U9_GGG(T129, T135, T131, lessc54_out_gg(T129, T135)) → IN1_IN_GG(T135, T131)

The TRS R consists of the following rules:

lessc22_in_g(s(T60)) → lessc22_out_g(s(T60))
lessc42_in_ag(0, s(T101)) → lessc42_out_ag(0, s(T101))
lessc42_in_ag(s(T108), s(T107)) → U26_ag(T108, T107, lessc42_in_ag(T108, T107))
U26_ag(T108, T107, lessc42_out_ag(T108, T107)) → lessc42_out_ag(s(T108), s(T107))
lessc42_in_gg(0, s(T101)) → lessc42_out_gg(0, s(T101))
lessc42_in_gg(s(T108), s(T107)) → U26_gg(T108, T107, lessc42_in_gg(T108, T107))
U26_gg(T108, T107, lessc42_out_gg(T108, T107)) → lessc42_out_gg(s(T108), s(T107))
lessc54_in_gg(0, s(T142)) → lessc54_out_gg(0, s(T142))
lessc54_in_gg(s(T147), s(T149)) → U27_gg(T147, T149, lessc54_in_gg(T147, T149))
U27_gg(T147, T149, lessc54_out_gg(T147, T149)) → lessc54_out_gg(s(T147), s(T149))
lessc54_in_ga(0, s(T142)) → lessc54_out_ga(0, s(T142))
lessc54_in_ga(s(T147), s(T149)) → U27_ga(T147, T149, lessc54_in_ga(T147, T149))
U27_ga(T147, T149, lessc54_out_ga(T147, T149)) → lessc54_out_ga(s(T147), s(T149))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
s(x1)  =  s(x1)
lessc22_in_g(x1)  =  lessc22_in_g(x1)
lessc22_out_g(x1)  =  lessc22_out_g(x1)
lessc42_in_ag(x1, x2)  =  lessc42_in_ag(x2)
lessc42_out_ag(x1, x2)  =  lessc42_out_ag(x1, x2)
U26_ag(x1, x2, x3)  =  U26_ag(x2, x3)
0  =  0
lessc42_in_gg(x1, x2)  =  lessc42_in_gg(x1, x2)
lessc42_out_gg(x1, x2)  =  lessc42_out_gg(x1, x2)
U26_gg(x1, x2, x3)  =  U26_gg(x1, x2, x3)
lessc54_in_gg(x1, x2)  =  lessc54_in_gg(x1, x2)
lessc54_out_gg(x1, x2)  =  lessc54_out_gg(x1, x2)
U27_gg(x1, x2, x3)  =  U27_gg(x1, x2, x3)
lessc54_in_ga(x1, x2)  =  lessc54_in_ga(x1)
lessc54_out_ga(x1, x2)  =  lessc54_out_ga(x1)
U27_ga(x1, x2, x3)  =  U27_ga(x1, x3)
IN1_IN_GG(x1, x2)  =  IN1_IN_GG(x1, x2)
P40_IN_GGG(x1, x2, x3)  =  P40_IN_GGG(x1, x2, x3)
U6_GGG(x1, x2, x3, x4)  =  U6_GGG(x1, x2, x3, x4)
P53_IN_GGG(x1, x2, x3)  =  P53_IN_GGG(x1, x2, x3)
U9_GGG(x1, x2, x3, x4)  =  U9_GGG(x1, x2, x3, x4)

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

(45) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(46) Obligation:

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

IN1_IN_GG(s(T91), tree(s(T90), T15, T16)) → P40_IN_GGG(T91, T90, T15)
P40_IN_GGG(T94, T90, T15) → U6_GGG(T94, T90, T15, lessc42_in_gg(T94, T90))
U6_GGG(T94, T90, T15, lessc42_out_gg(T94, T90)) → IN1_IN_GG(s(T94), T15)
IN1_IN_GG(T132, tree(T129, T130, T131)) → P53_IN_GGG(T129, T132, T131)
P53_IN_GGG(T129, T135, T131) → U9_GGG(T129, T135, T131, lessc54_in_gg(T129, T135))
U9_GGG(T129, T135, T131, lessc54_out_gg(T129, T135)) → IN1_IN_GG(T135, T131)

The TRS R consists of the following rules:

lessc42_in_gg(0, s(T101)) → lessc42_out_gg(0, s(T101))
lessc42_in_gg(s(T108), s(T107)) → U26_gg(T108, T107, lessc42_in_gg(T108, T107))
lessc54_in_gg(0, s(T142)) → lessc54_out_gg(0, s(T142))
lessc54_in_gg(s(T147), s(T149)) → U27_gg(T147, T149, lessc54_in_gg(T147, T149))
U26_gg(T108, T107, lessc42_out_gg(T108, T107)) → lessc42_out_gg(s(T108), s(T107))
U27_gg(T147, T149, lessc54_out_gg(T147, T149)) → lessc54_out_gg(s(T147), s(T149))

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

(47) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(48) Obligation:

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

IN1_IN_GG(s(T91), tree(s(T90), T15, T16)) → P40_IN_GGG(T91, T90, T15)
P40_IN_GGG(T94, T90, T15) → U6_GGG(T94, T90, T15, lessc42_in_gg(T94, T90))
U6_GGG(T94, T90, T15, lessc42_out_gg(T94, T90)) → IN1_IN_GG(s(T94), T15)
IN1_IN_GG(T132, tree(T129, T130, T131)) → P53_IN_GGG(T129, T132, T131)
P53_IN_GGG(T129, T135, T131) → U9_GGG(T129, T135, T131, lessc54_in_gg(T129, T135))
U9_GGG(T129, T135, T131, lessc54_out_gg(T129, T135)) → IN1_IN_GG(T135, T131)

The TRS R consists of the following rules:

lessc42_in_gg(0, s(T101)) → lessc42_out_gg(0, s(T101))
lessc42_in_gg(s(T108), s(T107)) → U26_gg(T108, T107, lessc42_in_gg(T108, T107))
lessc54_in_gg(0, s(T142)) → lessc54_out_gg(0, s(T142))
lessc54_in_gg(s(T147), s(T149)) → U27_gg(T147, T149, lessc54_in_gg(T147, T149))
U26_gg(T108, T107, lessc42_out_gg(T108, T107)) → lessc42_out_gg(s(T108), s(T107))
U27_gg(T147, T149, lessc54_out_gg(T147, T149)) → lessc54_out_gg(s(T147), s(T149))

The set Q consists of the following terms:

lessc42_in_gg(x0, x1)
lessc54_in_gg(x0, x1)
U26_gg(x0, x1, x2)
U27_gg(x0, x1, x2)

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

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

• P40_IN_GGG(T94, T90, T15) → U6_GGG(T94, T90, T15, lessc42_in_gg(T94, T90))
  The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3

• U6_GGG(T94, T90, T15, lessc42_out_gg(T94, T90)) → IN1_IN_GG(s(T94), T15)
  The graph contains the following edges 3 >= 2

• U9_GGG(T129, T135, T131, lessc54_out_gg(T129, T135)) → IN1_IN_GG(T135, T131)
  The graph contains the following edges 2 >= 1, 4 > 1, 3 >= 2

• IN1_IN_GG(s(T91), tree(s(T90), T15, T16)) → P40_IN_GGG(T91, T90, T15)
  The graph contains the following edges 1 > 1, 2 > 2, 2 > 3

• IN1_IN_GG(T132, tree(T129, T130, T131)) → P53_IN_GGG(T129, T132, T131)
  The graph contains the following edges 2 > 1, 1 >= 2, 2 > 3

• P53_IN_GGG(T129, T135, T131) → U9_GGG(T129, T135, T131, lessc54_in_gg(T129, T135))
  The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3

(50) YES

(51) Obligation:

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

IN1_IN_AG(T132, tree(T129, T130, T131)) → P53_IN_GAG(T129, T132, T131)
P53_IN_GAG(T129, T135, T131) → U9_GAG(T129, T135, T131, lessc54_in_ga(T129, T135))
U9_GAG(T129, T135, T131, lessc54_out_ga(T129, T135)) → IN1_IN_AG(T135, T131)

The TRS R consists of the following rules:

lessc22_in_g(s(T60)) → lessc22_out_g(s(T60))
lessc42_in_ag(0, s(T101)) → lessc42_out_ag(0, s(T101))
lessc42_in_ag(s(T108), s(T107)) → U26_ag(T108, T107, lessc42_in_ag(T108, T107))
U26_ag(T108, T107, lessc42_out_ag(T108, T107)) → lessc42_out_ag(s(T108), s(T107))
lessc42_in_gg(0, s(T101)) → lessc42_out_gg(0, s(T101))
lessc42_in_gg(s(T108), s(T107)) → U26_gg(T108, T107, lessc42_in_gg(T108, T107))
U26_gg(T108, T107, lessc42_out_gg(T108, T107)) → lessc42_out_gg(s(T108), s(T107))
lessc54_in_gg(0, s(T142)) → lessc54_out_gg(0, s(T142))
lessc54_in_gg(s(T147), s(T149)) → U27_gg(T147, T149, lessc54_in_gg(T147, T149))
U27_gg(T147, T149, lessc54_out_gg(T147, T149)) → lessc54_out_gg(s(T147), s(T149))
lessc54_in_ga(0, s(T142)) → lessc54_out_ga(0, s(T142))
lessc54_in_ga(s(T147), s(T149)) → U27_ga(T147, T149, lessc54_in_ga(T147, T149))
U27_ga(T147, T149, lessc54_out_ga(T147, T149)) → lessc54_out_ga(s(T147), s(T149))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
s(x1)  =  s(x1)
lessc22_in_g(x1)  =  lessc22_in_g(x1)
lessc22_out_g(x1)  =  lessc22_out_g(x1)
lessc42_in_ag(x1, x2)  =  lessc42_in_ag(x2)
lessc42_out_ag(x1, x2)  =  lessc42_out_ag(x1, x2)
U26_ag(x1, x2, x3)  =  U26_ag(x2, x3)
0  =  0
lessc42_in_gg(x1, x2)  =  lessc42_in_gg(x1, x2)
lessc42_out_gg(x1, x2)  =  lessc42_out_gg(x1, x2)
U26_gg(x1, x2, x3)  =  U26_gg(x1, x2, x3)
lessc54_in_gg(x1, x2)  =  lessc54_in_gg(x1, x2)
lessc54_out_gg(x1, x2)  =  lessc54_out_gg(x1, x2)
U27_gg(x1, x2, x3)  =  U27_gg(x1, x2, x3)
lessc54_in_ga(x1, x2)  =  lessc54_in_ga(x1)
lessc54_out_ga(x1, x2)  =  lessc54_out_ga(x1)
U27_ga(x1, x2, x3)  =  U27_ga(x1, x3)
IN1_IN_AG(x1, x2)  =  IN1_IN_AG(x2)
P53_IN_GAG(x1, x2, x3)  =  P53_IN_GAG(x1, x3)
U9_GAG(x1, x2, x3, x4)  =  U9_GAG(x1, x3, x4)

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

(52) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(53) Obligation:

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

IN1_IN_AG(T132, tree(T129, T130, T131)) → P53_IN_GAG(T129, T132, T131)
P53_IN_GAG(T129, T135, T131) → U9_GAG(T129, T135, T131, lessc54_in_ga(T129, T135))
U9_GAG(T129, T135, T131, lessc54_out_ga(T129, T135)) → IN1_IN_AG(T135, T131)

The TRS R consists of the following rules:

lessc54_in_ga(0, s(T142)) → lessc54_out_ga(0, s(T142))
lessc54_in_ga(s(T147), s(T149)) → U27_ga(T147, T149, lessc54_in_ga(T147, T149))
U27_ga(T147, T149, lessc54_out_ga(T147, T149)) → lessc54_out_ga(s(T147), s(T149))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
s(x1)  =  s(x1)
0  =  0
lessc54_in_ga(x1, x2)  =  lessc54_in_ga(x1)
lessc54_out_ga(x1, x2)  =  lessc54_out_ga(x1)
U27_ga(x1, x2, x3)  =  U27_ga(x1, x3)
IN1_IN_AG(x1, x2)  =  IN1_IN_AG(x2)
P53_IN_GAG(x1, x2, x3)  =  P53_IN_GAG(x1, x3)
U9_GAG(x1, x2, x3, x4)  =  U9_GAG(x1, x3, x4)

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

(54) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(55) Obligation:

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

IN1_IN_AG(tree(T129, T130, T131)) → P53_IN_GAG(T129, T131)
P53_IN_GAG(T129, T131) → U9_GAG(T129, T131, lessc54_in_ga(T129))
U9_GAG(T129, T131, lessc54_out_ga(T129)) → IN1_IN_AG(T131)

The TRS R consists of the following rules:

lessc54_in_ga(0) → lessc54_out_ga(0)
lessc54_in_ga(s(T147)) → U27_ga(T147, lessc54_in_ga(T147))
U27_ga(T147, lessc54_out_ga(T147)) → lessc54_out_ga(s(T147))

The set Q consists of the following terms:

lessc54_in_ga(x0)
U27_ga(x0, x1)

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

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

• P53_IN_GAG(T129, T131) → U9_GAG(T129, T131, lessc54_in_ga(T129))
  The graph contains the following edges 1 >= 1, 2 >= 2

• U9_GAG(T129, T131, lessc54_out_ga(T129)) → IN1_IN_AG(T131)
  The graph contains the following edges 2 >= 1

• IN1_IN_AG(tree(T129, T130, T131)) → P53_IN_GAG(T129, T131)
  The graph contains the following edges 1 > 1, 1 > 2

(57) YES