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.