Consider the TRS R consisting of the rewrite rules

1: or(T,T) -> T
2: or(F,T) -> T
3: or(T,F) -> T
4: or(F,F) -> F
5: and(T,B) -> B
6: and(B,T) -> B
7: and(F,B) -> F
8: and(B,F) -> F
9: imp(T,B) -> B
10: imp(F,B) -> T
11: not(T) -> F
12: not(F) -> T
13: if(T,B1,B2) -> B1
14: if(F,B1,B2) -> B2
15: eq(T,T) -> T
16: eq(F,F) -> T
17: eq(T,F) -> F
18: eq(F,T) -> F
19: eqt(nil,undefined) -> F
20: eqt(nil,pid(N2)) -> F
21: eqt(nil,int(N2)) -> F
22: eqt(nil,cons(H2,T2)) -> F
23: eqt(nil,tuple(H2,T2)) -> F
24: eqt(nil,tuplenil(H2)) -> F
25: eqt(a,nil) -> F
26: eqt(a,a) -> T
27: eqt(a,excl) -> F
28: eqt(a,false) -> F
29: eqt(a,lock) -> F
30: eqt(a,locker) -> F
31: eqt(a,mcrlrecord) -> F
32: eqt(a,ok) -> F
33: eqt(a,pending) -> F
34: eqt(a,release) -> F
35: eqt(a,request) -> F
36: eqt(a,resource) -> F
37: eqt(a,tag) -> F
38: eqt(a,true) -> F
39: eqt(a,undefined) -> F
40: eqt(a,pid(N2)) -> F
41: eqt(a,int(N2)) -> F
42: eqt(a,cons(H2,T2)) -> F
43: eqt(a,tuple(H2,T2)) -> F
44: eqt(a,tuplenil(H2)) -> F
45: eqt(excl,nil) -> F
46: eqt(excl,a) -> F
47: eqt(excl,excl) -> T
48: eqt(excl,false) -> F
49: eqt(excl,lock) -> F
50: eqt(excl,locker) -> F
51: eqt(excl,mcrlrecord) -> F
52: eqt(excl,ok) -> F
53: eqt(excl,pending) -> F
54: eqt(excl,release) -> F
55: eqt(excl,request) -> F
56: eqt(excl,resource) -> F
57: eqt(excl,tag) -> F
58: eqt(excl,true) -> F
59: eqt(excl,undefined) -> F
60: eqt(excl,pid(N2)) -> F
61: eqt(excl,eqt(false,int(N2))) -> F
62: eqt(false,cons(H2,T2)) -> F
63: eqt(false,tuple(H2,T2)) -> F
64: eqt(false,tuplenil(H2)) -> F
65: eqt(lock,nil) -> F
66: eqt(lock,a) -> F
67: eqt(lock,excl) -> F
68: eqt(lock,false) -> F
69: eqt(lock,lock) -> T
70: eqt(lock,locker) -> F
71: eqt(lock,mcrlrecord) -> F
72: eqt(lock,ok) -> F
73: eqt(lock,pending) -> F
74: eqt(lock,release) -> F
75: eqt(lock,request) -> F
76: eqt(lock,resource) -> F
77: eqt(lock,tag) -> F
78: eqt(lock,true) -> F
79: eqt(lock,undefined) -> F
80: eqt(lock,pid(N2)) -> F
81: eqt(lock,int(N2)) -> F
82: eqt(lock,cons(H2,T2)) -> F
83: eqt(lock,tuple(H2,T2)) -> F
84: eqt(lock,tuplenil(H2)) -> F
85: eqt(locker,nil) -> F
86: eqt(locker,a) -> F
87: eqt(locker,excl) -> F
88: eqt(locker,false) -> F
89: eqt(locker,lock) -> F
90: eqt(locker,locker) -> T
91: eqt(locker,mcrlrecord) -> F
92: eqt(locker,ok) -> F
93: eqt(locker,pending) -> F
94: eqt(locker,release) -> F
95: eqt(locker,request) -> F
96: eqt(locker,resource) -> F
97: eqt(locker,tag) -> F
98: eqt(locker,true) -> F
99: eqt(locker,undefined) -> F
100: eqt(locker,pid(N2)) -> F
101: eqt(locker,int(N2)) -> F
102: eqt(locker,cons(H2,T2)) -> F
103: eqt(locker,tuple(H2,T2)) -> F
104: eqt(locker,tuplenil(H2)) -> F
105: eqt(mcrlrecord,nil) -> F
106: eqt(mcrlrecord,a) -> F
107: eqt(mcrlrecord,excl) -> F
108: eqt(mcrlrecord,false) -> F
109: eqt(mcrlrecord,lock) -> F
110: eqt(mcrlrecord,locker) -> F
111: eqt(mcrlrecord,mcrlrecord) -> T
112: eqt(mcrlrecord,ok) -> F
113: eqt(mcrlrecord,pending) -> F
114: eqt(mcrlrecord,release) -> F
115: eqt(mcrlrecord,request) -> F
116: eqt(mcrlrecord,resource) -> F
117: eqt(ok,resource) -> F
118: eqt(ok,tag) -> F
119: eqt(ok,true) -> F
120: eqt(ok,undefined) -> F
121: eqt(ok,pid(N2)) -> F
122: eqt(ok,int(N2)) -> F
123: eqt(ok,cons(H2,T2)) -> F
124: eqt(ok,tuple(H2,T2)) -> F
125: eqt(ok,tuplenil(H2)) -> F
126: eqt(pending,nil) -> F
127: eqt(pending,a) -> F
128: eqt(pending,excl) -> F
129: eqt(pending,false) -> F
130: eqt(pending,lock) -> F
131: eqt(pending,locker) -> F
132: eqt(pending,mcrlrecord) -> F
133: eqt(pending,ok) -> F
134: eqt(pending,pending) -> T
135: eqt(pending,release) -> F
136: eqt(pending,request) -> F
137: eqt(pending,resource) -> F
138: eqt(pending,tag) -> F
139: eqt(pending,true) -> F
140: eqt(pending,undefined) -> F
141: eqt(pending,pid(N2)) -> F
142: eqt(pending,int(N2)) -> F
143: eqt(pending,cons(H2,T2)) -> F
144: eqt(pending,tuple(H2,T2)) -> F
145: eqt(pending,tuplenil(H2)) -> F
146: eqt(release,nil) -> F
147: eqt(release,a) -> F
148: eqt(release,excl) -> F
149: eqt(release,false) -> F
150: eqt(release,lock) -> F
151: eqt(release,locker) -> F
152: eqt(release,mcrlrecord) -> F
153: eqt(release,ok) -> F
154: eqt(request,mcrlrecord) -> F
155: eqt(request,ok) -> F
156: eqt(request,pending) -> F
157: eqt(request,release) -> F
158: eqt(request,request) -> T
159: eqt(request,resource) -> F
160: eqt(request,tag) -> F
161: eqt(request,true) -> F
162: eqt(request,undefined) -> F
163: eqt(request,pid(N2)) -> F
164: eqt(request,int(N2)) -> F
165: eqt(request,cons(H2,T2)) -> F
166: eqt(request,tuple(H2,T2)) -> F
167: eqt(request,tuplenil(H2)) -> F
168: eqt(resource,nil) -> F
169: eqt(resource,a) -> F
170: eqt(resource,excl) -> F
171: eqt(resource,false) -> F
172: eqt(resource,lock) -> F
173: eqt(resource,locker) -> F
174: eqt(resource,mcrlrecord) -> F
175: eqt(resource,ok) -> F
176: eqt(resource,pending) -> F
177: eqt(resource,release) -> F
178: eqt(resource,request) -> F
179: eqt(resource,resource) -> T
180: eqt(resource,tag) -> F
181: eqt(resource,true) -> F
182: eqt(resource,undefined) -> F
183: eqt(resource,pid(N2)) -> F
184: eqt(resource,int(N2)) -> F
185: eqt(resource,cons(H2,T2)) -> F
186: eqt(resource,tuple(H2,T2)) -> F
187: eqt(resource,tuplenil(H2)) -> F
188: eqt(tag,nil) -> F
189: eqt(tag,a) -> F
190: eqt(tag,excl) -> F
191: eqt(tag,false) -> F
192: eqt(tag,lock) -> F
193: eqt(tag,locker) -> F
194: eqt(tag,mcrlrecord) -> F
195: eqt(tag,ok) -> F
196: eqt(tag,pending) -> F
197: eqt(tag,release) -> F
198: eqt(tag,request) -> F
199: eqt(tag,resource) -> F
200: eqt(tag,tag) -> T
201: eqt(tag,true) -> F
202: eqt(tag,undefined) -> F
203: eqt(tag,pid(N2)) -> F
204: eqt(tag,int(N2)) -> F
205: eqt(tag,cons(H2,T2)) -> F
206: eqt(tag,tuple(H2,T2)) -> F
207: eqt(tag,tuplenil(H2)) -> F
208: eqt(true,nil) -> F
209: eqt(true,a) -> F
210: eqt(true,excl) -> F
211: eqt(true,false) -> F
212: eqt(true,lock) -> F
213: eqt(true,locker) -> F
214: eqt(true,mcrlrecord) -> F
215: eqt(true,ok) -> F
216: eqt(true,pending) -> F
217: eqt(true,release) -> F
218: eqt(true,request) -> F
219: eqt(true,resource) -> F
220: eqt(true,tag) -> F
221: eqt(true,true) -> T
222: eqt(true,undefined) -> F
223: eqt(true,pid(N2)) -> F
224: eqt(true,int(N2)) -> F
225: eqt(true,cons(H2,T2)) -> F
226: eqt(true,tuple(H2,T2)) -> F
227: eqt(true,tuplenil(H2)) -> F
228: eqt(undefined,nil) -> F
229: eqt(undefined,a) -> F
230: eqt(undefined,tuplenil(H2)) -> F
231: eqt(pid(N1),nil) -> F
232: eqt(pid(N1),a) -> F
233: eqt(pid(N1),excl) -> F
234: eqt(pid(N1),false) -> F
235: eqt(pid(N1),lock) -> F
236: eqt(pid(N1),locker) -> F
237: eqt(pid(N1),mcrlrecord) -> F
238: eqt(pid(N1),ok) -> F
239: eqt(pid(N1),pending) -> F
240: eqt(pid(N1),release) -> F
241: eqt(pid(N1),request) -> F
242: eqt(pid(N1),resource) -> F
243: eqt(pid(N1),tag) -> F
244: eqt(pid(N1),true) -> F
245: eqt(pid(N1),undefined) -> F
246: eqt(pid(N1),pid(N2)) -> eqt(N1,N2)
247: eqt(pid(N1),int(N2)) -> F
248: eqt(pid(N1),cons(H2,T2)) -> F
249: eqt(pid(N1),tuple(H2,T2)) -> F
250: eqt(pid(N1),tuplenil(H2)) -> F
251: eqt(int(N1),nil) -> F
252: eqt(int(N1),a) -> F
253: eqt(int(N1),excl) -> F
254: eqt(int(N1),false) -> F
255: eqt(int(N1),lock) -> F
256: eqt(int(N1),locker) -> F
257: eqt(int(N1),mcrlrecord) -> F
258: eqt(int(N1),ok) -> F
259: eqt(int(N1),pending) -> F
260: eqt(int(N1),release) -> F
261: eqt(int(N1),request) -> F
262: eqt(int(N1),resource) -> F
263: eqt(int(N1),tag) -> F
264: eqt(int(N1),true) -> F
265: eqt(int(N1),undefined) -> F
266: eqt(cons(H1,T1),resource) -> F
267: eqt(cons(H1,T1),tag) -> F
268: eqt(cons(H1,T1),true) -> F
269: eqt(cons(H1,T1),undefined) -> F
270: eqt(cons(H1,T1),pid(N2)) -> F
271: eqt(cons(H1,T1),int(N2)) -> F
272: eqt(cons(H1,T1),cons(H2,T2)) -> and(eqt(H1,H2),eqt(T1,T2))
273: eqt(cons(H1,T1),tuple(H2,T2)) -> F
274: eqt(cons(H1,T1),tuplenil(H2)) -> F
275: eqt(tuple(H1,T1),nil) -> F
276: eqt(tuple(H1,T1),a) -> F
277: eqt(tuple(H1,T1),excl) -> F
278: eqt(tuple(H1,T1),false) -> F
279: eqt(tuple(H1,T1),lock) -> F
280: eqt(tuple(H1,T1),locker) -> F
281: eqt(tuple(H1,T1),mcrlrecord) -> F
282: eqt(tuple(H1,T1),ok) -> F
283: eqt(tuple(H1,T1),pending) -> F
284: eqt(tuple(H1,T1),release) -> F
285: eqt(tuple(H1,T1),request) -> F
286: eqt(tuple(H1,T1),resource) -> F
287: eqt(tuple(H1,T1),tag) -> F
288: eqt(tuple(H1,T1),true) -> F
289: eqt(tuple(H1,T1),undefined) -> F
290: eqt(tuple(H1,T1),pid(N2)) -> F
291: eqt(tuple(H1,T1),int(N2)) -> F
292: eqt(tuple(H1,T1),cons(H2,T2)) -> F
293: eqt(tuple(H1,T1),tuple(H2,T2)) -> and(eqt(H1,H2),eqt(T1,T2))
294: eqt(tuple(H1,T1),tuplenil(H2)) -> F
295: eqt(tuplenil(H1),nil) -> F
296: eqt(tuplenil(H1),a) -> F
297: eqt(tuplenil(H1),excl) -> F
298: eqt(tuplenil(H1),false) -> F
299: eqt(tuplenil(H1),lock) -> F
300: eqt(tuplenil(H1),locker) -> F
301: eqt(tuplenil(H1),mcrlrecord) -> F
302: eqt(tuplenil(H1),ok) -> F
303: eqt(tuplenil(H1),pending) -> F
304: eqt(tuplenil(H1),release) -> F
305: eqt(tuplenil(H1),request) -> F
306: eqt(tuplenil(H1),resource) -> F
307: eqt(tuplenil(H1),tag) -> F
308: eqt(tuplenil(H1),true) -> F
309: eqt(tuplenil(H1),undefined) -> F
310: eqt(tuplenil(H1),pid(N2)) -> F
311: eqt(tuplenil(H1),int(N2)) -> F
312: eqt(tuplenil(H1),cons(H2,T2)) -> F
313: eqt(tuplenil(H1),tuple(H2,T2)) -> F
314: eqt(tuplenil(H1),tuplenil(H2)) -> eqt(H1,H2)
315: element(int(s(0)),tuplenil(T1)) -> T1
316: element(int(s(0)),tuple(T1,T2)) -> T1
317: element(int(s(s(N1))),tuple(T1,T2)) -> element(int(s(N1)),T2)
318: record_new(lock) -> tuple(mcrlrecord,tuple(lock,tuple(undefined,tuple(nil,tuplenil(nil)))))
319: record_extract(tuple(mcrlrecord,tuple(lock,tuple(F0,tuple(F1,tuplenil(F2))))),lock,resource) -> tuple(mcrlrecord,tuple(lock,tuple(F0,tuple(F1,tuplenil(F2)))))
320: record_update(tuple(mcrlrecord,tuple(lock,tuple(F0,tuple(F1,tuplenil(F2))))),lock,pending,NewF) -> tuple(mcrlrecord,tuple(lock,tuple(F0,tuple(F1,tuplenil(NewF)))))
321: record_updates(Record,Name,nil) -> Record
322: record_updates(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields)) -> record_updates(record_update(Record,Name,Field,NewF),Name,Fields)
323: locker2_map_promote_pending(nil,Pending) -> nil
324: locker2_map_promote_pending(cons(Lock,Locks),Pending) -> cons(locker2_promote_pending(Lock,Pending),locker2_map_promote_pending(Locks,Pending))
325: locker2_map_claim_lock(nil,Resources,Client) -> nil
326: locker2_map_claim_lock(cons(Lock,Locks),Resources,Client) -> cons(locker2_claim_lock(Lock,Resources,Client),locker2_map_claim_lock(Locks,Resources,Client))
327: locker2_map_add_pending(nil,Resources,Client) -> nil
328: locker2_promote_pending(Lock,Client) -> case0(Client,Lock,record_extract(Lock,lock,pending))
329: case0(Client,Lock,cons(Client,Pendings)) -> record_updates(Lock,lock,cons(tuple(excl,tuplenil(Client)),cons(tuple(pending,tuplenil(Pendings)),nil)))
330: case0(Client,Lock,MCRLFree0) -> Lock
331: locker2_remove_pending(Lock,Client) -> record_updates(Lock,lock,cons(tuple(pending,tuplenil(subtract(record_extract(Lock,lock,pending),cons(Client,nil)))),nil))
332: locker2_add_pending(Lock,Resources,Client) -> case1(Client,Resources,Lock,member(record_extract(Lock,lock,resource),Resources))
333: case1(Client,Resources,Lock,true) -> record_updates(Lock,lock,cons(tuple(pending,tuplenil(append(record_extract(Lock,lock,pending),cons(Client,nil)))),nil))
334: case1(Client,Resources,Lock,false) -> Lock
335: locker2_release_lock(Lock,Client) -> case2(Client,Lock,gen_modtageq(Client,record_extract(Lock,lock,excl)))
336: case2(Client,Lock,true) -> record_updates(Lock,lock,cons(tuple(excllock,excl),nil))
337: case4(Client,Lock,MCRLFree1) -> false
338: locker2_obtainables(nil,Client) -> true
339: locker2_obtainables(cons(Lock,Locks),Client) -> case5(Client,Locks,Lock,member(Client,record_extract(Lock,lock,pending)))
340: case5(Client,Locks,Lock,true) -> andt(locker2_obtainable(Lock,Client),locker2_obtainables(Locks,Client))
341: case5(Client,Locks,Lock,false) -> locker2_obtainables(Locks,Client)
342: locker2_check_available(Resource,nil) -> false
343: locker2_check_available(Resource,cons(Lock,Locks)) -> case6(Locks,Lock,Resource,equal(Resource,record_extract(Lock,lock,resource)))
344: case6(Locks,Lock,Resource,true) -> andt(equal(record_extract(Lock,lock,excl),nil),equal(record_extract(Lock,lock,pending),nil))
345: case6(Locks,Lock,Resource,false) -> locker2_check_available(Resource,Locks)
346: locker2_check_availables(nil,Locks) -> true
347: locker2_check_availables(cons(Resource,Resources),Locks) -> andt(locker2_check_available(Resource,Locks),locker2_check_availables(Resources,Locks))
348: locker2_adduniq(nil,List) -> List
349: append(cons(Head,Tail),List) -> cons(Head,append(Tail,List))
350: subtract(List,nil) -> List
351: subtract(List,cons(Head,Tail)) -> subtract(delete(Head,List),Tail)
352: delete(E,nil) -> nil
353: delete(E,cons(Head,Tail)) -> case8(Tail,Head,E,equal(E,Head))
354: case8(Tail,Head,E,true) -> Tail
355: case8(Tail,Head,E,false) -> cons(Head,delete(E,Tail))
356: gen_tag(Pid) -> tuple(Pid,tuplenil(tag))
357: gen_modtageq(Client1,Client2) -> equal(Client1,Client2)
358: member(E,nil) -> false
359: member(E,cons(Head,Tail)) -> case9(Tail,Head,E,equal(E,Head))
360: case9(Tail,Head,E,true) -> true
361: case9(Tail,Head,E,false) -> member(E,Tail)
362: eqs(empty,empty) -> T
363: eqs(empty,stack(E2,S2)) -> F
364: eqs(stack(E1,S1),empty) -> F
365: eqs(stack(E1,S1),stack(E2,S2)) -> and(eqt(E1,E2),eqs(S1,S2))
366: pushs(E1,S1) -> stack(E1,S1)
367: pops(stack(E1,S1)) -> S1
368: tops(stack(E1,S1)) -> E1
369: istops(E1,empty) -> F
370: istops(E1,stack(E2,S1)) -> eqt(E1,E2)
371: eqc(nocalls,nocalls) -> T
372: eqc(nocalls,calls(E2,S2,CS2)) -> F
373: eqc(calls(E1,S1,CS1),nocalls) -> F
374: eqc(calls(E1,S1,CS1),calls(E2,S2,CS2)) -> and(eqt(E1,E2),and(eqs(S1,S2),eqc(CS1,CS2)))
375: push(E1,E2,nocalls) -> calls(E1,stack(E2,empty),nocalls)
376: push(E1,E2,calls(E3,S1,CS1)) -> push1(E1,E2,E3,S1,CS1,eqt(E1,E3))
377: push1(E1,E2,E3,S1,CS1,T) -> calls(E3,pushs(E2,S1),CS1)

There are 61 dependency pairs:

378: EQT(pid(N1),pid(N2)) -> EQT(N1,N2)
379: EQT(cons(H1,T1),cons(H2,T2)) -> AND(eqt(H1,H2),eqt(T1,T2))
380: EQT(cons(H1,T1),cons(H2,T2)) -> EQT(H1,H2)
381: EQT(cons(H1,T1),cons(H2,T2)) -> EQT(T1,T2)
382: EQT(tuple(H1,T1),tuple(H2,T2)) -> AND(eqt(H1,H2),eqt(T1,T2))
383: EQT(tuple(H1,T1),tuple(H2,T2)) -> EQT(H1,H2)
384: EQT(tuple(H1,T1),tuple(H2,T2)) -> EQT(T1,T2)
385: EQT(tuplenil(H1),tuplenil(H2)) -> EQT(H1,H2)
386: ELEMENT(int(s(s(N1))),tuple(T1,T2)) -> ELEMENT(int(s(N1)),T2)
387: RECORD_UPDATES(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields)) -> RECORD_UPDATES(record_update(Record,Name,Field,NewF),Name,Fields)
388: RECORD_UPDATES(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields)) -> RECORD_UPDATE(Record,Name,Field,NewF)
389: LOCKER2_MAP_PROMOTE_PENDING(cons(Lock,Locks),Pending) -> LOCKER2_PROMOTE_PENDING(Lock,Pending)
390: LOCKER2_MAP_PROMOTE_PENDING(cons(Lock,Locks),Pending) -> LOCKER2_MAP_PROMOTE_PENDING(Locks,Pending)
391: LOCKER2_MAP_CLAIM_LOCK(cons(Lock,Locks),Resources,Client) -> LOCKER2_MAP_CLAIM_LOCK(Locks,Resources,Client)
392: LOCKER2_PROMOTE_PENDING(Lock,Client) -> CASE0(Client,Lock,record_extract(Lock,lock,pending))
393: LOCKER2_PROMOTE_PENDING(Lock,Client) -> RECORD_EXTRACT(Lock,lock,pending)
394: CASE0(Client,Lock,cons(Client,Pendings)) -> RECORD_UPDATES(Lock,lock,cons(tuple(excl,tuplenil(Client)),cons(tuple(pending,tuplenil(Pendings)),nil)))
395: LOCKER2_REMOVE_PENDING(Lock,Client) -> RECORD_UPDATES(Lock,lock,cons(tuple(pending,tuplenil(subtract(record_extract(Lock,lock,pending),cons(Client,nil)))),nil))
396: LOCKER2_REMOVE_PENDING(Lock,Client) -> SUBTRACT(record_extract(Lock,lock,pending),cons(Client,nil))
397: LOCKER2_REMOVE_PENDING(Lock,Client) -> RECORD_EXTRACT(Lock,lock,pending)
398: LOCKER2_ADD_PENDING(Lock,Resources,Client) -> CASE1(Client,Resources,Lock,member(record_extract(Lock,lock,resource),Resources))
399: LOCKER2_ADD_PENDING(Lock,Resources,Client) -> MEMBER(record_extract(Lock,lock,resource),Resources)
400: LOCKER2_ADD_PENDING(Lock,Resources,Client) -> RECORD_EXTRACT(Lock,lock,resource)
401: CASE1(Client,Resources,Lock,true) -> RECORD_UPDATES(Lock,lock,cons(tuple(pending,tuplenil(append(record_extract(Lock,lock,pending),cons(Client,nil)))),nil))
402: CASE1(Client,Resources,Lock,true) -> APPEND(record_extract(Lock,lock,pending),cons(Client,nil))
403: CASE1(Client,Resources,Lock,true) -> RECORD_EXTRACT(Lock,lock,pending)
404: LOCKER2_RELEASE_LOCK(Lock,Client) -> CASE2(Client,Lock,gen_modtageq(Client,record_extract(Lock,lock,excl)))
405: LOCKER2_RELEASE_LOCK(Lock,Client) -> GEN_MODTAGEQ(Client,record_extract(Lock,lock,excl))
406: LOCKER2_RELEASE_LOCK(Lock,Client) -> RECORD_EXTRACT(Lock,lock,excl)
407: CASE2(Client,Lock,true) -> RECORD_UPDATES(Lock,lock,cons(tuple(excllock,excl),nil))
408: LOCKER2_OBTAINABLES(cons(Lock,Locks),Client) -> CASE5(Client,Locks,Lock,member(Client,record_extract(Lock,lock,pending)))
409: LOCKER2_OBTAINABLES(cons(Lock,Locks),Client) -> MEMBER(Client,record_extract(Lock,lock,pending))
410: LOCKER2_OBTAINABLES(cons(Lock,Locks),Client) -> RECORD_EXTRACT(Lock,lock,pending)
411: CASE5(Client,Locks,Lock,true) -> LOCKER2_OBTAINABLES(Locks,Client)
412: CASE5(Client,Locks,Lock,false) -> LOCKER2_OBTAINABLES(Locks,Client)
413: LOCKER2_CHECK_AVAILABLE(Resource,cons(Lock,Locks)) -> CASE6(Locks,Lock,Resource,equal(Resource,record_extract(Lock,lock,resource)))
414: LOCKER2_CHECK_AVAILABLE(Resource,cons(Lock,Locks)) -> RECORD_EXTRACT(Lock,lock,resource)
415: CASE6(Locks,Lock,Resource,true) -> RECORD_EXTRACT(Lock,lock,excl)
416: CASE6(Locks,Lock,Resource,true) -> RECORD_EXTRACT(Lock,lock,pending)
417: CASE6(Locks,Lock,Resource,false) -> LOCKER2_CHECK_AVAILABLE(Resource,Locks)
418: LOCKER2_CHECK_AVAILABLES(cons(Resource,Resources),Locks) -> LOCKER2_CHECK_AVAILABLE(Resource,Locks)
419: LOCKER2_CHECK_AVAILABLES(cons(Resource,Resources),Locks) -> LOCKER2_CHECK_AVAILABLES(Resources,Locks)
420: APPEND(cons(Head,Tail),List) -> APPEND(Tail,List)
421: SUBTRACT(List,cons(Head,Tail)) -> SUBTRACT(delete(Head,List),Tail)
422: SUBTRACT(List,cons(Head,Tail)) -> DELETE(Head,List)
423: DELETE(E,cons(Head,Tail)) -> CASE8(Tail,Head,E,equal(E,Head))
424: CASE8(Tail,Head,E,false) -> DELETE(E,Tail)
425: MEMBER(E,cons(Head,Tail)) -> CASE9(Tail,Head,E,equal(E,Head))
426: CASE9(Tail,Head,E,false) -> MEMBER(E,Tail)
427: EQS(stack(E1,S1),stack(E2,S2)) -> AND(eqt(E1,E2),eqs(S1,S2))
428: EQS(stack(E1,S1),stack(E2,S2)) -> EQT(E1,E2)
429: EQS(stack(E1,S1),stack(E2,S2)) -> EQS(S1,S2)
430: ISTOPS(E1,stack(E2,S1)) -> EQT(E1,E2)
431: EQC(calls(E1,S1,CS1),calls(E2,S2,CS2)) -> AND(eqt(E1,E2),and(eqs(S1,S2),eqc(CS1,CS2)))
432: EQC(calls(E1,S1,CS1),calls(E2,S2,CS2)) -> EQT(E1,E2)
433: EQC(calls(E1,S1,CS1),calls(E2,S2,CS2)) -> AND(eqs(S1,S2),eqc(CS1,CS2))
434: EQC(calls(E1,S1,CS1),calls(E2,S2,CS2)) -> EQS(S1,S2)
435: EQC(calls(E1,S1,CS1),calls(E2,S2,CS2)) -> EQC(CS1,CS2)
436: PUSH(E1,E2,calls(E3,S1,CS1)) -> PUSH1(E1,E2,E3,S1,CS1,eqt(E1,E3))
437: PUSH(E1,E2,calls(E3,S1,CS1)) -> EQT(E1,E3)
438: PUSH1(E1,E2,E3,S1,CS1,T) -> PUSHS(E2,S1)

The approximated dependency graph contains 11 SCCs:
{420},
{386},
{391},
{387},
{419},
{421},
{408,411,412},
{378,380,381,383-385},
{429},
{435}
and {390}.

- Consider the SCC {420}.
There are no usable rules.
By taking the polynomial interpretation
[APPEND](x,y) = [cons](x,y) = x + y + 1,
rule 420
is strictly decreasing.

- Consider the SCC {386}.
There are no usable rules.
By taking the polynomial interpretation
[int](x) = [s](x) = x + 1
and [ELEMENT](x,y) = [tuple](x,y) = x + y + 1,
rule 386
is strictly decreasing.

- Consider the SCC {391}.
There are no usable rules.
By taking the polynomial interpretation
[cons](x,y) = x + y + 1
and [LOCKER2_MAP_CLAIM_LOCK](x,y,z) = x + y + z + 1,
rule 391
is strictly decreasing.

- Consider the SCC {387}.
The usable rules are {320}.
By taking the polynomial interpretation
[lock] = [mcrlrecord] = [pending] = 1,
[tuplenil](x) = x + 1,
[cons](x,y) = [tuple](x,y) = x + y + 1,
[RECORD_UPDATES](x,y,z) = x + y + z + 1
and [record_update](x,y,z,w) = x + z + w + 1,
the rules in {320,387}
are strictly decreasing.

- Consider the SCC {419}.
There are no usable rules.
By taking the polynomial interpretation
[cons](x,y) = [LOCKER2_CHECK_AVAILABLES](x,y) = x + y + 1,
rule 419
is strictly decreasing.

- Consider the SCC {421}.
The usable rules are {352-355}.
By taking the polynomial interpretation
[equal](x,y) = [false] = [nil] = [true] = 1,
[cons](x,y) = [delete](x,y) = x + y + 1,
[case8](x,y,z,w) = x + y + z + w + 1
and [SUBTRACT](x,y) = y + 1,
the rules in {353,355}
are weakly decreasing and
the rules in {352,354,421}
are strictly decreasing.

- Consider the SCC {408,411,412}.
The usable rules are {319,358-361}.
By taking the polynomial interpretation
[equal](x,y) = [false] = [lock] = [mcrlrecord] = [nil] = [pending] = [resource] = [true] = 1,
[tuplenil](x) = x + 1,
[cons](x,y) = [LOCKER2_OBTAINABLES](x,y) = [member](x,y) = [tuple](x,y) = x + y + 1,
[CASE5](x,y,z,w) = [record_extract](x,y,z) = x + y + z + 1
and [case9](x,y,z,w) = x + y + z + w + 1,
the rules in {359,411,412}
are weakly decreasing and
the rules in {319,358,360,361,408}
are strictly decreasing.

- Consider the SCC {378,380,381,383-385}.
There are no usable rules.
By taking the polynomial interpretation
[pid](x) = [tuplenil](x) = x + 1
and [cons](x,y) = [EQT](x,y) = [tuple](x,y) = x + y + 1,
the rules in {378,380,381,383-385}
are strictly decreasing.

- Consider the SCC {429}.
There are no usable rules.
By taking the polynomial interpretation
[EQS](x,y) = [stack](x,y) = x + y + 1,
rule 429
is strictly decreasing.

- Consider the SCC {435}.
There are no usable rules.
By taking the polynomial interpretation
[EQC](x,y) = x + y + 1
and [calls](x,y,z) = x + y + z + 1,
rule 435
is strictly decreasing.

- Consider the SCC {390}.
There are no usable rules.
By taking the polynomial interpretation
[cons](x,y) = [LOCKER2_MAP_PROMOTE_PENDING](x,y) = x + y + 1,
rule 390
is strictly decreasing.

Hence the TRS is terminating.