Certification Problem

Input (TPDB TRS_Standard/CiME_04/mucrl1)

The rewrite relation of the following TRS is considered.

There are 377 ruless (increase limit for explicit display).

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

case5^#(Client,Locks,Lock,true)	→	locker2_obtainables^#(Locks,Client)	(378)
delete^#(E,cons(Head,Tail))	→	case8^#(Tail,Head,E,equal(E,Head))	(379)
case5^#(Client,Locks,Lock,false)	→	locker2_obtainables^#(Locks,Client)	(380)
case0^#(Client,Lock,cons(Client,Pendings))	→	record_updates^#(Lock,lock,cons(tuple(excl,tuplenil(Client)),cons(tuple(pending,tuplenil(Pendings)),nil)))	(381)
append^#(cons(Head,Tail),List)	→	append^#(Tail,List)	(382)
member^#(E,cons(Head,Tail))	→	case9^#(Tail,Head,E,equal(E,Head))	(383)
element^#(int(s(s(N1))),tuple(T1,T2))	→	element^#(int(s(N1)),T2)	(384)
eqs^#(stack(E1,S1),stack(E2,S2))	→	and^#(eqt(E1,E2),eqs(S1,S2))	(385)
locker2_map_claim_lock^#(cons(Lock,Locks),Resources,Client)	→	locker2_map_claim_lock^#(Locks,Resources,Client)	(386)
locker2_add_pending^#(Lock,Resources,Client)	→	record_extract^#(Lock,lock,resource)	(387)
push1^#(E1,E2,E3,S1,CS1,T)	→	pushs^#(E2,S1)	(388)
eqt^#(pid(N1),pid(N2))	→	eqt^#(N1,N2)	(389)
eqt^#(cons(H1,T1),cons(H2,T2))	→	eqt^#(T1,T2)	(390)
eqs^#(stack(E1,S1),stack(E2,S2))	→	eqt^#(E1,E2)	(391)
eqt^#(tuple(H1,T1),tuple(H2,T2))	→	eqt^#(H1,H2)	(392)
eqt^#(cons(H1,T1),cons(H2,T2))	→	and^#(eqt(H1,H2),eqt(T1,T2))	(393)
locker2_release_lock^#(Lock,Client)	→	case2^#(Client,Lock,gen_modtageq(Client,record_extract(Lock,lock,excl)))	(394)
case8^#(Tail,Head,E,false)	→	delete^#(E,Tail)	(395)
locker2_add_pending^#(Lock,Resources,Client)	→	case1^#(Client,Resources,Lock,member(record_extract(Lock,lock,resource),Resources))	(396)
eqt^#(tuplenil(H1),tuplenil(H2))	→	eqt^#(H1,H2)	(397)
eqc^#(calls(E1,S1,CS1),calls(E2,S2,CS2))	→	eqt^#(E1,E2)	(398)
eqc^#(calls(E1,S1,CS1),calls(E2,S2,CS2))	→	eqs^#(S1,S2)	(399)
locker2_release_lock^#(Lock,Client)	→	record_extract^#(Lock,lock,excl)	(400)
locker2_check_availables^#(cons(Resource,Resources),Locks)	→	locker2_check_availables^#(Resources,Locks)	(401)
locker2_check_availables^#(cons(Resource,Resources),Locks)	→	locker2_check_available^#(Resource,Locks)	(402)
locker2_promote_pending^#(Lock,Client)	→	record_extract^#(Lock,lock,pending)	(403)
eqc^#(calls(E1,S1,CS1),calls(E2,S2,CS2))	→	eqc^#(CS1,CS2)	(404)
case1^#(Client,Resources,Lock,true)	→	append^#(record_extract(Lock,lock,pending),cons(Client,nil))	(405)
locker2_release_lock^#(Lock,Client)	→	gen_modtageq^#(Client,record_extract(Lock,lock,excl))	(406)
case6^#(Locks,Lock,Resource,false)	→	locker2_check_available^#(Resource,Locks)	(407)
case1^#(Client,Resources,Lock,true)	→	record_updates^#(Lock,lock,cons(tuple(pending,tuplenil(append(record_extract(Lock,lock,pending),cons(Client,nil)))),nil))	(408)
locker2_add_pending^#(Lock,Resources,Client)	→	member^#(record_extract(Lock,lock,resource),Resources)	(409)
locker2_check_available^#(Resource,cons(Lock,Locks))	→	case6^#(Locks,Lock,Resource,equal(Resource,record_extract(Lock,lock,resource)))	(410)
case6^#(Locks,Lock,Resource,true)	→	record_extract^#(Lock,lock,excl)	(411)
locker2_remove_pending^#(Lock,Client)	→	record_extract^#(Lock,lock,pending)	(412)
eqt^#(tuple(H1,T1),tuple(H2,T2))	→	eqt^#(T1,T2)	(413)
eqs^#(stack(E1,S1),stack(E2,S2))	→	eqs^#(S1,S2)	(414)
eqc^#(calls(E1,S1,CS1),calls(E2,S2,CS2))	→	and^#(eqs(S1,S2),eqc(CS1,CS2))	(415)
push^#(E1,E2,calls(E3,S1,CS1))	→	push1^#(E1,E2,E3,S1,CS1,eqt(E1,E3))	(416)
eqt^#(tuple(H1,T1),tuple(H2,T2))	→	and^#(eqt(H1,H2),eqt(T1,T2))	(417)
locker2_promote_pending^#(Lock,Client)	→	case0^#(Client,Lock,record_extract(Lock,lock,pending))	(418)
subtract^#(List,cons(Head,Tail))	→	delete^#(Head,List)	(419)
record_updates^#(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields))	→	record_update^#(Record,Name,Field,NewF)	(420)
push^#(E1,E2,calls(E3,S1,CS1))	→	eqt^#(E1,E3)	(421)
subtract^#(List,cons(Head,Tail))	→	subtract^#(delete(Head,List),Tail)	(422)
eqt^#(cons(H1,T1),cons(H2,T2))	→	eqt^#(H1,H2)	(423)
locker2_obtainables^#(cons(Lock,Locks),Client)	→	record_extract^#(Lock,lock,pending)	(424)
case1^#(Client,Resources,Lock,true)	→	record_extract^#(Lock,lock,pending)	(425)
locker2_remove_pending^#(Lock,Client)	→	subtract^#(record_extract(Lock,lock,pending),cons(Client,nil))	(426)
case6^#(Locks,Lock,Resource,true)	→	record_extract^#(Lock,lock,pending)	(427)
case9^#(Tail,Head,E,false)	→	member^#(E,Tail)	(428)
record_updates^#(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields))	→	record_updates^#(record_update(Record,Name,Field,NewF),Name,Fields)	(429)
locker2_obtainables^#(cons(Lock,Locks),Client)	→	member^#(Client,record_extract(Lock,lock,pending))	(430)
locker2_map_promote_pending^#(cons(Lock,Locks),Pending)	→	locker2_promote_pending^#(Lock,Pending)	(431)
case2^#(Client,Lock,true)	→	record_updates^#(Lock,lock,cons(tuple(excllock,excl),nil))	(432)
istops^#(E1,stack(E2,S1))	→	eqt^#(E1,E2)	(433)
eqc^#(calls(E1,S1,CS1),calls(E2,S2,CS2))	→	and^#(eqt(E1,E2),and(eqs(S1,S2),eqc(CS1,CS2)))	(434)
locker2_obtainables^#(cons(Lock,Locks),Client)	→	case5^#(Client,Locks,Lock,member(Client,record_extract(Lock,lock,pending)))	(435)
locker2_map_promote_pending^#(cons(Lock,Locks),Pending)	→	locker2_map_promote_pending^#(Locks,Pending)	(436)
locker2_check_available^#(Resource,cons(Lock,Locks))	→	record_extract^#(Lock,lock,resource)	(437)
locker2_remove_pending^#(Lock,Client)	→	record_updates^#(Lock,lock,cons(tuple(pending,tuplenil(subtract(record_extract(Lock,lock,pending),cons(Client,nil)))),nil))	(438)

1.1 Dependency Graph Processor

The dependency pairs are split into 10 components.

The 1^st component contains the pair

locker2_map_promote_pending^#(cons(Lock,Locks),Pending)

→

locker2_map_promote_pending^#(Locks,Pending)

(436)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a]	=	0
[locker2_promote_pending^#(x₁, x₂)]	=	0
[locker2_promote_pending(x₁, x₂)]	=	0
[locker2_check_availables(x₁, x₂)]	=	0
[element(x₁, x₂)]	=	0
[record_extract(x₁, x₂, x₃)]	=	0
[case6^#(x₁,...,x₄)]	=	0
[tuplenil(x₁)]	=	0
[s(x₁)]	=	0
[case2^#(x₁, x₂, x₃)]	=	0
[append^#(x₁, x₂)]	=	0
[resource]	=	0
[locker2_obtainable(x₁, x₂)]	=	0
[locker2_adduniq(x₁, x₂)]	=	0
[locker2_add_pending^#(x₁, x₂, x₃)]	=	0
[member(x₁, x₂)]	=	0
[case4^#(x₁, x₂, x₃)]	=	0
[T]	=	0
[lock]	=	0
[locker2_release_lock^#(x₁, x₂)]	=	0
[F]	=	0
[and(x₁, x₂)]	=	0
[locker2_map_add_pending(x₁, x₂, x₃)]	=	0
[eq(x₁, x₂)]	=	0
[stack(x₁, x₂)]	=	0
[locker2_map_claim_lock(x₁, x₂, x₃)]	=	0
[tag]	=	0
[record_updates(x₁, x₂, x₃)]	=	0
[locker2_adduniq^#(x₁, x₂)]	=	0
[false]	=	0
[excl]	=	0
[locker2_map_claim_lock^#(x₁, x₂, x₃)]	=	0
[excllock]	=	0
[case5(x₁,...,x₄)]	=	0
[tops^#(x₁)]	=	0
[case1(x₁,...,x₄)]	=	0
[pops^#(x₁)]	=	0
[record_update(x₁,...,x₄)]	=	0
[locker2_claim_lock(x₁, x₂, x₃)]	=	0
[pid(x₁)]	=	0
[eqc^#(x₁, x₂)]	=	0
[push1(x₁,...,x₆)]	=	0
[locker2_remove_pending(x₁, x₂)]	=	0
[eqt^#(x₁, x₂)]	=	0
[true]	=	0
[eqs^#(x₁, x₂)]	=	0
[eq^#(x₁, x₂)]	=	0
[not^#(x₁)]	=	0
[delete(x₁, x₂)]	=	0
[record_new^#(x₁)]	=	0
[record_updates^#(x₁, x₂, x₃)]	=	0
[locker2_map_promote_pending^#(x₁, x₂)]	=	x₁ + 0
[push1^#(x₁,...,x₆)]	=	0
[ok]	=	0
[append(x₁, x₂)]	=	0
[istops(x₁, x₂)]	=	0
[push^#(x₁, x₂, x₃)]	=	0
[if(x₁, x₂, x₃)]	=	0
[0]	=	0
[record_update^#(x₁,...,x₄)]	=	0
[push(x₁, x₂, x₃)]	=	0
[locker2_obtainables(x₁, x₂)]	=	0
[tops(x₁)]	=	0
[case0(x₁, x₂, x₃)]	=	0
[gen_tag^#(x₁)]	=	0
[locker2_check_available(x₁, x₂)]	=	0
[locker2_map_add_pending^#(x₁, x₂, x₃)]	=	0
[nil]	=	0
[imp^#(x₁, x₂)]	=	0
[or(x₁, x₂)]	=	0
[locker2_release_lock(x₁, x₂)]	=	0
[istops^#(x₁, x₂)]	=	0
[locker2_check_available^#(x₁, x₂)]	=	0
[locker2_check_availables^#(x₁, x₂)]	=	0
[locker]	=	0
[mcrlrecord]	=	0
[release]	=	0
[case0^#(x₁, x₂, x₃)]	=	0
[gen_tag(x₁)]	=	0
[delete^#(x₁, x₂)]	=	0
[gen_modtageq(x₁, x₂)]	=	0
[tuple(x₁, x₂)]	=	0
[eqc(x₁, x₂)]	=	0
[int(x₁)]	=	0
[subtract(x₁, x₂)]	=	0
[case2(x₁, x₂, x₃)]	=	0
[locker2_obtainables^#(x₁, x₂)]	=	0
[undefined]	=	0
[request]	=	0
[eqs(x₁, x₂)]	=	0
[record_new(x₁)]	=	0
[nocalls]	=	0
[cons(x₁, x₂)]	=	x₂ + 1
[member^#(x₁, x₂)]	=	0
[if^#(x₁, x₂, x₃)]	=	0
[eqt(x₁, x₂)]	=	0
[equal(x₁, x₂)]	=	0
[case9(x₁,...,x₄)]	=	0
[empty]	=	0
[case1^#(x₁,...,x₄)]	=	0
[pushs(x₁, x₂)]	=	0
[case8^#(x₁,...,x₄)]	=	0
[pending]	=	0
[pushs^#(x₁, x₂)]	=	0
[subtract^#(x₁, x₂)]	=	0
[record_extract^#(x₁, x₂, x₃)]	=	0
[case8(x₁,...,x₄)]	=	0
[or^#(x₁, x₂)]	=	0
[case5^#(x₁,...,x₄)]	=	0
[locker2_add_pending(x₁, x₂, x₃)]	=	0
[case4(x₁, x₂, x₃)]	=	0
[imp(x₁, x₂)]	=	0
[element^#(x₁, x₂)]	=	0
[calls(x₁, x₂, x₃)]	=	0
[locker2_map_promote_pending(x₁, x₂)]	=	0
[pops(x₁)]	=	0
[case6(x₁,...,x₄)]	=	0
[and^#(x₁, x₂)]	=	0
[case9^#(x₁,...,x₄)]	=	0
[not(x₁)]	=	0
[andt(x₁, x₂)]	=	0
[locker2_remove_pending^#(x₁, x₂)]	=	0
[gen_modtageq^#(x₁, x₂)]	=	0

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pair

locker2_map_promote_pending^#(cons(Lock,Locks),Pending)

→

locker2_map_promote_pending^#(Locks,Pending)

(436)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

eqc^#(calls(E1,S1,CS1),calls(E2,S2,CS2))

→

eqc^#(CS1,CS2)

(404)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a]	=	0
[locker2_promote_pending^#(x₁, x₂)]	=	0
[locker2_promote_pending(x₁, x₂)]	=	0
[locker2_check_availables(x₁, x₂)]	=	0
[element(x₁, x₂)]	=	0
[record_extract(x₁, x₂, x₃)]	=	0
[case6^#(x₁,...,x₄)]	=	0
[tuplenil(x₁)]	=	0
[s(x₁)]	=	0
[case2^#(x₁, x₂, x₃)]	=	0
[append^#(x₁, x₂)]	=	0
[resource]	=	0
[locker2_obtainable(x₁, x₂)]	=	0
[locker2_adduniq(x₁, x₂)]	=	0
[locker2_add_pending^#(x₁, x₂, x₃)]	=	0
[member(x₁, x₂)]	=	0
[case4^#(x₁, x₂, x₃)]	=	0
[T]	=	0
[lock]	=	0
[locker2_release_lock^#(x₁, x₂)]	=	0
[F]	=	0
[and(x₁, x₂)]	=	0
[locker2_map_add_pending(x₁, x₂, x₃)]	=	0
[eq(x₁, x₂)]	=	0
[stack(x₁, x₂)]	=	0
[locker2_map_claim_lock(x₁, x₂, x₃)]	=	0
[tag]	=	0
[record_updates(x₁, x₂, x₃)]	=	0
[locker2_adduniq^#(x₁, x₂)]	=	0
[false]	=	0
[excl]	=	0
[locker2_map_claim_lock^#(x₁, x₂, x₃)]	=	0
[excllock]	=	0
[case5(x₁,...,x₄)]	=	0
[tops^#(x₁)]	=	0
[case1(x₁,...,x₄)]	=	0
[pops^#(x₁)]	=	0
[record_update(x₁,...,x₄)]	=	0
[locker2_claim_lock(x₁, x₂, x₃)]	=	0
[pid(x₁)]	=	0
[eqc^#(x₁, x₂)]	=	x₂ + 0
[push1(x₁,...,x₆)]	=	0
[locker2_remove_pending(x₁, x₂)]	=	0
[eqt^#(x₁, x₂)]	=	0
[true]	=	0
[eqs^#(x₁, x₂)]	=	0
[eq^#(x₁, x₂)]	=	0
[not^#(x₁)]	=	0
[delete(x₁, x₂)]	=	0
[record_new^#(x₁)]	=	0
[record_updates^#(x₁, x₂, x₃)]	=	0
[locker2_map_promote_pending^#(x₁, x₂)]	=	0
[push1^#(x₁,...,x₆)]	=	0
[ok]	=	0
[append(x₁, x₂)]	=	0
[istops(x₁, x₂)]	=	0
[push^#(x₁, x₂, x₃)]	=	0
[if(x₁, x₂, x₃)]	=	0
[0]	=	0
[record_update^#(x₁,...,x₄)]	=	0
[push(x₁, x₂, x₃)]	=	0
[locker2_obtainables(x₁, x₂)]	=	0
[tops(x₁)]	=	0
[case0(x₁, x₂, x₃)]	=	0
[gen_tag^#(x₁)]	=	0
[locker2_check_available(x₁, x₂)]	=	0
[locker2_map_add_pending^#(x₁, x₂, x₃)]	=	0
[nil]	=	0
[imp^#(x₁, x₂)]	=	0
[or(x₁, x₂)]	=	0
[locker2_release_lock(x₁, x₂)]	=	0
[istops^#(x₁, x₂)]	=	0
[locker2_check_available^#(x₁, x₂)]	=	0
[locker2_check_availables^#(x₁, x₂)]	=	0
[locker]	=	0
[mcrlrecord]	=	0
[release]	=	0
[case0^#(x₁, x₂, x₃)]	=	0
[gen_tag(x₁)]	=	0
[delete^#(x₁, x₂)]	=	0
[gen_modtageq(x₁, x₂)]	=	0
[tuple(x₁, x₂)]	=	0
[eqc(x₁, x₂)]	=	0
[int(x₁)]	=	0
[subtract(x₁, x₂)]	=	0
[case2(x₁, x₂, x₃)]	=	0
[locker2_obtainables^#(x₁, x₂)]	=	0
[undefined]	=	0
[request]	=	0
[eqs(x₁, x₂)]	=	0
[record_new(x₁)]	=	0
[nocalls]	=	0
[cons(x₁, x₂)]	=	1
[member^#(x₁, x₂)]	=	0
[if^#(x₁, x₂, x₃)]	=	0
[eqt(x₁, x₂)]	=	0
[equal(x₁, x₂)]	=	0
[case9(x₁,...,x₄)]	=	0
[empty]	=	0
[case1^#(x₁,...,x₄)]	=	0
[pushs(x₁, x₂)]	=	0
[case8^#(x₁,...,x₄)]	=	0
[pending]	=	0
[pushs^#(x₁, x₂)]	=	0
[subtract^#(x₁, x₂)]	=	0
[record_extract^#(x₁, x₂, x₃)]	=	0
[case8(x₁,...,x₄)]	=	0
[or^#(x₁, x₂)]	=	0
[case5^#(x₁,...,x₄)]	=	0
[locker2_add_pending(x₁, x₂, x₃)]	=	0
[case4(x₁, x₂, x₃)]	=	0
[imp(x₁, x₂)]	=	0
[element^#(x₁, x₂)]	=	0
[calls(x₁, x₂, x₃)]	=	x₃ + 1
[locker2_map_promote_pending(x₁, x₂)]	=	0
[pops(x₁)]	=	0
[case6(x₁,...,x₄)]	=	0
[and^#(x₁, x₂)]	=	0
[case9^#(x₁,...,x₄)]	=	0
[not(x₁)]	=	0
[andt(x₁, x₂)]	=	0
[locker2_remove_pending^#(x₁, x₂)]	=	0
[gen_modtageq^#(x₁, x₂)]	=	0

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pair

eqc^#(calls(E1,S1,CS1),calls(E2,S2,CS2))

→

eqc^#(CS1,CS2)

(404)

could be deleted.

1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 3^rd component contains the pair

locker2_check_availables^#(cons(Resource,Resources),Locks)

→

locker2_check_availables^#(Resources,Locks)

(401)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a]	=	0
[locker2_promote_pending^#(x₁, x₂)]	=	0
[locker2_promote_pending(x₁, x₂)]	=	0
[locker2_check_availables(x₁, x₂)]	=	0
[element(x₁, x₂)]	=	0
[record_extract(x₁, x₂, x₃)]	=	0
[case6^#(x₁,...,x₄)]	=	0
[tuplenil(x₁)]	=	0
[s(x₁)]	=	0
[case2^#(x₁, x₂, x₃)]	=	0
[append^#(x₁, x₂)]	=	0
[resource]	=	0
[locker2_obtainable(x₁, x₂)]	=	0
[locker2_adduniq(x₁, x₂)]	=	0
[locker2_add_pending^#(x₁, x₂, x₃)]	=	0
[member(x₁, x₂)]	=	0
[case4^#(x₁, x₂, x₃)]	=	0
[T]	=	0
[lock]	=	0
[locker2_release_lock^#(x₁, x₂)]	=	0
[F]	=	0
[and(x₁, x₂)]	=	0
[locker2_map_add_pending(x₁, x₂, x₃)]	=	0
[eq(x₁, x₂)]	=	0
[stack(x₁, x₂)]	=	0
[locker2_map_claim_lock(x₁, x₂, x₃)]	=	0
[tag]	=	0
[record_updates(x₁, x₂, x₃)]	=	0
[locker2_adduniq^#(x₁, x₂)]	=	0
[false]	=	0
[excl]	=	0
[locker2_map_claim_lock^#(x₁, x₂, x₃)]	=	0
[excllock]	=	0
[case5(x₁,...,x₄)]	=	0
[tops^#(x₁)]	=	0
[case1(x₁,...,x₄)]	=	0
[pops^#(x₁)]	=	0
[record_update(x₁,...,x₄)]	=	0
[locker2_claim_lock(x₁, x₂, x₃)]	=	0
[pid(x₁)]	=	0
[eqc^#(x₁, x₂)]	=	0
[push1(x₁,...,x₆)]	=	0
[locker2_remove_pending(x₁, x₂)]	=	0
[eqt^#(x₁, x₂)]	=	0
[true]	=	0
[eqs^#(x₁, x₂)]	=	0
[eq^#(x₁, x₂)]	=	0
[not^#(x₁)]	=	0
[delete(x₁, x₂)]	=	0
[record_new^#(x₁)]	=	0
[record_updates^#(x₁, x₂, x₃)]	=	0
[locker2_map_promote_pending^#(x₁, x₂)]	=	0
[push1^#(x₁,...,x₆)]	=	0
[ok]	=	0
[append(x₁, x₂)]	=	0
[istops(x₁, x₂)]	=	0
[push^#(x₁, x₂, x₃)]	=	0
[if(x₁, x₂, x₃)]	=	0
[0]	=	0
[record_update^#(x₁,...,x₄)]	=	0
[push(x₁, x₂, x₃)]	=	0
[locker2_obtainables(x₁, x₂)]	=	0
[tops(x₁)]	=	0
[case0(x₁, x₂, x₃)]	=	0
[gen_tag^#(x₁)]	=	0
[locker2_check_available(x₁, x₂)]	=	0
[locker2_map_add_pending^#(x₁, x₂, x₃)]	=	0
[nil]	=	0
[imp^#(x₁, x₂)]	=	0
[or(x₁, x₂)]	=	0
[locker2_release_lock(x₁, x₂)]	=	0
[istops^#(x₁, x₂)]	=	0
[locker2_check_available^#(x₁, x₂)]	=	0
[locker2_check_availables^#(x₁, x₂)]	=	x₁ + 0
[locker]	=	0
[mcrlrecord]	=	0
[release]	=	0
[case0^#(x₁, x₂, x₃)]	=	0
[gen_tag(x₁)]	=	0
[delete^#(x₁, x₂)]	=	0
[gen_modtageq(x₁, x₂)]	=	0
[tuple(x₁, x₂)]	=	0
[eqc(x₁, x₂)]	=	0
[int(x₁)]	=	0
[subtract(x₁, x₂)]	=	0
[case2(x₁, x₂, x₃)]	=	0
[locker2_obtainables^#(x₁, x₂)]	=	0
[undefined]	=	0
[request]	=	0
[eqs(x₁, x₂)]	=	0
[record_new(x₁)]	=	0
[nocalls]	=	0
[cons(x₁, x₂)]	=	x₂ + 1
[member^#(x₁, x₂)]	=	0
[if^#(x₁, x₂, x₃)]	=	0
[eqt(x₁, x₂)]	=	0
[equal(x₁, x₂)]	=	0
[case9(x₁,...,x₄)]	=	0
[empty]	=	0
[case1^#(x₁,...,x₄)]	=	0
[pushs(x₁, x₂)]	=	0
[case8^#(x₁,...,x₄)]	=	0
[pending]	=	0
[pushs^#(x₁, x₂)]	=	0
[subtract^#(x₁, x₂)]	=	0
[record_extract^#(x₁, x₂, x₃)]	=	0
[case8(x₁,...,x₄)]	=	0
[or^#(x₁, x₂)]	=	0
[case5^#(x₁,...,x₄)]	=	0
[locker2_add_pending(x₁, x₂, x₃)]	=	0
[case4(x₁, x₂, x₃)]	=	0
[imp(x₁, x₂)]	=	0
[element^#(x₁, x₂)]	=	0
[calls(x₁, x₂, x₃)]	=	1
[locker2_map_promote_pending(x₁, x₂)]	=	0
[pops(x₁)]	=	0
[case6(x₁,...,x₄)]	=	0
[and^#(x₁, x₂)]	=	0
[case9^#(x₁,...,x₄)]	=	0
[not(x₁)]	=	0
[andt(x₁, x₂)]	=	0
[locker2_remove_pending^#(x₁, x₂)]	=	0
[gen_modtageq^#(x₁, x₂)]	=	0

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pair

locker2_check_availables^#(cons(Resource,Resources),Locks)

→

locker2_check_availables^#(Resources,Locks)

(401)

could be deleted.

1.1.3.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 4^th component contains the pair

subtract^#(List,cons(Head,Tail))

→

subtract^#(delete(Head,List),Tail)

(422)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a]	=	0
[locker2_promote_pending^#(x₁, x₂)]	=	0
[locker2_promote_pending(x₁, x₂)]	=	0
[locker2_check_availables(x₁, x₂)]	=	0
[element(x₁, x₂)]	=	0
[record_extract(x₁, x₂, x₃)]	=	0
[case6^#(x₁,...,x₄)]	=	0
[tuplenil(x₁)]	=	0
[s(x₁)]	=	0
[case2^#(x₁, x₂, x₃)]	=	0
[append^#(x₁, x₂)]	=	0
[resource]	=	0
[locker2_obtainable(x₁, x₂)]	=	0
[locker2_adduniq(x₁, x₂)]	=	0
[locker2_add_pending^#(x₁, x₂, x₃)]	=	0
[member(x₁, x₂)]	=	0
[case4^#(x₁, x₂, x₃)]	=	0
[T]	=	0
[lock]	=	0
[locker2_release_lock^#(x₁, x₂)]	=	0
[F]	=	0
[and(x₁, x₂)]	=	0
[locker2_map_add_pending(x₁, x₂, x₃)]	=	0
[eq(x₁, x₂)]	=	0
[stack(x₁, x₂)]	=	0
[locker2_map_claim_lock(x₁, x₂, x₃)]	=	0
[tag]	=	0
[record_updates(x₁, x₂, x₃)]	=	0
[locker2_adduniq^#(x₁, x₂)]	=	0
[false]	=	1
[excl]	=	0
[locker2_map_claim_lock^#(x₁, x₂, x₃)]	=	0
[excllock]	=	0
[case5(x₁,...,x₄)]	=	0
[tops^#(x₁)]	=	0
[case1(x₁,...,x₄)]	=	0
[pops^#(x₁)]	=	0
[record_update(x₁,...,x₄)]	=	0
[locker2_claim_lock(x₁, x₂, x₃)]	=	0
[pid(x₁)]	=	0
[eqc^#(x₁, x₂)]	=	0
[push1(x₁,...,x₆)]	=	0
[locker2_remove_pending(x₁, x₂)]	=	0
[eqt^#(x₁, x₂)]	=	0
[true]	=	33036
[eqs^#(x₁, x₂)]	=	0
[eq^#(x₁, x₂)]	=	0
[not^#(x₁)]	=	0
[delete(x₁, x₂)]	=	x₁ + x₂ + 2438
[record_new^#(x₁)]	=	0
[record_updates^#(x₁, x₂, x₃)]	=	0
[locker2_map_promote_pending^#(x₁, x₂)]	=	0
[push1^#(x₁,...,x₆)]	=	0
[ok]	=	0
[append(x₁, x₂)]	=	0
[istops(x₁, x₂)]	=	0
[push^#(x₁, x₂, x₃)]	=	0
[if(x₁, x₂, x₃)]	=	0
[0]	=	0
[record_update^#(x₁,...,x₄)]	=	0
[push(x₁, x₂, x₃)]	=	0
[locker2_obtainables(x₁, x₂)]	=	0
[tops(x₁)]	=	0
[case0(x₁, x₂, x₃)]	=	0
[gen_tag^#(x₁)]	=	0
[locker2_check_available(x₁, x₂)]	=	0
[locker2_map_add_pending^#(x₁, x₂, x₃)]	=	0
[nil]	=	17221
[imp^#(x₁, x₂)]	=	0
[or(x₁, x₂)]	=	0
[locker2_release_lock(x₁, x₂)]	=	0
[istops^#(x₁, x₂)]	=	0
[locker2_check_available^#(x₁, x₂)]	=	0
[locker2_check_availables^#(x₁, x₂)]	=	0
[locker]	=	0
[mcrlrecord]	=	0
[release]	=	0
[case0^#(x₁, x₂, x₃)]	=	0
[gen_tag(x₁)]	=	0
[delete^#(x₁, x₂)]	=	0
[gen_modtageq(x₁, x₂)]	=	0
[tuple(x₁, x₂)]	=	0
[eqc(x₁, x₂)]	=	0
[int(x₁)]	=	0
[subtract(x₁, x₂)]	=	0
[case2(x₁, x₂, x₃)]	=	0
[locker2_obtainables^#(x₁, x₂)]	=	0
[undefined]	=	0
[request]	=	0
[eqs(x₁, x₂)]	=	0
[record_new(x₁)]	=	0
[nocalls]	=	0
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[member^#(x₁, x₂)]	=	0
[if^#(x₁, x₂, x₃)]	=	0
[eqt(x₁, x₂)]	=	0
[equal(x₁, x₂)]	=	2440
[case9(x₁,...,x₄)]	=	0
[empty]	=	0
[case1^#(x₁,...,x₄)]	=	0
[pushs(x₁, x₂)]	=	0
[case8^#(x₁,...,x₄)]	=	0
[pending]	=	0
[pushs^#(x₁, x₂)]	=	0
[subtract^#(x₁, x₂)]	=	x₂ + 0
[record_extract^#(x₁, x₂, x₃)]	=	0
[case8(x₁,...,x₄)]	=	x₄ + 0
[or^#(x₁, x₂)]	=	0
[case5^#(x₁,...,x₄)]	=	0
[locker2_add_pending(x₁, x₂, x₃)]	=	0
[case4(x₁, x₂, x₃)]	=	0
[imp(x₁, x₂)]	=	0
[element^#(x₁, x₂)]	=	0
[calls(x₁, x₂, x₃)]	=	1
[locker2_map_promote_pending(x₁, x₂)]	=	0
[pops(x₁)]	=	0
[case6(x₁,...,x₄)]	=	0
[and^#(x₁, x₂)]	=	0
[case9^#(x₁,...,x₄)]	=	0
[not(x₁)]	=	0
[andt(x₁, x₂)]	=	0
[locker2_remove_pending^#(x₁, x₂)]	=	0
[gen_modtageq^#(x₁, x₂)]	=	0

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pair

subtract^#(List,cons(Head,Tail))

→

subtract^#(delete(Head,List),Tail)

(422)

could be deleted.

1.1.4.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 5^th component contains the pair

locker2_map_claim_lock^#(cons(Lock,Locks),Resources,Client)

→

locker2_map_claim_lock^#(Locks,Resources,Client)

(386)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a]	=	0
[locker2_promote_pending^#(x₁, x₂)]	=	0
[locker2_promote_pending(x₁, x₂)]	=	0
[locker2_check_availables(x₁, x₂)]	=	0
[element(x₁, x₂)]	=	0
[record_extract(x₁, x₂, x₃)]	=	0
[case6^#(x₁,...,x₄)]	=	0
[tuplenil(x₁)]	=	0
[s(x₁)]	=	0
[case2^#(x₁, x₂, x₃)]	=	0
[append^#(x₁, x₂)]	=	0
[resource]	=	0
[locker2_obtainable(x₁, x₂)]	=	0
[locker2_adduniq(x₁, x₂)]	=	0
[locker2_add_pending^#(x₁, x₂, x₃)]	=	0
[member(x₁, x₂)]	=	0
[case4^#(x₁, x₂, x₃)]	=	0
[T]	=	0
[lock]	=	0
[locker2_release_lock^#(x₁, x₂)]	=	0
[F]	=	0
[and(x₁, x₂)]	=	0
[locker2_map_add_pending(x₁, x₂, x₃)]	=	0
[eq(x₁, x₂)]	=	0
[stack(x₁, x₂)]	=	0
[locker2_map_claim_lock(x₁, x₂, x₃)]	=	0
[tag]	=	0
[record_updates(x₁, x₂, x₃)]	=	0
[locker2_adduniq^#(x₁, x₂)]	=	0
[false]	=	1
[excl]	=	0
[locker2_map_claim_lock^#(x₁, x₂, x₃)]	=	x₁ + 0
[excllock]	=	0
[case5(x₁,...,x₄)]	=	0
[tops^#(x₁)]	=	0
[case1(x₁,...,x₄)]	=	0
[pops^#(x₁)]	=	0
[record_update(x₁,...,x₄)]	=	0
[locker2_claim_lock(x₁, x₂, x₃)]	=	0
[pid(x₁)]	=	0
[eqc^#(x₁, x₂)]	=	0
[push1(x₁,...,x₆)]	=	0
[locker2_remove_pending(x₁, x₂)]	=	0
[eqt^#(x₁, x₂)]	=	0
[true]	=	1
[eqs^#(x₁, x₂)]	=	0
[eq^#(x₁, x₂)]	=	0
[not^#(x₁)]	=	0
[delete(x₁, x₂)]	=	x₁ + x₂ + 2438
[record_new^#(x₁)]	=	0
[record_updates^#(x₁, x₂, x₃)]	=	0
[locker2_map_promote_pending^#(x₁, x₂)]	=	0
[push1^#(x₁,...,x₆)]	=	0
[ok]	=	0
[append(x₁, x₂)]	=	0
[istops(x₁, x₂)]	=	0
[push^#(x₁, x₂, x₃)]	=	0
[if(x₁, x₂, x₃)]	=	0
[0]	=	0
[record_update^#(x₁,...,x₄)]	=	0
[push(x₁, x₂, x₃)]	=	0
[locker2_obtainables(x₁, x₂)]	=	0
[tops(x₁)]	=	0
[case0(x₁, x₂, x₃)]	=	0
[gen_tag^#(x₁)]	=	0
[locker2_check_available(x₁, x₂)]	=	0
[locker2_map_add_pending^#(x₁, x₂, x₃)]	=	0
[nil]	=	17221
[imp^#(x₁, x₂)]	=	0
[or(x₁, x₂)]	=	0
[locker2_release_lock(x₁, x₂)]	=	0
[istops^#(x₁, x₂)]	=	0
[locker2_check_available^#(x₁, x₂)]	=	0
[locker2_check_availables^#(x₁, x₂)]	=	0
[locker]	=	0
[mcrlrecord]	=	0
[release]	=	0
[case0^#(x₁, x₂, x₃)]	=	0
[gen_tag(x₁)]	=	0
[delete^#(x₁, x₂)]	=	0
[gen_modtageq(x₁, x₂)]	=	0
[tuple(x₁, x₂)]	=	0
[eqc(x₁, x₂)]	=	0
[int(x₁)]	=	0
[subtract(x₁, x₂)]	=	0
[case2(x₁, x₂, x₃)]	=	0
[locker2_obtainables^#(x₁, x₂)]	=	0
[undefined]	=	0
[request]	=	0
[eqs(x₁, x₂)]	=	0
[record_new(x₁)]	=	0
[nocalls]	=	0
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[member^#(x₁, x₂)]	=	0
[if^#(x₁, x₂, x₃)]	=	0
[eqt(x₁, x₂)]	=	0
[equal(x₁, x₂)]	=	2440
[case9(x₁,...,x₄)]	=	0
[empty]	=	0
[case1^#(x₁,...,x₄)]	=	0
[pushs(x₁, x₂)]	=	0
[case8^#(x₁,...,x₄)]	=	0
[pending]	=	0
[pushs^#(x₁, x₂)]	=	0
[subtract^#(x₁, x₂)]	=	0
[record_extract^#(x₁, x₂, x₃)]	=	0
[case8(x₁,...,x₄)]	=	x₄ + 0
[or^#(x₁, x₂)]	=	0
[case5^#(x₁,...,x₄)]	=	0
[locker2_add_pending(x₁, x₂, x₃)]	=	0
[case4(x₁, x₂, x₃)]	=	0
[imp(x₁, x₂)]	=	0
[element^#(x₁, x₂)]	=	0
[calls(x₁, x₂, x₃)]	=	1
[locker2_map_promote_pending(x₁, x₂)]	=	0
[pops(x₁)]	=	0
[case6(x₁,...,x₄)]	=	0
[and^#(x₁, x₂)]	=	0
[case9^#(x₁,...,x₄)]	=	0
[not(x₁)]	=	0
[andt(x₁, x₂)]	=	0
[locker2_remove_pending^#(x₁, x₂)]	=	0
[gen_modtageq^#(x₁, x₂)]	=	0

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pair

locker2_map_claim_lock^#(cons(Lock,Locks),Resources,Client)

→

locker2_map_claim_lock^#(Locks,Resources,Client)

(386)

could be deleted.

1.1.5.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 6^th component contains the pair

element^#(int(s(s(N1))),tuple(T1,T2))

→

element^#(int(s(N1)),T2)

(384)

1.1.6 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a]	=	0
[locker2_promote_pending^#(x₁, x₂)]	=	0
[locker2_promote_pending(x₁, x₂)]	=	0
[locker2_check_availables(x₁, x₂)]	=	0
[element(x₁, x₂)]	=	0
[record_extract(x₁, x₂, x₃)]	=	0
[case6^#(x₁,...,x₄)]	=	0
[tuplenil(x₁)]	=	0
[s(x₁)]	=	x₁ + 1
[case2^#(x₁, x₂, x₃)]	=	0
[append^#(x₁, x₂)]	=	0
[resource]	=	0
[locker2_obtainable(x₁, x₂)]	=	0
[locker2_adduniq(x₁, x₂)]	=	0
[locker2_add_pending^#(x₁, x₂, x₃)]	=	0
[member(x₁, x₂)]	=	0
[case4^#(x₁, x₂, x₃)]	=	0
[T]	=	0
[lock]	=	0
[locker2_release_lock^#(x₁, x₂)]	=	0
[F]	=	0
[and(x₁, x₂)]	=	0
[locker2_map_add_pending(x₁, x₂, x₃)]	=	0
[eq(x₁, x₂)]	=	0
[stack(x₁, x₂)]	=	0
[locker2_map_claim_lock(x₁, x₂, x₃)]	=	0
[tag]	=	0
[record_updates(x₁, x₂, x₃)]	=	0
[locker2_adduniq^#(x₁, x₂)]	=	0
[false]	=	1
[excl]	=	0
[locker2_map_claim_lock^#(x₁, x₂, x₃)]	=	0
[excllock]	=	0
[case5(x₁,...,x₄)]	=	0
[tops^#(x₁)]	=	0
[case1(x₁,...,x₄)]	=	0
[pops^#(x₁)]	=	0
[record_update(x₁,...,x₄)]	=	0
[locker2_claim_lock(x₁, x₂, x₃)]	=	0
[pid(x₁)]	=	0
[eqc^#(x₁, x₂)]	=	0
[push1(x₁,...,x₆)]	=	0
[locker2_remove_pending(x₁, x₂)]	=	0
[eqt^#(x₁, x₂)]	=	0
[true]	=	1
[eqs^#(x₁, x₂)]	=	0
[eq^#(x₁, x₂)]	=	0
[not^#(x₁)]	=	0
[delete(x₁, x₂)]	=	x₁ + x₂ + 2438
[record_new^#(x₁)]	=	0
[record_updates^#(x₁, x₂, x₃)]	=	0
[locker2_map_promote_pending^#(x₁, x₂)]	=	0
[push1^#(x₁,...,x₆)]	=	0
[ok]	=	0
[append(x₁, x₂)]	=	0
[istops(x₁, x₂)]	=	0
[push^#(x₁, x₂, x₃)]	=	0
[if(x₁, x₂, x₃)]	=	0
[0]	=	0
[record_update^#(x₁,...,x₄)]	=	0
[push(x₁, x₂, x₃)]	=	0
[locker2_obtainables(x₁, x₂)]	=	0
[tops(x₁)]	=	0
[case0(x₁, x₂, x₃)]	=	0
[gen_tag^#(x₁)]	=	0
[locker2_check_available(x₁, x₂)]	=	0
[locker2_map_add_pending^#(x₁, x₂, x₃)]	=	0
[nil]	=	17221
[imp^#(x₁, x₂)]	=	0
[or(x₁, x₂)]	=	0
[locker2_release_lock(x₁, x₂)]	=	0
[istops^#(x₁, x₂)]	=	0
[locker2_check_available^#(x₁, x₂)]	=	0
[locker2_check_availables^#(x₁, x₂)]	=	0
[locker]	=	0
[mcrlrecord]	=	0
[release]	=	0
[case0^#(x₁, x₂, x₃)]	=	0
[gen_tag(x₁)]	=	0
[delete^#(x₁, x₂)]	=	0
[gen_modtageq(x₁, x₂)]	=	0
[tuple(x₁, x₂)]	=	x₂ + 58713
[eqc(x₁, x₂)]	=	0
[int(x₁)]	=	x₁ + 5853
[subtract(x₁, x₂)]	=	0
[case2(x₁, x₂, x₃)]	=	0
[locker2_obtainables^#(x₁, x₂)]	=	0
[undefined]	=	0
[request]	=	0
[eqs(x₁, x₂)]	=	0
[record_new(x₁)]	=	0
[nocalls]	=	0
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[member^#(x₁, x₂)]	=	0
[if^#(x₁, x₂, x₃)]	=	0
[eqt(x₁, x₂)]	=	0
[equal(x₁, x₂)]	=	2440
[case9(x₁,...,x₄)]	=	0
[empty]	=	0
[case1^#(x₁,...,x₄)]	=	0
[pushs(x₁, x₂)]	=	0
[case8^#(x₁,...,x₄)]	=	0
[pending]	=	0
[pushs^#(x₁, x₂)]	=	0
[subtract^#(x₁, x₂)]	=	0
[record_extract^#(x₁, x₂, x₃)]	=	0
[case8(x₁,...,x₄)]	=	x₄ + 0
[or^#(x₁, x₂)]	=	0
[case5^#(x₁,...,x₄)]	=	0
[locker2_add_pending(x₁, x₂, x₃)]	=	0
[case4(x₁, x₂, x₃)]	=	0
[imp(x₁, x₂)]	=	0
[element^#(x₁, x₂)]	=	x₁ + x₂ + 0
[calls(x₁, x₂, x₃)]	=	1
[locker2_map_promote_pending(x₁, x₂)]	=	0
[pops(x₁)]	=	0
[case6(x₁,...,x₄)]	=	0
[and^#(x₁, x₂)]	=	0
[case9^#(x₁,...,x₄)]	=	0
[not(x₁)]	=	0
[andt(x₁, x₂)]	=	0
[locker2_remove_pending^#(x₁, x₂)]	=	0
[gen_modtageq^#(x₁, x₂)]	=	0

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pair

element^#(int(s(s(N1))),tuple(T1,T2))

→

element^#(int(s(N1)),T2)

(384)

could be deleted.

1.1.6.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 7^th component contains the pair

append^#(cons(Head,Tail),List)

→

append^#(Tail,List)

(382)

1.1.7 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a]	=	0
[locker2_promote_pending^#(x₁, x₂)]	=	0
[locker2_promote_pending(x₁, x₂)]	=	0
[locker2_check_availables(x₁, x₂)]	=	0
[element(x₁, x₂)]	=	0
[record_extract(x₁, x₂, x₃)]	=	0
[case6^#(x₁,...,x₄)]	=	0
[tuplenil(x₁)]	=	0
[s(x₁)]	=	1
[case2^#(x₁, x₂, x₃)]	=	0
[append^#(x₁, x₂)]	=	x₁ + 0
[resource]	=	0
[locker2_obtainable(x₁, x₂)]	=	0
[locker2_adduniq(x₁, x₂)]	=	0
[locker2_add_pending^#(x₁, x₂, x₃)]	=	0
[member(x₁, x₂)]	=	0
[case4^#(x₁, x₂, x₃)]	=	0
[T]	=	0
[lock]	=	0
[locker2_release_lock^#(x₁, x₂)]	=	0
[F]	=	0
[and(x₁, x₂)]	=	0
[locker2_map_add_pending(x₁, x₂, x₃)]	=	0
[eq(x₁, x₂)]	=	0
[stack(x₁, x₂)]	=	0
[locker2_map_claim_lock(x₁, x₂, x₃)]	=	0
[tag]	=	0
[record_updates(x₁, x₂, x₃)]	=	0
[locker2_adduniq^#(x₁, x₂)]	=	0
[false]	=	1
[excl]	=	0
[locker2_map_claim_lock^#(x₁, x₂, x₃)]	=	0
[excllock]	=	0
[case5(x₁,...,x₄)]	=	0
[tops^#(x₁)]	=	0
[case1(x₁,...,x₄)]	=	0
[pops^#(x₁)]	=	0
[record_update(x₁,...,x₄)]	=	0
[locker2_claim_lock(x₁, x₂, x₃)]	=	0
[pid(x₁)]	=	0
[eqc^#(x₁, x₂)]	=	0
[push1(x₁,...,x₆)]	=	0
[locker2_remove_pending(x₁, x₂)]	=	0
[eqt^#(x₁, x₂)]	=	0
[true]	=	1
[eqs^#(x₁, x₂)]	=	0
[eq^#(x₁, x₂)]	=	0
[not^#(x₁)]	=	0
[delete(x₁, x₂)]	=	x₁ + x₂ + 16203
[record_new^#(x₁)]	=	0
[record_updates^#(x₁, x₂, x₃)]	=	0
[locker2_map_promote_pending^#(x₁, x₂)]	=	0
[push1^#(x₁,...,x₆)]	=	0
[ok]	=	0
[append(x₁, x₂)]	=	0
[istops(x₁, x₂)]	=	0
[push^#(x₁, x₂, x₃)]	=	0
[if(x₁, x₂, x₃)]	=	0
[0]	=	0
[record_update^#(x₁,...,x₄)]	=	0
[push(x₁, x₂, x₃)]	=	0
[locker2_obtainables(x₁, x₂)]	=	0
[tops(x₁)]	=	0
[case0(x₁, x₂, x₃)]	=	0
[gen_tag^#(x₁)]	=	0
[locker2_check_available(x₁, x₂)]	=	0
[locker2_map_add_pending^#(x₁, x₂, x₃)]	=	0
[nil]	=	17221
[imp^#(x₁, x₂)]	=	0
[or(x₁, x₂)]	=	0
[locker2_release_lock(x₁, x₂)]	=	0
[istops^#(x₁, x₂)]	=	0
[locker2_check_available^#(x₁, x₂)]	=	0
[locker2_check_availables^#(x₁, x₂)]	=	0
[locker]	=	0
[mcrlrecord]	=	0
[release]	=	0
[case0^#(x₁, x₂, x₃)]	=	0
[gen_tag(x₁)]	=	0
[delete^#(x₁, x₂)]	=	0
[gen_modtageq(x₁, x₂)]	=	0
[tuple(x₁, x₂)]	=	58713
[eqc(x₁, x₂)]	=	0
[int(x₁)]	=	5853
[subtract(x₁, x₂)]	=	0
[case2(x₁, x₂, x₃)]	=	0
[locker2_obtainables^#(x₁, x₂)]	=	0
[undefined]	=	0
[request]	=	0
[eqs(x₁, x₂)]	=	0
[record_new(x₁)]	=	0
[nocalls]	=	0
[cons(x₁, x₂)]	=	x₁ + x₂ + 20538
[member^#(x₁, x₂)]	=	0
[if^#(x₁, x₂, x₃)]	=	0
[eqt(x₁, x₂)]	=	0
[equal(x₁, x₂)]	=	3
[case9(x₁,...,x₄)]	=	0
[empty]	=	0
[case1^#(x₁,...,x₄)]	=	0
[pushs(x₁, x₂)]	=	0
[case8^#(x₁,...,x₄)]	=	0
[pending]	=	0
[pushs^#(x₁, x₂)]	=	0
[subtract^#(x₁, x₂)]	=	0
[record_extract^#(x₁, x₂, x₃)]	=	0
[case8(x₁,...,x₄)]	=	x₄ + 36739
[or^#(x₁, x₂)]	=	0
[case5^#(x₁,...,x₄)]	=	0
[locker2_add_pending(x₁, x₂, x₃)]	=	0
[case4(x₁, x₂, x₃)]	=	0
[imp(x₁, x₂)]	=	0
[element^#(x₁, x₂)]	=	0
[calls(x₁, x₂, x₃)]	=	1
[locker2_map_promote_pending(x₁, x₂)]	=	0
[pops(x₁)]	=	0
[case6(x₁,...,x₄)]	=	0
[and^#(x₁, x₂)]	=	0
[case9^#(x₁,...,x₄)]	=	0
[not(x₁)]	=	0
[andt(x₁, x₂)]	=	0
[locker2_remove_pending^#(x₁, x₂)]	=	0
[gen_modtageq^#(x₁, x₂)]	=	0

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pair

append^#(cons(Head,Tail),List)

→

append^#(Tail,List)

(382)

could be deleted.

1.1.7.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 8^th component contains the pair

eqs^#(stack(E1,S1),stack(E2,S2))

→

eqs^#(S1,S2)

(414)

1.1.8 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a]	=	0
[locker2_promote_pending^#(x₁, x₂)]	=	0
[locker2_promote_pending(x₁, x₂)]	=	0
[locker2_check_availables(x₁, x₂)]	=	0
[element(x₁, x₂)]	=	0
[record_extract(x₁, x₂, x₃)]	=	0
[case6^#(x₁,...,x₄)]	=	0
[tuplenil(x₁)]	=	0
[s(x₁)]	=	1
[case2^#(x₁, x₂, x₃)]	=	0
[append^#(x₁, x₂)]	=	0
[resource]	=	0
[locker2_obtainable(x₁, x₂)]	=	0
[locker2_adduniq(x₁, x₂)]	=	0
[locker2_add_pending^#(x₁, x₂, x₃)]	=	0
[member(x₁, x₂)]	=	0
[case4^#(x₁, x₂, x₃)]	=	0
[T]	=	0
[lock]	=	0
[locker2_release_lock^#(x₁, x₂)]	=	0
[F]	=	0
[and(x₁, x₂)]	=	0
[locker2_map_add_pending(x₁, x₂, x₃)]	=	0
[eq(x₁, x₂)]	=	0
[stack(x₁, x₂)]	=	x₂ + 1
[locker2_map_claim_lock(x₁, x₂, x₃)]	=	0
[tag]	=	0
[record_updates(x₁, x₂, x₃)]	=	0
[locker2_adduniq^#(x₁, x₂)]	=	0
[false]	=	1
[excl]	=	0
[locker2_map_claim_lock^#(x₁, x₂, x₃)]	=	0
[excllock]	=	0
[case5(x₁,...,x₄)]	=	0
[tops^#(x₁)]	=	0
[case1(x₁,...,x₄)]	=	0
[pops^#(x₁)]	=	0
[record_update(x₁,...,x₄)]	=	0
[locker2_claim_lock(x₁, x₂, x₃)]	=	0
[pid(x₁)]	=	0
[eqc^#(x₁, x₂)]	=	0
[push1(x₁,...,x₆)]	=	0
[locker2_remove_pending(x₁, x₂)]	=	0
[eqt^#(x₁, x₂)]	=	0
[true]	=	1
[eqs^#(x₁, x₂)]	=	x₁ + x₂ + 0
[eq^#(x₁, x₂)]	=	0
[not^#(x₁)]	=	0
[delete(x₁, x₂)]	=	x₁ + x₂ + 6296
[record_new^#(x₁)]	=	0
[record_updates^#(x₁, x₂, x₃)]	=	0
[locker2_map_promote_pending^#(x₁, x₂)]	=	0
[push1^#(x₁,...,x₆)]	=	0
[ok]	=	0
[append(x₁, x₂)]	=	0
[istops(x₁, x₂)]	=	0
[push^#(x₁, x₂, x₃)]	=	0
[if(x₁, x₂, x₃)]	=	0
[0]	=	0
[record_update^#(x₁,...,x₄)]	=	0
[push(x₁, x₂, x₃)]	=	0
[locker2_obtainables(x₁, x₂)]	=	0
[tops(x₁)]	=	0
[case0(x₁, x₂, x₃)]	=	0
[gen_tag^#(x₁)]	=	0
[locker2_check_available(x₁, x₂)]	=	0
[locker2_map_add_pending^#(x₁, x₂, x₃)]	=	0
[nil]	=	34889
[imp^#(x₁, x₂)]	=	0
[or(x₁, x₂)]	=	0
[locker2_release_lock(x₁, x₂)]	=	0
[istops^#(x₁, x₂)]	=	0
[locker2_check_available^#(x₁, x₂)]	=	0
[locker2_check_availables^#(x₁, x₂)]	=	0
[locker]	=	0
[mcrlrecord]	=	0
[release]	=	0
[case0^#(x₁, x₂, x₃)]	=	0
[gen_tag(x₁)]	=	0
[delete^#(x₁, x₂)]	=	0
[gen_modtageq(x₁, x₂)]	=	0
[tuple(x₁, x₂)]	=	58713
[eqc(x₁, x₂)]	=	0
[int(x₁)]	=	5853
[subtract(x₁, x₂)]	=	0
[case2(x₁, x₂, x₃)]	=	0
[locker2_obtainables^#(x₁, x₂)]	=	0
[undefined]	=	0
[request]	=	0
[eqs(x₁, x₂)]	=	0
[record_new(x₁)]	=	0
[nocalls]	=	0
[cons(x₁, x₂)]	=	x₁ + x₂ + 8386
[member^#(x₁, x₂)]	=	0
[if^#(x₁, x₂, x₃)]	=	0
[eqt(x₁, x₂)]	=	0
[equal(x₁, x₂)]	=	3
[case9(x₁,...,x₄)]	=	0
[empty]	=	0
[case1^#(x₁,...,x₄)]	=	0
[pushs(x₁, x₂)]	=	0
[case8^#(x₁,...,x₄)]	=	0
[pending]	=	0
[pushs^#(x₁, x₂)]	=	0
[subtract^#(x₁, x₂)]	=	0
[record_extract^#(x₁, x₂, x₃)]	=	0
[case8(x₁,...,x₄)]	=	x₄ + 14680
[or^#(x₁, x₂)]	=	0
[case5^#(x₁,...,x₄)]	=	0
[locker2_add_pending(x₁, x₂, x₃)]	=	0
[case4(x₁, x₂, x₃)]	=	0
[imp(x₁, x₂)]	=	0
[element^#(x₁, x₂)]	=	0
[calls(x₁, x₂, x₃)]	=	1
[locker2_map_promote_pending(x₁, x₂)]	=	0
[pops(x₁)]	=	0
[case6(x₁,...,x₄)]	=	0
[and^#(x₁, x₂)]	=	0
[case9^#(x₁,...,x₄)]	=	0
[not(x₁)]	=	0
[andt(x₁, x₂)]	=	0
[locker2_remove_pending^#(x₁, x₂)]	=	0
[gen_modtageq^#(x₁, x₂)]	=	0

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pair

eqs^#(stack(E1,S1),stack(E2,S2))

→

eqs^#(S1,S2)

(414)

could be deleted.

1.1.8.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 9^th component contains the pair

eqt^#(tuplenil(H1),tuplenil(H2))	→	eqt^#(H1,H2)	(397)
eqt^#(cons(H1,T1),cons(H2,T2))	→	eqt^#(H1,H2)	(423)
eqt^#(tuple(H1,T1),tuple(H2,T2))	→	eqt^#(H1,H2)	(392)
eqt^#(cons(H1,T1),cons(H2,T2))	→	eqt^#(T1,T2)	(390)
eqt^#(pid(N1),pid(N2))	→	eqt^#(N1,N2)	(389)
eqt^#(tuple(H1,T1),tuple(H2,T2))	→	eqt^#(T1,T2)	(413)

1.1.9 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a]	=	0
[locker2_promote_pending^#(x₁, x₂)]	=	0
[locker2_promote_pending(x₁, x₂)]	=	0
[locker2_check_availables(x₁, x₂)]	=	0
[element(x₁, x₂)]	=	0
[record_extract(x₁, x₂, x₃)]	=	0
[case6^#(x₁,...,x₄)]	=	0
[tuplenil(x₁)]	=	x₁ + 1
[s(x₁)]	=	1
[case2^#(x₁, x₂, x₃)]	=	0
[append^#(x₁, x₂)]	=	0
[resource]	=	0
[locker2_obtainable(x₁, x₂)]	=	0
[locker2_adduniq(x₁, x₂)]	=	0
[locker2_add_pending^#(x₁, x₂, x₃)]	=	0
[member(x₁, x₂)]	=	0
[case4^#(x₁, x₂, x₃)]	=	0
[T]	=	0
[lock]	=	0
[locker2_release_lock^#(x₁, x₂)]	=	0
[F]	=	0
[and(x₁, x₂)]	=	0
[locker2_map_add_pending(x₁, x₂, x₃)]	=	0
[eq(x₁, x₂)]	=	0
[stack(x₁, x₂)]	=	1
[locker2_map_claim_lock(x₁, x₂, x₃)]	=	0
[tag]	=	0
[record_updates(x₁, x₂, x₃)]	=	0
[locker2_adduniq^#(x₁, x₂)]	=	0
[false]	=	1
[excl]	=	0
[locker2_map_claim_lock^#(x₁, x₂, x₃)]	=	0
[excllock]	=	0
[case5(x₁,...,x₄)]	=	0
[tops^#(x₁)]	=	0
[case1(x₁,...,x₄)]	=	0
[pops^#(x₁)]	=	0
[record_update(x₁,...,x₄)]	=	0
[locker2_claim_lock(x₁, x₂, x₃)]	=	0
[pid(x₁)]	=	x₁ + 1
[eqc^#(x₁, x₂)]	=	0
[push1(x₁,...,x₆)]	=	0
[locker2_remove_pending(x₁, x₂)]	=	0
[eqt^#(x₁, x₂)]	=	x₁ + x₂ + 0
[true]	=	1
[eqs^#(x₁, x₂)]	=	0
[eq^#(x₁, x₂)]	=	0
[not^#(x₁)]	=	0
[delete(x₁, x₂)]	=	x₁ + x₂ + 6296
[record_new^#(x₁)]	=	0
[record_updates^#(x₁, x₂, x₃)]	=	0
[locker2_map_promote_pending^#(x₁, x₂)]	=	0
[push1^#(x₁,...,x₆)]	=	0
[ok]	=	0
[append(x₁, x₂)]	=	0
[istops(x₁, x₂)]	=	0
[push^#(x₁, x₂, x₃)]	=	0
[if(x₁, x₂, x₃)]	=	0
[0]	=	0
[record_update^#(x₁,...,x₄)]	=	0
[push(x₁, x₂, x₃)]	=	0
[locker2_obtainables(x₁, x₂)]	=	0
[tops(x₁)]	=	0
[case0(x₁, x₂, x₃)]	=	0
[gen_tag^#(x₁)]	=	0
[locker2_check_available(x₁, x₂)]	=	0
[locker2_map_add_pending^#(x₁, x₂, x₃)]	=	0
[nil]	=	1
[imp^#(x₁, x₂)]	=	0
[or(x₁, x₂)]	=	0
[locker2_release_lock(x₁, x₂)]	=	0
[istops^#(x₁, x₂)]	=	0
[locker2_check_available^#(x₁, x₂)]	=	0
[locker2_check_availables^#(x₁, x₂)]	=	0
[locker]	=	0
[mcrlrecord]	=	0
[release]	=	0
[case0^#(x₁, x₂, x₃)]	=	0
[gen_tag(x₁)]	=	0
[delete^#(x₁, x₂)]	=	0
[gen_modtageq(x₁, x₂)]	=	0
[tuple(x₁, x₂)]	=	x₁ + x₂ + 3037
[eqc(x₁, x₂)]	=	0
[int(x₁)]	=	5853
[subtract(x₁, x₂)]	=	0
[case2(x₁, x₂, x₃)]	=	0
[locker2_obtainables^#(x₁, x₂)]	=	0
[undefined]	=	0
[request]	=	0
[eqs(x₁, x₂)]	=	0
[record_new(x₁)]	=	0
[nocalls]	=	0
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[member^#(x₁, x₂)]	=	0
[if^#(x₁, x₂, x₃)]	=	0
[eqt(x₁, x₂)]	=	0
[equal(x₁, x₂)]	=	3
[case9(x₁,...,x₄)]	=	0
[empty]	=	0
[case1^#(x₁,...,x₄)]	=	0
[pushs(x₁, x₂)]	=	0
[case8^#(x₁,...,x₄)]	=	0
[pending]	=	0
[pushs^#(x₁, x₂)]	=	0
[subtract^#(x₁, x₂)]	=	0
[record_extract^#(x₁, x₂, x₃)]	=	0
[case8(x₁,...,x₄)]	=	x₄ + 6295
[or^#(x₁, x₂)]	=	0
[case5^#(x₁,...,x₄)]	=	0
[locker2_add_pending(x₁, x₂, x₃)]	=	0
[case4(x₁, x₂, x₃)]	=	0
[imp(x₁, x₂)]	=	0
[element^#(x₁, x₂)]	=	0
[calls(x₁, x₂, x₃)]	=	1
[locker2_map_promote_pending(x₁, x₂)]	=	0
[pops(x₁)]	=	0
[case6(x₁,...,x₄)]	=	0
[and^#(x₁, x₂)]	=	0
[case9^#(x₁,...,x₄)]	=	0
[not(x₁)]	=	0
[andt(x₁, x₂)]	=	0
[locker2_remove_pending^#(x₁, x₂)]	=	0
[gen_modtageq^#(x₁, x₂)]	=	0

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pairs

eqt^#(tuplenil(H1),tuplenil(H2))	→	eqt^#(H1,H2)	(397)
eqt^#(cons(H1,T1),cons(H2,T2))	→	eqt^#(H1,H2)	(423)
eqt^#(tuple(H1,T1),tuple(H2,T2))	→	eqt^#(H1,H2)	(392)
eqt^#(cons(H1,T1),cons(H2,T2))	→	eqt^#(T1,T2)	(390)
eqt^#(pid(N1),pid(N2))	→	eqt^#(N1,N2)	(389)
eqt^#(tuple(H1,T1),tuple(H2,T2))	→	eqt^#(T1,T2)	(413)

could be deleted.

1.1.9.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 10^th component contains the pair

record_updates^#(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields))

→

record_updates^#(record_update(Record,Name,Field,NewF),Name,Fields)

(429)

1.1.10 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a]	=	0
[locker2_promote_pending^#(x₁, x₂)]	=	0
[locker2_promote_pending(x₁, x₂)]	=	0
[locker2_check_availables(x₁, x₂)]	=	0
[element(x₁, x₂)]	=	0
[record_extract(x₁, x₂, x₃)]	=	0
[case6^#(x₁,...,x₄)]	=	0
[tuplenil(x₁)]	=	x₁ + 1
[s(x₁)]	=	1
[case2^#(x₁, x₂, x₃)]	=	0
[append^#(x₁, x₂)]	=	0
[resource]	=	0
[locker2_obtainable(x₁, x₂)]	=	0
[locker2_adduniq(x₁, x₂)]	=	0
[locker2_add_pending^#(x₁, x₂, x₃)]	=	0
[member(x₁, x₂)]	=	0
[case4^#(x₁, x₂, x₃)]	=	0
[T]	=	0
[lock]	=	62709
[locker2_release_lock^#(x₁, x₂)]	=	0
[F]	=	0
[and(x₁, x₂)]	=	0
[locker2_map_add_pending(x₁, x₂, x₃)]	=	0
[eq(x₁, x₂)]	=	0
[stack(x₁, x₂)]	=	1
[locker2_map_claim_lock(x₁, x₂, x₃)]	=	0
[tag]	=	0
[record_updates(x₁, x₂, x₃)]	=	0
[locker2_adduniq^#(x₁, x₂)]	=	0
[false]	=	1
[excl]	=	0
[locker2_map_claim_lock^#(x₁, x₂, x₃)]	=	0
[excllock]	=	0
[case5(x₁,...,x₄)]	=	0
[tops^#(x₁)]	=	0
[case1(x₁,...,x₄)]	=	0
[pops^#(x₁)]	=	0
[record_update(x₁,...,x₄)]	=	x₁ + x₃ + x₄ + 1
[locker2_claim_lock(x₁, x₂, x₃)]	=	0
[pid(x₁)]	=	1
[eqc^#(x₁, x₂)]	=	0
[push1(x₁,...,x₆)]	=	0
[locker2_remove_pending(x₁, x₂)]	=	0
[eqt^#(x₁, x₂)]	=	0
[true]	=	1
[eqs^#(x₁, x₂)]	=	0
[eq^#(x₁, x₂)]	=	0
[not^#(x₁)]	=	0
[delete(x₁, x₂)]	=	x₁ + x₂ + 6296
[record_new^#(x₁)]	=	0
[record_updates^#(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 0
[locker2_map_promote_pending^#(x₁, x₂)]	=	0
[push1^#(x₁,...,x₆)]	=	0
[ok]	=	0
[append(x₁, x₂)]	=	0
[istops(x₁, x₂)]	=	0
[push^#(x₁, x₂, x₃)]	=	0
[if(x₁, x₂, x₃)]	=	0
[0]	=	0
[record_update^#(x₁,...,x₄)]	=	0
[push(x₁, x₂, x₃)]	=	0
[locker2_obtainables(x₁, x₂)]	=	0
[tops(x₁)]	=	0
[case0(x₁, x₂, x₃)]	=	0
[gen_tag^#(x₁)]	=	0
[locker2_check_available(x₁, x₂)]	=	0
[locker2_map_add_pending^#(x₁, x₂, x₃)]	=	0
[nil]	=	1
[imp^#(x₁, x₂)]	=	0
[or(x₁, x₂)]	=	0
[locker2_release_lock(x₁, x₂)]	=	0
[istops^#(x₁, x₂)]	=	0
[locker2_check_available^#(x₁, x₂)]	=	0
[locker2_check_availables^#(x₁, x₂)]	=	0
[locker]	=	0
[mcrlrecord]	=	32797
[release]	=	0
[case0^#(x₁, x₂, x₃)]	=	0
[gen_tag(x₁)]	=	0
[delete^#(x₁, x₂)]	=	0
[gen_modtageq(x₁, x₂)]	=	0
[tuple(x₁, x₂)]	=	x₁ + x₂ + 0
[eqc(x₁, x₂)]	=	0
[int(x₁)]	=	5853
[subtract(x₁, x₂)]	=	0
[case2(x₁, x₂, x₃)]	=	0
[locker2_obtainables^#(x₁, x₂)]	=	0
[undefined]	=	0
[request]	=	0
[eqs(x₁, x₂)]	=	0
[record_new(x₁)]	=	0
[nocalls]	=	0
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[member^#(x₁, x₂)]	=	0
[if^#(x₁, x₂, x₃)]	=	0
[eqt(x₁, x₂)]	=	0
[equal(x₁, x₂)]	=	3
[case9(x₁,...,x₄)]	=	0
[empty]	=	0
[case1^#(x₁,...,x₄)]	=	0
[pushs(x₁, x₂)]	=	0
[case8^#(x₁,...,x₄)]	=	0
[pending]	=	1
[pushs^#(x₁, x₂)]	=	0
[subtract^#(x₁, x₂)]	=	0
[record_extract^#(x₁, x₂, x₃)]	=	0
[case8(x₁,...,x₄)]	=	x₄ + 6295
[or^#(x₁, x₂)]	=	0
[case5^#(x₁,...,x₄)]	=	0
[locker2_add_pending(x₁, x₂, x₃)]	=	0
[case4(x₁, x₂, x₃)]	=	0
[imp(x₁, x₂)]	=	0
[element^#(x₁, x₂)]	=	0
[calls(x₁, x₂, x₃)]	=	1
[locker2_map_promote_pending(x₁, x₂)]	=	0
[pops(x₁)]	=	0
[case6(x₁,...,x₄)]	=	0
[and^#(x₁, x₂)]	=	0
[case9^#(x₁,...,x₄)]	=	0
[not(x₁)]	=	0
[andt(x₁, x₂)]	=	0
[locker2_remove_pending^#(x₁, x₂)]	=	0
[gen_modtageq^#(x₁, x₂)]	=	0

together with the usable rule

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)))))

(320)

(w.r.t. the implicit argument filter of the reduction pair), the pair

record_updates^#(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields))

→

record_updates^#(record_update(Record,Name,Field,NewF),Name,Fields)

(429)

could be deleted.

1.1.10.1 Dependency Graph Processor

The dependency pairs are split into 0 components.