YES

We show the termination of the TRS R:

  or(T(),T()) -> T()
  or(F(),T()) -> T()
  or(T(),F()) -> T()
  or(F(),F()) -> F()
  and(T(),B) -> B
  and(B,T()) -> B
  and(F(),B) -> F()
  and(B,F()) -> F()
  imp(T(),B) -> B
  imp(F(),B) -> T()
  not(T()) -> F()
  not(F()) -> T()
  if(T(),B1,B2) -> B1
  if(F(),B1,B2) -> B2
  eq(T(),T()) -> T()
  eq(F(),F()) -> T()
  eq(T(),F()) -> F()
  eq(F(),T()) -> F()
  eqt(nil(),undefined()) -> F()
  eqt(nil(),pid(N2)) -> F()
  eqt(nil(),int(N2)) -> F()
  eqt(nil(),cons(H2,T2)) -> F()
  eqt(nil(),tuple(H2,T2)) -> F()
  eqt(nil(),tuplenil(H2)) -> F()
  eqt(a(),nil()) -> F()
  eqt(a(),a()) -> T()
  eqt(a(),excl()) -> F()
  eqt(a(),false()) -> F()
  eqt(a(),lock()) -> F()
  eqt(a(),locker()) -> F()
  eqt(a(),mcrlrecord()) -> F()
  eqt(a(),ok()) -> F()
  eqt(a(),pending()) -> F()
  eqt(a(),release()) -> F()
  eqt(a(),request()) -> F()
  eqt(a(),resource()) -> F()
  eqt(a(),tag()) -> F()
  eqt(a(),true()) -> F()
  eqt(a(),undefined()) -> F()
  eqt(a(),pid(N2)) -> F()
  eqt(a(),int(N2)) -> F()
  eqt(a(),cons(H2,T2)) -> F()
  eqt(a(),tuple(H2,T2)) -> F()
  eqt(a(),tuplenil(H2)) -> F()
  eqt(excl(),nil()) -> F()
  eqt(excl(),a()) -> F()
  eqt(excl(),excl()) -> T()
  eqt(excl(),false()) -> F()
  eqt(excl(),lock()) -> F()
  eqt(excl(),locker()) -> F()
  eqt(excl(),mcrlrecord()) -> F()
  eqt(excl(),ok()) -> F()
  eqt(excl(),pending()) -> F()
  eqt(excl(),release()) -> F()
  eqt(excl(),request()) -> F()
  eqt(excl(),resource()) -> F()
  eqt(excl(),tag()) -> F()
  eqt(excl(),true()) -> F()
  eqt(excl(),undefined()) -> F()
  eqt(excl(),pid(N2)) -> F()
  eqt(excl(),eqt(false(),int(N2))) -> F()
  eqt(false(),cons(H2,T2)) -> F()
  eqt(false(),tuple(H2,T2)) -> F()
  eqt(false(),tuplenil(H2)) -> F()
  eqt(lock(),nil()) -> F()
  eqt(lock(),a()) -> F()
  eqt(lock(),excl()) -> F()
  eqt(lock(),false()) -> F()
  eqt(lock(),lock()) -> T()
  eqt(lock(),locker()) -> F()
  eqt(lock(),mcrlrecord()) -> F()
  eqt(lock(),ok()) -> F()
  eqt(lock(),pending()) -> F()
  eqt(lock(),release()) -> F()
  eqt(lock(),request()) -> F()
  eqt(lock(),resource()) -> F()
  eqt(lock(),tag()) -> F()
  eqt(lock(),true()) -> F()
  eqt(lock(),undefined()) -> F()
  eqt(lock(),pid(N2)) -> F()
  eqt(lock(),int(N2)) -> F()
  eqt(lock(),cons(H2,T2)) -> F()
  eqt(lock(),tuple(H2,T2)) -> F()
  eqt(lock(),tuplenil(H2)) -> F()
  eqt(locker(),nil()) -> F()
  eqt(locker(),a()) -> F()
  eqt(locker(),excl()) -> F()
  eqt(locker(),false()) -> F()
  eqt(locker(),lock()) -> F()
  eqt(locker(),locker()) -> T()
  eqt(locker(),mcrlrecord()) -> F()
  eqt(locker(),ok()) -> F()
  eqt(locker(),pending()) -> F()
  eqt(locker(),release()) -> F()
  eqt(locker(),request()) -> F()
  eqt(locker(),resource()) -> F()
  eqt(locker(),tag()) -> F()
  eqt(locker(),true()) -> F()
  eqt(locker(),undefined()) -> F()
  eqt(locker(),pid(N2)) -> F()
  eqt(locker(),int(N2)) -> F()
  eqt(locker(),cons(H2,T2)) -> F()
  eqt(locker(),tuple(H2,T2)) -> F()
  eqt(locker(),tuplenil(H2)) -> F()
  eqt(mcrlrecord(),nil()) -> F()
  eqt(mcrlrecord(),a()) -> F()
  eqt(mcrlrecord(),excl()) -> F()
  eqt(mcrlrecord(),false()) -> F()
  eqt(mcrlrecord(),lock()) -> F()
  eqt(mcrlrecord(),locker()) -> F()
  eqt(mcrlrecord(),mcrlrecord()) -> T()
  eqt(mcrlrecord(),ok()) -> F()
  eqt(mcrlrecord(),pending()) -> F()
  eqt(mcrlrecord(),release()) -> F()
  eqt(mcrlrecord(),request()) -> F()
  eqt(mcrlrecord(),resource()) -> F()
  eqt(ok(),resource()) -> F()
  eqt(ok(),tag()) -> F()
  eqt(ok(),true()) -> F()
  eqt(ok(),undefined()) -> F()
  eqt(ok(),pid(N2)) -> F()
  eqt(ok(),int(N2)) -> F()
  eqt(ok(),cons(H2,T2)) -> F()
  eqt(ok(),tuple(H2,T2)) -> F()
  eqt(ok(),tuplenil(H2)) -> F()
  eqt(pending(),nil()) -> F()
  eqt(pending(),a()) -> F()
  eqt(pending(),excl()) -> F()
  eqt(pending(),false()) -> F()
  eqt(pending(),lock()) -> F()
  eqt(pending(),locker()) -> F()
  eqt(pending(),mcrlrecord()) -> F()
  eqt(pending(),ok()) -> F()
  eqt(pending(),pending()) -> T()
  eqt(pending(),release()) -> F()
  eqt(pending(),request()) -> F()
  eqt(pending(),resource()) -> F()
  eqt(pending(),tag()) -> F()
  eqt(pending(),true()) -> F()
  eqt(pending(),undefined()) -> F()
  eqt(pending(),pid(N2)) -> F()
  eqt(pending(),int(N2)) -> F()
  eqt(pending(),cons(H2,T2)) -> F()
  eqt(pending(),tuple(H2,T2)) -> F()
  eqt(pending(),tuplenil(H2)) -> F()
  eqt(release(),nil()) -> F()
  eqt(release(),a()) -> F()
  eqt(release(),excl()) -> F()
  eqt(release(),false()) -> F()
  eqt(release(),lock()) -> F()
  eqt(release(),locker()) -> F()
  eqt(release(),mcrlrecord()) -> F()
  eqt(release(),ok()) -> F()
  eqt(request(),mcrlrecord()) -> F()
  eqt(request(),ok()) -> F()
  eqt(request(),pending()) -> F()
  eqt(request(),release()) -> F()
  eqt(request(),request()) -> T()
  eqt(request(),resource()) -> F()
  eqt(request(),tag()) -> F()
  eqt(request(),true()) -> F()
  eqt(request(),undefined()) -> F()
  eqt(request(),pid(N2)) -> F()
  eqt(request(),int(N2)) -> F()
  eqt(request(),cons(H2,T2)) -> F()
  eqt(request(),tuple(H2,T2)) -> F()
  eqt(request(),tuplenil(H2)) -> F()
  eqt(resource(),nil()) -> F()
  eqt(resource(),a()) -> F()
  eqt(resource(),excl()) -> F()
  eqt(resource(),false()) -> F()
  eqt(resource(),lock()) -> F()
  eqt(resource(),locker()) -> F()
  eqt(resource(),mcrlrecord()) -> F()
  eqt(resource(),ok()) -> F()
  eqt(resource(),pending()) -> F()
  eqt(resource(),release()) -> F()
  eqt(resource(),request()) -> F()
  eqt(resource(),resource()) -> T()
  eqt(resource(),tag()) -> F()
  eqt(resource(),true()) -> F()
  eqt(resource(),undefined()) -> F()
  eqt(resource(),pid(N2)) -> F()
  eqt(resource(),int(N2)) -> F()
  eqt(resource(),cons(H2,T2)) -> F()
  eqt(resource(),tuple(H2,T2)) -> F()
  eqt(resource(),tuplenil(H2)) -> F()
  eqt(tag(),nil()) -> F()
  eqt(tag(),a()) -> F()
  eqt(tag(),excl()) -> F()
  eqt(tag(),false()) -> F()
  eqt(tag(),lock()) -> F()
  eqt(tag(),locker()) -> F()
  eqt(tag(),mcrlrecord()) -> F()
  eqt(tag(),ok()) -> F()
  eqt(tag(),pending()) -> F()
  eqt(tag(),release()) -> F()
  eqt(tag(),request()) -> F()
  eqt(tag(),resource()) -> F()
  eqt(tag(),tag()) -> T()
  eqt(tag(),true()) -> F()
  eqt(tag(),undefined()) -> F()
  eqt(tag(),pid(N2)) -> F()
  eqt(tag(),int(N2)) -> F()
  eqt(tag(),cons(H2,T2)) -> F()
  eqt(tag(),tuple(H2,T2)) -> F()
  eqt(tag(),tuplenil(H2)) -> F()
  eqt(true(),nil()) -> F()
  eqt(true(),a()) -> F()
  eqt(true(),excl()) -> F()
  eqt(true(),false()) -> F()
  eqt(true(),lock()) -> F()
  eqt(true(),locker()) -> F()
  eqt(true(),mcrlrecord()) -> F()
  eqt(true(),ok()) -> F()
  eqt(true(),pending()) -> F()
  eqt(true(),release()) -> F()
  eqt(true(),request()) -> F()
  eqt(true(),resource()) -> F()
  eqt(true(),tag()) -> F()
  eqt(true(),true()) -> T()
  eqt(true(),undefined()) -> F()
  eqt(true(),pid(N2)) -> F()
  eqt(true(),int(N2)) -> F()
  eqt(true(),cons(H2,T2)) -> F()
  eqt(true(),tuple(H2,T2)) -> F()
  eqt(true(),tuplenil(H2)) -> F()
  eqt(undefined(),nil()) -> F()
  eqt(undefined(),a()) -> F()
  eqt(undefined(),tuplenil(H2)) -> F()
  eqt(pid(N1),nil()) -> F()
  eqt(pid(N1),a()) -> F()
  eqt(pid(N1),excl()) -> F()
  eqt(pid(N1),false()) -> F()
  eqt(pid(N1),lock()) -> F()
  eqt(pid(N1),locker()) -> F()
  eqt(pid(N1),mcrlrecord()) -> F()
  eqt(pid(N1),ok()) -> F()
  eqt(pid(N1),pending()) -> F()
  eqt(pid(N1),release()) -> F()
  eqt(pid(N1),request()) -> F()
  eqt(pid(N1),resource()) -> F()
  eqt(pid(N1),tag()) -> F()
  eqt(pid(N1),true()) -> F()
  eqt(pid(N1),undefined()) -> F()
  eqt(pid(N1),pid(N2)) -> eqt(N1,N2)
  eqt(pid(N1),int(N2)) -> F()
  eqt(pid(N1),cons(H2,T2)) -> F()
  eqt(pid(N1),tuple(H2,T2)) -> F()
  eqt(pid(N1),tuplenil(H2)) -> F()
  eqt(int(N1),nil()) -> F()
  eqt(int(N1),a()) -> F()
  eqt(int(N1),excl()) -> F()
  eqt(int(N1),false()) -> F()
  eqt(int(N1),lock()) -> F()
  eqt(int(N1),locker()) -> F()
  eqt(int(N1),mcrlrecord()) -> F()
  eqt(int(N1),ok()) -> F()
  eqt(int(N1),pending()) -> F()
  eqt(int(N1),release()) -> F()
  eqt(int(N1),request()) -> F()
  eqt(int(N1),resource()) -> F()
  eqt(int(N1),tag()) -> F()
  eqt(int(N1),true()) -> F()
  eqt(int(N1),undefined()) -> F()
  eqt(cons(H1,T1),resource()) -> F()
  eqt(cons(H1,T1),tag()) -> F()
  eqt(cons(H1,T1),true()) -> F()
  eqt(cons(H1,T1),undefined()) -> F()
  eqt(cons(H1,T1),pid(N2)) -> F()
  eqt(cons(H1,T1),int(N2)) -> F()
  eqt(cons(H1,T1),cons(H2,T2)) -> and(eqt(H1,H2),eqt(T1,T2))
  eqt(cons(H1,T1),tuple(H2,T2)) -> F()
  eqt(cons(H1,T1),tuplenil(H2)) -> F()
  eqt(tuple(H1,T1),nil()) -> F()
  eqt(tuple(H1,T1),a()) -> F()
  eqt(tuple(H1,T1),excl()) -> F()
  eqt(tuple(H1,T1),false()) -> F()
  eqt(tuple(H1,T1),lock()) -> F()
  eqt(tuple(H1,T1),locker()) -> F()
  eqt(tuple(H1,T1),mcrlrecord()) -> F()
  eqt(tuple(H1,T1),ok()) -> F()
  eqt(tuple(H1,T1),pending()) -> F()
  eqt(tuple(H1,T1),release()) -> F()
  eqt(tuple(H1,T1),request()) -> F()
  eqt(tuple(H1,T1),resource()) -> F()
  eqt(tuple(H1,T1),tag()) -> F()
  eqt(tuple(H1,T1),true()) -> F()
  eqt(tuple(H1,T1),undefined()) -> F()
  eqt(tuple(H1,T1),pid(N2)) -> F()
  eqt(tuple(H1,T1),int(N2)) -> F()
  eqt(tuple(H1,T1),cons(H2,T2)) -> F()
  eqt(tuple(H1,T1),tuple(H2,T2)) -> and(eqt(H1,H2),eqt(T1,T2))
  eqt(tuple(H1,T1),tuplenil(H2)) -> F()
  eqt(tuplenil(H1),nil()) -> F()
  eqt(tuplenil(H1),a()) -> F()
  eqt(tuplenil(H1),excl()) -> F()
  eqt(tuplenil(H1),false()) -> F()
  eqt(tuplenil(H1),lock()) -> F()
  eqt(tuplenil(H1),locker()) -> F()
  eqt(tuplenil(H1),mcrlrecord()) -> F()
  eqt(tuplenil(H1),ok()) -> F()
  eqt(tuplenil(H1),pending()) -> F()
  eqt(tuplenil(H1),release()) -> F()
  eqt(tuplenil(H1),request()) -> F()
  eqt(tuplenil(H1),resource()) -> F()
  eqt(tuplenil(H1),tag()) -> F()
  eqt(tuplenil(H1),true()) -> F()
  eqt(tuplenil(H1),undefined()) -> F()
  eqt(tuplenil(H1),pid(N2)) -> F()
  eqt(tuplenil(H1),int(N2)) -> F()
  eqt(tuplenil(H1),cons(H2,T2)) -> F()
  eqt(tuplenil(H1),tuple(H2,T2)) -> F()
  eqt(tuplenil(H1),tuplenil(H2)) -> eqt(H1,H2)
  element(int(s(|0|())),tuplenil(T1)) -> T1
  element(int(s(|0|())),tuple(T1,T2)) -> T1
  element(int(s(s(N1))),tuple(T1,T2)) -> element(int(s(N1)),T2)
  record_new(lock()) -> tuple(mcrlrecord(),tuple(lock(),tuple(undefined(),tuple(nil(),tuplenil(nil())))))
  record_extract(tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(F2))))),lock(),resource()) -> tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(F2)))))
  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)))))
  record_updates(Record,Name,nil()) -> Record
  record_updates(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields)) -> record_updates(record_update(Record,Name,Field,NewF),Name,Fields)
  locker2_map_promote_pending(nil(),Pending) -> nil()
  locker2_map_promote_pending(cons(Lock,Locks),Pending) -> cons(locker2_promote_pending(Lock,Pending),locker2_map_promote_pending(Locks,Pending))
  locker2_map_claim_lock(nil(),Resources,Client) -> nil()
  locker2_map_claim_lock(cons(Lock,Locks),Resources,Client) -> cons(locker2_claim_lock(Lock,Resources,Client),locker2_map_claim_lock(Locks,Resources,Client))
  locker2_map_add_pending(nil(),Resources,Client) -> nil()
  locker2_promote_pending(Lock,Client) -> case0(Client,Lock,record_extract(Lock,lock(),pending()))
  case0(Client,Lock,cons(Client,Pendings)) -> record_updates(Lock,lock(),cons(tuple(excl(),tuplenil(Client)),cons(tuple(pending(),tuplenil(Pendings)),nil())))
  case0(Client,Lock,MCRLFree0) -> Lock
  locker2_remove_pending(Lock,Client) -> record_updates(Lock,lock(),cons(tuple(pending(),tuplenil(subtract(record_extract(Lock,lock(),pending()),cons(Client,nil())))),nil()))
  locker2_add_pending(Lock,Resources,Client) -> case1(Client,Resources,Lock,member(record_extract(Lock,lock(),resource()),Resources))
  case1(Client,Resources,Lock,true()) -> record_updates(Lock,lock(),cons(tuple(pending(),tuplenil(append(record_extract(Lock,lock(),pending()),cons(Client,nil())))),nil()))
  case1(Client,Resources,Lock,false()) -> Lock
  locker2_release_lock(Lock,Client) -> case2(Client,Lock,gen_modtageq(Client,record_extract(Lock,lock(),excl())))
  case2(Client,Lock,true()) -> record_updates(Lock,lock(),cons(tuple(excllock(),excl()),nil()))
  case4(Client,Lock,MCRLFree1) -> false()
  locker2_obtainables(nil(),Client) -> true()
  locker2_obtainables(cons(Lock,Locks),Client) -> case5(Client,Locks,Lock,member(Client,record_extract(Lock,lock(),pending())))
  case5(Client,Locks,Lock,true()) -> andt(locker2_obtainable(Lock,Client),locker2_obtainables(Locks,Client))
  case5(Client,Locks,Lock,false()) -> locker2_obtainables(Locks,Client)
  locker2_check_available(Resource,nil()) -> false()
  locker2_check_available(Resource,cons(Lock,Locks)) -> case6(Locks,Lock,Resource,equal(Resource,record_extract(Lock,lock(),resource())))
  case6(Locks,Lock,Resource,true()) -> andt(equal(record_extract(Lock,lock(),excl()),nil()),equal(record_extract(Lock,lock(),pending()),nil()))
  case6(Locks,Lock,Resource,false()) -> locker2_check_available(Resource,Locks)
  locker2_check_availables(nil(),Locks) -> true()
  locker2_check_availables(cons(Resource,Resources),Locks) -> andt(locker2_check_available(Resource,Locks),locker2_check_availables(Resources,Locks))
  locker2_adduniq(nil(),List) -> List
  append(cons(Head,Tail),List) -> cons(Head,append(Tail,List))
  subtract(List,nil()) -> List
  subtract(List,cons(Head,Tail)) -> subtract(delete(Head,List),Tail)
  delete(E,nil()) -> nil()
  delete(E,cons(Head,Tail)) -> case8(Tail,Head,E,equal(E,Head))
  case8(Tail,Head,E,true()) -> Tail
  case8(Tail,Head,E,false()) -> cons(Head,delete(E,Tail))
  gen_tag(Pid) -> tuple(Pid,tuplenil(tag()))
  gen_modtageq(Client1,Client2) -> equal(Client1,Client2)
  member(E,nil()) -> false()
  member(E,cons(Head,Tail)) -> case9(Tail,Head,E,equal(E,Head))
  case9(Tail,Head,E,true()) -> true()
  case9(Tail,Head,E,false()) -> member(E,Tail)
  eqs(empty(),empty()) -> T()
  eqs(empty(),stack(E2,S2)) -> F()
  eqs(stack(E1,S1),empty()) -> F()
  eqs(stack(E1,S1),stack(E2,S2)) -> and(eqt(E1,E2),eqs(S1,S2))
  pushs(E1,S1) -> stack(E1,S1)
  pops(stack(E1,S1)) -> S1
  tops(stack(E1,S1)) -> E1
  istops(E1,empty()) -> F()
  istops(E1,stack(E2,S1)) -> eqt(E1,E2)
  eqc(nocalls(),nocalls()) -> T()
  eqc(nocalls(),calls(E2,S2,CS2)) -> F()
  eqc(calls(E1,S1,CS1),nocalls()) -> F()
  eqc(calls(E1,S1,CS1),calls(E2,S2,CS2)) -> and(eqt(E1,E2),and(eqs(S1,S2),eqc(CS1,CS2)))
  push(E1,E2,nocalls()) -> calls(E1,stack(E2,empty()),nocalls())
  push(E1,E2,calls(E3,S1,CS1)) -> push1(E1,E2,E3,S1,CS1,eqt(E1,E3))
  push1(E1,E2,E3,S1,CS1,T()) -> calls(E3,pushs(E2,S1),CS1)

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: eqt#(pid(N1),pid(N2)) -> eqt#(N1,N2)
p2: eqt#(cons(H1,T1),cons(H2,T2)) -> and#(eqt(H1,H2),eqt(T1,T2))
p3: eqt#(cons(H1,T1),cons(H2,T2)) -> eqt#(H1,H2)
p4: eqt#(cons(H1,T1),cons(H2,T2)) -> eqt#(T1,T2)
p5: eqt#(tuple(H1,T1),tuple(H2,T2)) -> and#(eqt(H1,H2),eqt(T1,T2))
p6: eqt#(tuple(H1,T1),tuple(H2,T2)) -> eqt#(H1,H2)
p7: eqt#(tuple(H1,T1),tuple(H2,T2)) -> eqt#(T1,T2)
p8: eqt#(tuplenil(H1),tuplenil(H2)) -> eqt#(H1,H2)
p9: element#(int(s(s(N1))),tuple(T1,T2)) -> element#(int(s(N1)),T2)
p10: record_updates#(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields)) -> record_updates#(record_update(Record,Name,Field,NewF),Name,Fields)
p11: record_updates#(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields)) -> record_update#(Record,Name,Field,NewF)
p12: locker2_map_promote_pending#(cons(Lock,Locks),Pending) -> locker2_promote_pending#(Lock,Pending)
p13: locker2_map_promote_pending#(cons(Lock,Locks),Pending) -> locker2_map_promote_pending#(Locks,Pending)
p14: locker2_map_claim_lock#(cons(Lock,Locks),Resources,Client) -> locker2_map_claim_lock#(Locks,Resources,Client)
p15: locker2_promote_pending#(Lock,Client) -> case0#(Client,Lock,record_extract(Lock,lock(),pending()))
p16: locker2_promote_pending#(Lock,Client) -> record_extract#(Lock,lock(),pending())
p17: case0#(Client,Lock,cons(Client,Pendings)) -> record_updates#(Lock,lock(),cons(tuple(excl(),tuplenil(Client)),cons(tuple(pending(),tuplenil(Pendings)),nil())))
p18: locker2_remove_pending#(Lock,Client) -> record_updates#(Lock,lock(),cons(tuple(pending(),tuplenil(subtract(record_extract(Lock,lock(),pending()),cons(Client,nil())))),nil()))
p19: locker2_remove_pending#(Lock,Client) -> subtract#(record_extract(Lock,lock(),pending()),cons(Client,nil()))
p20: locker2_remove_pending#(Lock,Client) -> record_extract#(Lock,lock(),pending())
p21: locker2_add_pending#(Lock,Resources,Client) -> case1#(Client,Resources,Lock,member(record_extract(Lock,lock(),resource()),Resources))
p22: locker2_add_pending#(Lock,Resources,Client) -> member#(record_extract(Lock,lock(),resource()),Resources)
p23: locker2_add_pending#(Lock,Resources,Client) -> record_extract#(Lock,lock(),resource())
p24: case1#(Client,Resources,Lock,true()) -> record_updates#(Lock,lock(),cons(tuple(pending(),tuplenil(append(record_extract(Lock,lock(),pending()),cons(Client,nil())))),nil()))
p25: case1#(Client,Resources,Lock,true()) -> append#(record_extract(Lock,lock(),pending()),cons(Client,nil()))
p26: case1#(Client,Resources,Lock,true()) -> record_extract#(Lock,lock(),pending())
p27: locker2_release_lock#(Lock,Client) -> case2#(Client,Lock,gen_modtageq(Client,record_extract(Lock,lock(),excl())))
p28: locker2_release_lock#(Lock,Client) -> gen_modtageq#(Client,record_extract(Lock,lock(),excl()))
p29: locker2_release_lock#(Lock,Client) -> record_extract#(Lock,lock(),excl())
p30: case2#(Client,Lock,true()) -> record_updates#(Lock,lock(),cons(tuple(excllock(),excl()),nil()))
p31: locker2_obtainables#(cons(Lock,Locks),Client) -> case5#(Client,Locks,Lock,member(Client,record_extract(Lock,lock(),pending())))
p32: locker2_obtainables#(cons(Lock,Locks),Client) -> member#(Client,record_extract(Lock,lock(),pending()))
p33: locker2_obtainables#(cons(Lock,Locks),Client) -> record_extract#(Lock,lock(),pending())
p34: case5#(Client,Locks,Lock,true()) -> locker2_obtainables#(Locks,Client)
p35: case5#(Client,Locks,Lock,false()) -> locker2_obtainables#(Locks,Client)
p36: locker2_check_available#(Resource,cons(Lock,Locks)) -> case6#(Locks,Lock,Resource,equal(Resource,record_extract(Lock,lock(),resource())))
p37: locker2_check_available#(Resource,cons(Lock,Locks)) -> record_extract#(Lock,lock(),resource())
p38: case6#(Locks,Lock,Resource,true()) -> record_extract#(Lock,lock(),excl())
p39: case6#(Locks,Lock,Resource,true()) -> record_extract#(Lock,lock(),pending())
p40: case6#(Locks,Lock,Resource,false()) -> locker2_check_available#(Resource,Locks)
p41: locker2_check_availables#(cons(Resource,Resources),Locks) -> locker2_check_available#(Resource,Locks)
p42: locker2_check_availables#(cons(Resource,Resources),Locks) -> locker2_check_availables#(Resources,Locks)
p43: append#(cons(Head,Tail),List) -> append#(Tail,List)
p44: subtract#(List,cons(Head,Tail)) -> subtract#(delete(Head,List),Tail)
p45: subtract#(List,cons(Head,Tail)) -> delete#(Head,List)
p46: delete#(E,cons(Head,Tail)) -> case8#(Tail,Head,E,equal(E,Head))
p47: case8#(Tail,Head,E,false()) -> delete#(E,Tail)
p48: member#(E,cons(Head,Tail)) -> case9#(Tail,Head,E,equal(E,Head))
p49: case9#(Tail,Head,E,false()) -> member#(E,Tail)
p50: eqs#(stack(E1,S1),stack(E2,S2)) -> and#(eqt(E1,E2),eqs(S1,S2))
p51: eqs#(stack(E1,S1),stack(E2,S2)) -> eqt#(E1,E2)
p52: eqs#(stack(E1,S1),stack(E2,S2)) -> eqs#(S1,S2)
p53: istops#(E1,stack(E2,S1)) -> eqt#(E1,E2)
p54: eqc#(calls(E1,S1,CS1),calls(E2,S2,CS2)) -> and#(eqt(E1,E2),and(eqs(S1,S2),eqc(CS1,CS2)))
p55: eqc#(calls(E1,S1,CS1),calls(E2,S2,CS2)) -> eqt#(E1,E2)
p56: eqc#(calls(E1,S1,CS1),calls(E2,S2,CS2)) -> and#(eqs(S1,S2),eqc(CS1,CS2))
p57: eqc#(calls(E1,S1,CS1),calls(E2,S2,CS2)) -> eqs#(S1,S2)
p58: eqc#(calls(E1,S1,CS1),calls(E2,S2,CS2)) -> eqc#(CS1,CS2)
p59: push#(E1,E2,calls(E3,S1,CS1)) -> push1#(E1,E2,E3,S1,CS1,eqt(E1,E3))
p60: push#(E1,E2,calls(E3,S1,CS1)) -> eqt#(E1,E3)
p61: push1#(E1,E2,E3,S1,CS1,T()) -> pushs#(E2,S1)

and R consists of:

r1: or(T(),T()) -> T()
r2: or(F(),T()) -> T()
r3: or(T(),F()) -> T()
r4: or(F(),F()) -> F()
r5: and(T(),B) -> B
r6: and(B,T()) -> B
r7: and(F(),B) -> F()
r8: and(B,F()) -> F()
r9: imp(T(),B) -> B
r10: imp(F(),B) -> T()
r11: not(T()) -> F()
r12: not(F()) -> T()
r13: if(T(),B1,B2) -> B1
r14: if(F(),B1,B2) -> B2
r15: eq(T(),T()) -> T()
r16: eq(F(),F()) -> T()
r17: eq(T(),F()) -> F()
r18: eq(F(),T()) -> F()
r19: eqt(nil(),undefined()) -> F()
r20: eqt(nil(),pid(N2)) -> F()
r21: eqt(nil(),int(N2)) -> F()
r22: eqt(nil(),cons(H2,T2)) -> F()
r23: eqt(nil(),tuple(H2,T2)) -> F()
r24: eqt(nil(),tuplenil(H2)) -> F()
r25: eqt(a(),nil()) -> F()
r26: eqt(a(),a()) -> T()
r27: eqt(a(),excl()) -> F()
r28: eqt(a(),false()) -> F()
r29: eqt(a(),lock()) -> F()
r30: eqt(a(),locker()) -> F()
r31: eqt(a(),mcrlrecord()) -> F()
r32: eqt(a(),ok()) -> F()
r33: eqt(a(),pending()) -> F()
r34: eqt(a(),release()) -> F()
r35: eqt(a(),request()) -> F()
r36: eqt(a(),resource()) -> F()
r37: eqt(a(),tag()) -> F()
r38: eqt(a(),true()) -> F()
r39: eqt(a(),undefined()) -> F()
r40: eqt(a(),pid(N2)) -> F()
r41: eqt(a(),int(N2)) -> F()
r42: eqt(a(),cons(H2,T2)) -> F()
r43: eqt(a(),tuple(H2,T2)) -> F()
r44: eqt(a(),tuplenil(H2)) -> F()
r45: eqt(excl(),nil()) -> F()
r46: eqt(excl(),a()) -> F()
r47: eqt(excl(),excl()) -> T()
r48: eqt(excl(),false()) -> F()
r49: eqt(excl(),lock()) -> F()
r50: eqt(excl(),locker()) -> F()
r51: eqt(excl(),mcrlrecord()) -> F()
r52: eqt(excl(),ok()) -> F()
r53: eqt(excl(),pending()) -> F()
r54: eqt(excl(),release()) -> F()
r55: eqt(excl(),request()) -> F()
r56: eqt(excl(),resource()) -> F()
r57: eqt(excl(),tag()) -> F()
r58: eqt(excl(),true()) -> F()
r59: eqt(excl(),undefined()) -> F()
r60: eqt(excl(),pid(N2)) -> F()
r61: eqt(excl(),eqt(false(),int(N2))) -> F()
r62: eqt(false(),cons(H2,T2)) -> F()
r63: eqt(false(),tuple(H2,T2)) -> F()
r64: eqt(false(),tuplenil(H2)) -> F()
r65: eqt(lock(),nil()) -> F()
r66: eqt(lock(),a()) -> F()
r67: eqt(lock(),excl()) -> F()
r68: eqt(lock(),false()) -> F()
r69: eqt(lock(),lock()) -> T()
r70: eqt(lock(),locker()) -> F()
r71: eqt(lock(),mcrlrecord()) -> F()
r72: eqt(lock(),ok()) -> F()
r73: eqt(lock(),pending()) -> F()
r74: eqt(lock(),release()) -> F()
r75: eqt(lock(),request()) -> F()
r76: eqt(lock(),resource()) -> F()
r77: eqt(lock(),tag()) -> F()
r78: eqt(lock(),true()) -> F()
r79: eqt(lock(),undefined()) -> F()
r80: eqt(lock(),pid(N2)) -> F()
r81: eqt(lock(),int(N2)) -> F()
r82: eqt(lock(),cons(H2,T2)) -> F()
r83: eqt(lock(),tuple(H2,T2)) -> F()
r84: eqt(lock(),tuplenil(H2)) -> F()
r85: eqt(locker(),nil()) -> F()
r86: eqt(locker(),a()) -> F()
r87: eqt(locker(),excl()) -> F()
r88: eqt(locker(),false()) -> F()
r89: eqt(locker(),lock()) -> F()
r90: eqt(locker(),locker()) -> T()
r91: eqt(locker(),mcrlrecord()) -> F()
r92: eqt(locker(),ok()) -> F()
r93: eqt(locker(),pending()) -> F()
r94: eqt(locker(),release()) -> F()
r95: eqt(locker(),request()) -> F()
r96: eqt(locker(),resource()) -> F()
r97: eqt(locker(),tag()) -> F()
r98: eqt(locker(),true()) -> F()
r99: eqt(locker(),undefined()) -> F()
r100: eqt(locker(),pid(N2)) -> F()
r101: eqt(locker(),int(N2)) -> F()
r102: eqt(locker(),cons(H2,T2)) -> F()
r103: eqt(locker(),tuple(H2,T2)) -> F()
r104: eqt(locker(),tuplenil(H2)) -> F()
r105: eqt(mcrlrecord(),nil()) -> F()
r106: eqt(mcrlrecord(),a()) -> F()
r107: eqt(mcrlrecord(),excl()) -> F()
r108: eqt(mcrlrecord(),false()) -> F()
r109: eqt(mcrlrecord(),lock()) -> F()
r110: eqt(mcrlrecord(),locker()) -> F()
r111: eqt(mcrlrecord(),mcrlrecord()) -> T()
r112: eqt(mcrlrecord(),ok()) -> F()
r113: eqt(mcrlrecord(),pending()) -> F()
r114: eqt(mcrlrecord(),release()) -> F()
r115: eqt(mcrlrecord(),request()) -> F()
r116: eqt(mcrlrecord(),resource()) -> F()
r117: eqt(ok(),resource()) -> F()
r118: eqt(ok(),tag()) -> F()
r119: eqt(ok(),true()) -> F()
r120: eqt(ok(),undefined()) -> F()
r121: eqt(ok(),pid(N2)) -> F()
r122: eqt(ok(),int(N2)) -> F()
r123: eqt(ok(),cons(H2,T2)) -> F()
r124: eqt(ok(),tuple(H2,T2)) -> F()
r125: eqt(ok(),tuplenil(H2)) -> F()
r126: eqt(pending(),nil()) -> F()
r127: eqt(pending(),a()) -> F()
r128: eqt(pending(),excl()) -> F()
r129: eqt(pending(),false()) -> F()
r130: eqt(pending(),lock()) -> F()
r131: eqt(pending(),locker()) -> F()
r132: eqt(pending(),mcrlrecord()) -> F()
r133: eqt(pending(),ok()) -> F()
r134: eqt(pending(),pending()) -> T()
r135: eqt(pending(),release()) -> F()
r136: eqt(pending(),request()) -> F()
r137: eqt(pending(),resource()) -> F()
r138: eqt(pending(),tag()) -> F()
r139: eqt(pending(),true()) -> F()
r140: eqt(pending(),undefined()) -> F()
r141: eqt(pending(),pid(N2)) -> F()
r142: eqt(pending(),int(N2)) -> F()
r143: eqt(pending(),cons(H2,T2)) -> F()
r144: eqt(pending(),tuple(H2,T2)) -> F()
r145: eqt(pending(),tuplenil(H2)) -> F()
r146: eqt(release(),nil()) -> F()
r147: eqt(release(),a()) -> F()
r148: eqt(release(),excl()) -> F()
r149: eqt(release(),false()) -> F()
r150: eqt(release(),lock()) -> F()
r151: eqt(release(),locker()) -> F()
r152: eqt(release(),mcrlrecord()) -> F()
r153: eqt(release(),ok()) -> F()
r154: eqt(request(),mcrlrecord()) -> F()
r155: eqt(request(),ok()) -> F()
r156: eqt(request(),pending()) -> F()
r157: eqt(request(),release()) -> F()
r158: eqt(request(),request()) -> T()
r159: eqt(request(),resource()) -> F()
r160: eqt(request(),tag()) -> F()
r161: eqt(request(),true()) -> F()
r162: eqt(request(),undefined()) -> F()
r163: eqt(request(),pid(N2)) -> F()
r164: eqt(request(),int(N2)) -> F()
r165: eqt(request(),cons(H2,T2)) -> F()
r166: eqt(request(),tuple(H2,T2)) -> F()
r167: eqt(request(),tuplenil(H2)) -> F()
r168: eqt(resource(),nil()) -> F()
r169: eqt(resource(),a()) -> F()
r170: eqt(resource(),excl()) -> F()
r171: eqt(resource(),false()) -> F()
r172: eqt(resource(),lock()) -> F()
r173: eqt(resource(),locker()) -> F()
r174: eqt(resource(),mcrlrecord()) -> F()
r175: eqt(resource(),ok()) -> F()
r176: eqt(resource(),pending()) -> F()
r177: eqt(resource(),release()) -> F()
r178: eqt(resource(),request()) -> F()
r179: eqt(resource(),resource()) -> T()
r180: eqt(resource(),tag()) -> F()
r181: eqt(resource(),true()) -> F()
r182: eqt(resource(),undefined()) -> F()
r183: eqt(resource(),pid(N2)) -> F()
r184: eqt(resource(),int(N2)) -> F()
r185: eqt(resource(),cons(H2,T2)) -> F()
r186: eqt(resource(),tuple(H2,T2)) -> F()
r187: eqt(resource(),tuplenil(H2)) -> F()
r188: eqt(tag(),nil()) -> F()
r189: eqt(tag(),a()) -> F()
r190: eqt(tag(),excl()) -> F()
r191: eqt(tag(),false()) -> F()
r192: eqt(tag(),lock()) -> F()
r193: eqt(tag(),locker()) -> F()
r194: eqt(tag(),mcrlrecord()) -> F()
r195: eqt(tag(),ok()) -> F()
r196: eqt(tag(),pending()) -> F()
r197: eqt(tag(),release()) -> F()
r198: eqt(tag(),request()) -> F()
r199: eqt(tag(),resource()) -> F()
r200: eqt(tag(),tag()) -> T()
r201: eqt(tag(),true()) -> F()
r202: eqt(tag(),undefined()) -> F()
r203: eqt(tag(),pid(N2)) -> F()
r204: eqt(tag(),int(N2)) -> F()
r205: eqt(tag(),cons(H2,T2)) -> F()
r206: eqt(tag(),tuple(H2,T2)) -> F()
r207: eqt(tag(),tuplenil(H2)) -> F()
r208: eqt(true(),nil()) -> F()
r209: eqt(true(),a()) -> F()
r210: eqt(true(),excl()) -> F()
r211: eqt(true(),false()) -> F()
r212: eqt(true(),lock()) -> F()
r213: eqt(true(),locker()) -> F()
r214: eqt(true(),mcrlrecord()) -> F()
r215: eqt(true(),ok()) -> F()
r216: eqt(true(),pending()) -> F()
r217: eqt(true(),release()) -> F()
r218: eqt(true(),request()) -> F()
r219: eqt(true(),resource()) -> F()
r220: eqt(true(),tag()) -> F()
r221: eqt(true(),true()) -> T()
r222: eqt(true(),undefined()) -> F()
r223: eqt(true(),pid(N2)) -> F()
r224: eqt(true(),int(N2)) -> F()
r225: eqt(true(),cons(H2,T2)) -> F()
r226: eqt(true(),tuple(H2,T2)) -> F()
r227: eqt(true(),tuplenil(H2)) -> F()
r228: eqt(undefined(),nil()) -> F()
r229: eqt(undefined(),a()) -> F()
r230: eqt(undefined(),tuplenil(H2)) -> F()
r231: eqt(pid(N1),nil()) -> F()
r232: eqt(pid(N1),a()) -> F()
r233: eqt(pid(N1),excl()) -> F()
r234: eqt(pid(N1),false()) -> F()
r235: eqt(pid(N1),lock()) -> F()
r236: eqt(pid(N1),locker()) -> F()
r237: eqt(pid(N1),mcrlrecord()) -> F()
r238: eqt(pid(N1),ok()) -> F()
r239: eqt(pid(N1),pending()) -> F()
r240: eqt(pid(N1),release()) -> F()
r241: eqt(pid(N1),request()) -> F()
r242: eqt(pid(N1),resource()) -> F()
r243: eqt(pid(N1),tag()) -> F()
r244: eqt(pid(N1),true()) -> F()
r245: eqt(pid(N1),undefined()) -> F()
r246: eqt(pid(N1),pid(N2)) -> eqt(N1,N2)
r247: eqt(pid(N1),int(N2)) -> F()
r248: eqt(pid(N1),cons(H2,T2)) -> F()
r249: eqt(pid(N1),tuple(H2,T2)) -> F()
r250: eqt(pid(N1),tuplenil(H2)) -> F()
r251: eqt(int(N1),nil()) -> F()
r252: eqt(int(N1),a()) -> F()
r253: eqt(int(N1),excl()) -> F()
r254: eqt(int(N1),false()) -> F()
r255: eqt(int(N1),lock()) -> F()
r256: eqt(int(N1),locker()) -> F()
r257: eqt(int(N1),mcrlrecord()) -> F()
r258: eqt(int(N1),ok()) -> F()
r259: eqt(int(N1),pending()) -> F()
r260: eqt(int(N1),release()) -> F()
r261: eqt(int(N1),request()) -> F()
r262: eqt(int(N1),resource()) -> F()
r263: eqt(int(N1),tag()) -> F()
r264: eqt(int(N1),true()) -> F()
r265: eqt(int(N1),undefined()) -> F()
r266: eqt(cons(H1,T1),resource()) -> F()
r267: eqt(cons(H1,T1),tag()) -> F()
r268: eqt(cons(H1,T1),true()) -> F()
r269: eqt(cons(H1,T1),undefined()) -> F()
r270: eqt(cons(H1,T1),pid(N2)) -> F()
r271: eqt(cons(H1,T1),int(N2)) -> F()
r272: eqt(cons(H1,T1),cons(H2,T2)) -> and(eqt(H1,H2),eqt(T1,T2))
r273: eqt(cons(H1,T1),tuple(H2,T2)) -> F()
r274: eqt(cons(H1,T1),tuplenil(H2)) -> F()
r275: eqt(tuple(H1,T1),nil()) -> F()
r276: eqt(tuple(H1,T1),a()) -> F()
r277: eqt(tuple(H1,T1),excl()) -> F()
r278: eqt(tuple(H1,T1),false()) -> F()
r279: eqt(tuple(H1,T1),lock()) -> F()
r280: eqt(tuple(H1,T1),locker()) -> F()
r281: eqt(tuple(H1,T1),mcrlrecord()) -> F()
r282: eqt(tuple(H1,T1),ok()) -> F()
r283: eqt(tuple(H1,T1),pending()) -> F()
r284: eqt(tuple(H1,T1),release()) -> F()
r285: eqt(tuple(H1,T1),request()) -> F()
r286: eqt(tuple(H1,T1),resource()) -> F()
r287: eqt(tuple(H1,T1),tag()) -> F()
r288: eqt(tuple(H1,T1),true()) -> F()
r289: eqt(tuple(H1,T1),undefined()) -> F()
r290: eqt(tuple(H1,T1),pid(N2)) -> F()
r291: eqt(tuple(H1,T1),int(N2)) -> F()
r292: eqt(tuple(H1,T1),cons(H2,T2)) -> F()
r293: eqt(tuple(H1,T1),tuple(H2,T2)) -> and(eqt(H1,H2),eqt(T1,T2))
r294: eqt(tuple(H1,T1),tuplenil(H2)) -> F()
r295: eqt(tuplenil(H1),nil()) -> F()
r296: eqt(tuplenil(H1),a()) -> F()
r297: eqt(tuplenil(H1),excl()) -> F()
r298: eqt(tuplenil(H1),false()) -> F()
r299: eqt(tuplenil(H1),lock()) -> F()
r300: eqt(tuplenil(H1),locker()) -> F()
r301: eqt(tuplenil(H1),mcrlrecord()) -> F()
r302: eqt(tuplenil(H1),ok()) -> F()
r303: eqt(tuplenil(H1),pending()) -> F()
r304: eqt(tuplenil(H1),release()) -> F()
r305: eqt(tuplenil(H1),request()) -> F()
r306: eqt(tuplenil(H1),resource()) -> F()
r307: eqt(tuplenil(H1),tag()) -> F()
r308: eqt(tuplenil(H1),true()) -> F()
r309: eqt(tuplenil(H1),undefined()) -> F()
r310: eqt(tuplenil(H1),pid(N2)) -> F()
r311: eqt(tuplenil(H1),int(N2)) -> F()
r312: eqt(tuplenil(H1),cons(H2,T2)) -> F()
r313: eqt(tuplenil(H1),tuple(H2,T2)) -> F()
r314: eqt(tuplenil(H1),tuplenil(H2)) -> eqt(H1,H2)
r315: element(int(s(|0|())),tuplenil(T1)) -> T1
r316: element(int(s(|0|())),tuple(T1,T2)) -> T1
r317: element(int(s(s(N1))),tuple(T1,T2)) -> element(int(s(N1)),T2)
r318: record_new(lock()) -> tuple(mcrlrecord(),tuple(lock(),tuple(undefined(),tuple(nil(),tuplenil(nil())))))
r319: record_extract(tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(F2))))),lock(),resource()) -> tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(F2)))))
r320: 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)))))
r321: record_updates(Record,Name,nil()) -> Record
r322: record_updates(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields)) -> record_updates(record_update(Record,Name,Field,NewF),Name,Fields)
r323: locker2_map_promote_pending(nil(),Pending) -> nil()
r324: locker2_map_promote_pending(cons(Lock,Locks),Pending) -> cons(locker2_promote_pending(Lock,Pending),locker2_map_promote_pending(Locks,Pending))
r325: locker2_map_claim_lock(nil(),Resources,Client) -> nil()
r326: locker2_map_claim_lock(cons(Lock,Locks),Resources,Client) -> cons(locker2_claim_lock(Lock,Resources,Client),locker2_map_claim_lock(Locks,Resources,Client))
r327: locker2_map_add_pending(nil(),Resources,Client) -> nil()
r328: locker2_promote_pending(Lock,Client) -> case0(Client,Lock,record_extract(Lock,lock(),pending()))
r329: case0(Client,Lock,cons(Client,Pendings)) -> record_updates(Lock,lock(),cons(tuple(excl(),tuplenil(Client)),cons(tuple(pending(),tuplenil(Pendings)),nil())))
r330: case0(Client,Lock,MCRLFree0) -> Lock
r331: locker2_remove_pending(Lock,Client) -> record_updates(Lock,lock(),cons(tuple(pending(),tuplenil(subtract(record_extract(Lock,lock(),pending()),cons(Client,nil())))),nil()))
r332: locker2_add_pending(Lock,Resources,Client) -> case1(Client,Resources,Lock,member(record_extract(Lock,lock(),resource()),Resources))
r333: case1(Client,Resources,Lock,true()) -> record_updates(Lock,lock(),cons(tuple(pending(),tuplenil(append(record_extract(Lock,lock(),pending()),cons(Client,nil())))),nil()))
r334: case1(Client,Resources,Lock,false()) -> Lock
r335: locker2_release_lock(Lock,Client) -> case2(Client,Lock,gen_modtageq(Client,record_extract(Lock,lock(),excl())))
r336: case2(Client,Lock,true()) -> record_updates(Lock,lock(),cons(tuple(excllock(),excl()),nil()))
r337: case4(Client,Lock,MCRLFree1) -> false()
r338: locker2_obtainables(nil(),Client) -> true()
r339: locker2_obtainables(cons(Lock,Locks),Client) -> case5(Client,Locks,Lock,member(Client,record_extract(Lock,lock(),pending())))
r340: case5(Client,Locks,Lock,true()) -> andt(locker2_obtainable(Lock,Client),locker2_obtainables(Locks,Client))
r341: case5(Client,Locks,Lock,false()) -> locker2_obtainables(Locks,Client)
r342: locker2_check_available(Resource,nil()) -> false()
r343: locker2_check_available(Resource,cons(Lock,Locks)) -> case6(Locks,Lock,Resource,equal(Resource,record_extract(Lock,lock(),resource())))
r344: case6(Locks,Lock,Resource,true()) -> andt(equal(record_extract(Lock,lock(),excl()),nil()),equal(record_extract(Lock,lock(),pending()),nil()))
r345: case6(Locks,Lock,Resource,false()) -> locker2_check_available(Resource,Locks)
r346: locker2_check_availables(nil(),Locks) -> true()
r347: locker2_check_availables(cons(Resource,Resources),Locks) -> andt(locker2_check_available(Resource,Locks),locker2_check_availables(Resources,Locks))
r348: locker2_adduniq(nil(),List) -> List
r349: append(cons(Head,Tail),List) -> cons(Head,append(Tail,List))
r350: subtract(List,nil()) -> List
r351: subtract(List,cons(Head,Tail)) -> subtract(delete(Head,List),Tail)
r352: delete(E,nil()) -> nil()
r353: delete(E,cons(Head,Tail)) -> case8(Tail,Head,E,equal(E,Head))
r354: case8(Tail,Head,E,true()) -> Tail
r355: case8(Tail,Head,E,false()) -> cons(Head,delete(E,Tail))
r356: gen_tag(Pid) -> tuple(Pid,tuplenil(tag()))
r357: gen_modtageq(Client1,Client2) -> equal(Client1,Client2)
r358: member(E,nil()) -> false()
r359: member(E,cons(Head,Tail)) -> case9(Tail,Head,E,equal(E,Head))
r360: case9(Tail,Head,E,true()) -> true()
r361: case9(Tail,Head,E,false()) -> member(E,Tail)
r362: eqs(empty(),empty()) -> T()
r363: eqs(empty(),stack(E2,S2)) -> F()
r364: eqs(stack(E1,S1),empty()) -> F()
r365: eqs(stack(E1,S1),stack(E2,S2)) -> and(eqt(E1,E2),eqs(S1,S2))
r366: pushs(E1,S1) -> stack(E1,S1)
r367: pops(stack(E1,S1)) -> S1
r368: tops(stack(E1,S1)) -> E1
r369: istops(E1,empty()) -> F()
r370: istops(E1,stack(E2,S1)) -> eqt(E1,E2)
r371: eqc(nocalls(),nocalls()) -> T()
r372: eqc(nocalls(),calls(E2,S2,CS2)) -> F()
r373: eqc(calls(E1,S1,CS1),nocalls()) -> F()
r374: eqc(calls(E1,S1,CS1),calls(E2,S2,CS2)) -> and(eqt(E1,E2),and(eqs(S1,S2),eqc(CS1,CS2)))
r375: push(E1,E2,nocalls()) -> calls(E1,stack(E2,empty()),nocalls())
r376: push(E1,E2,calls(E3,S1,CS1)) -> push1(E1,E2,E3,S1,CS1,eqt(E1,E3))
r377: push1(E1,E2,E3,S1,CS1,T()) -> calls(E3,pushs(E2,S1),CS1)

The estimated dependency graph contains the following SCCs:

  {p58}
  {p52}
  {p1, p3, p4, p6, p7, p8}
  {p9}
  {p10}
  {p13}
  {p14}
  {p44}
  {p42}
  {p43}


-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: eqc#(calls(E1,S1,CS1),calls(E2,S2,CS2)) -> eqc#(CS1,CS2)

and R consists of:

r1: or(T(),T()) -> T()
r2: or(F(),T()) -> T()
r3: or(T(),F()) -> T()
r4: or(F(),F()) -> F()
r5: and(T(),B) -> B
r6: and(B,T()) -> B
r7: and(F(),B) -> F()
r8: and(B,F()) -> F()
r9: imp(T(),B) -> B
r10: imp(F(),B) -> T()
r11: not(T()) -> F()
r12: not(F()) -> T()
r13: if(T(),B1,B2) -> B1
r14: if(F(),B1,B2) -> B2
r15: eq(T(),T()) -> T()
r16: eq(F(),F()) -> T()
r17: eq(T(),F()) -> F()
r18: eq(F(),T()) -> F()
r19: eqt(nil(),undefined()) -> F()
r20: eqt(nil(),pid(N2)) -> F()
r21: eqt(nil(),int(N2)) -> F()
r22: eqt(nil(),cons(H2,T2)) -> F()
r23: eqt(nil(),tuple(H2,T2)) -> F()
r24: eqt(nil(),tuplenil(H2)) -> F()
r25: eqt(a(),nil()) -> F()
r26: eqt(a(),a()) -> T()
r27: eqt(a(),excl()) -> F()
r28: eqt(a(),false()) -> F()
r29: eqt(a(),lock()) -> F()
r30: eqt(a(),locker()) -> F()
r31: eqt(a(),mcrlrecord()) -> F()
r32: eqt(a(),ok()) -> F()
r33: eqt(a(),pending()) -> F()
r34: eqt(a(),release()) -> F()
r35: eqt(a(),request()) -> F()
r36: eqt(a(),resource()) -> F()
r37: eqt(a(),tag()) -> F()
r38: eqt(a(),true()) -> F()
r39: eqt(a(),undefined()) -> F()
r40: eqt(a(),pid(N2)) -> F()
r41: eqt(a(),int(N2)) -> F()
r42: eqt(a(),cons(H2,T2)) -> F()
r43: eqt(a(),tuple(H2,T2)) -> F()
r44: eqt(a(),tuplenil(H2)) -> F()
r45: eqt(excl(),nil()) -> F()
r46: eqt(excl(),a()) -> F()
r47: eqt(excl(),excl()) -> T()
r48: eqt(excl(),false()) -> F()
r49: eqt(excl(),lock()) -> F()
r50: eqt(excl(),locker()) -> F()
r51: eqt(excl(),mcrlrecord()) -> F()
r52: eqt(excl(),ok()) -> F()
r53: eqt(excl(),pending()) -> F()
r54: eqt(excl(),release()) -> F()
r55: eqt(excl(),request()) -> F()
r56: eqt(excl(),resource()) -> F()
r57: eqt(excl(),tag()) -> F()
r58: eqt(excl(),true()) -> F()
r59: eqt(excl(),undefined()) -> F()
r60: eqt(excl(),pid(N2)) -> F()
r61: eqt(excl(),eqt(false(),int(N2))) -> F()
r62: eqt(false(),cons(H2,T2)) -> F()
r63: eqt(false(),tuple(H2,T2)) -> F()
r64: eqt(false(),tuplenil(H2)) -> F()
r65: eqt(lock(),nil()) -> F()
r66: eqt(lock(),a()) -> F()
r67: eqt(lock(),excl()) -> F()
r68: eqt(lock(),false()) -> F()
r69: eqt(lock(),lock()) -> T()
r70: eqt(lock(),locker()) -> F()
r71: eqt(lock(),mcrlrecord()) -> F()
r72: eqt(lock(),ok()) -> F()
r73: eqt(lock(),pending()) -> F()
r74: eqt(lock(),release()) -> F()
r75: eqt(lock(),request()) -> F()
r76: eqt(lock(),resource()) -> F()
r77: eqt(lock(),tag()) -> F()
r78: eqt(lock(),true()) -> F()
r79: eqt(lock(),undefined()) -> F()
r80: eqt(lock(),pid(N2)) -> F()
r81: eqt(lock(),int(N2)) -> F()
r82: eqt(lock(),cons(H2,T2)) -> F()
r83: eqt(lock(),tuple(H2,T2)) -> F()
r84: eqt(lock(),tuplenil(H2)) -> F()
r85: eqt(locker(),nil()) -> F()
r86: eqt(locker(),a()) -> F()
r87: eqt(locker(),excl()) -> F()
r88: eqt(locker(),false()) -> F()
r89: eqt(locker(),lock()) -> F()
r90: eqt(locker(),locker()) -> T()
r91: eqt(locker(),mcrlrecord()) -> F()
r92: eqt(locker(),ok()) -> F()
r93: eqt(locker(),pending()) -> F()
r94: eqt(locker(),release()) -> F()
r95: eqt(locker(),request()) -> F()
r96: eqt(locker(),resource()) -> F()
r97: eqt(locker(),tag()) -> F()
r98: eqt(locker(),true()) -> F()
r99: eqt(locker(),undefined()) -> F()
r100: eqt(locker(),pid(N2)) -> F()
r101: eqt(locker(),int(N2)) -> F()
r102: eqt(locker(),cons(H2,T2)) -> F()
r103: eqt(locker(),tuple(H2,T2)) -> F()
r104: eqt(locker(),tuplenil(H2)) -> F()
r105: eqt(mcrlrecord(),nil()) -> F()
r106: eqt(mcrlrecord(),a()) -> F()
r107: eqt(mcrlrecord(),excl()) -> F()
r108: eqt(mcrlrecord(),false()) -> F()
r109: eqt(mcrlrecord(),lock()) -> F()
r110: eqt(mcrlrecord(),locker()) -> F()
r111: eqt(mcrlrecord(),mcrlrecord()) -> T()
r112: eqt(mcrlrecord(),ok()) -> F()
r113: eqt(mcrlrecord(),pending()) -> F()
r114: eqt(mcrlrecord(),release()) -> F()
r115: eqt(mcrlrecord(),request()) -> F()
r116: eqt(mcrlrecord(),resource()) -> F()
r117: eqt(ok(),resource()) -> F()
r118: eqt(ok(),tag()) -> F()
r119: eqt(ok(),true()) -> F()
r120: eqt(ok(),undefined()) -> F()
r121: eqt(ok(),pid(N2)) -> F()
r122: eqt(ok(),int(N2)) -> F()
r123: eqt(ok(),cons(H2,T2)) -> F()
r124: eqt(ok(),tuple(H2,T2)) -> F()
r125: eqt(ok(),tuplenil(H2)) -> F()
r126: eqt(pending(),nil()) -> F()
r127: eqt(pending(),a()) -> F()
r128: eqt(pending(),excl()) -> F()
r129: eqt(pending(),false()) -> F()
r130: eqt(pending(),lock()) -> F()
r131: eqt(pending(),locker()) -> F()
r132: eqt(pending(),mcrlrecord()) -> F()
r133: eqt(pending(),ok()) -> F()
r134: eqt(pending(),pending()) -> T()
r135: eqt(pending(),release()) -> F()
r136: eqt(pending(),request()) -> F()
r137: eqt(pending(),resource()) -> F()
r138: eqt(pending(),tag()) -> F()
r139: eqt(pending(),true()) -> F()
r140: eqt(pending(),undefined()) -> F()
r141: eqt(pending(),pid(N2)) -> F()
r142: eqt(pending(),int(N2)) -> F()
r143: eqt(pending(),cons(H2,T2)) -> F()
r144: eqt(pending(),tuple(H2,T2)) -> F()
r145: eqt(pending(),tuplenil(H2)) -> F()
r146: eqt(release(),nil()) -> F()
r147: eqt(release(),a()) -> F()
r148: eqt(release(),excl()) -> F()
r149: eqt(release(),false()) -> F()
r150: eqt(release(),lock()) -> F()
r151: eqt(release(),locker()) -> F()
r152: eqt(release(),mcrlrecord()) -> F()
r153: eqt(release(),ok()) -> F()
r154: eqt(request(),mcrlrecord()) -> F()
r155: eqt(request(),ok()) -> F()
r156: eqt(request(),pending()) -> F()
r157: eqt(request(),release()) -> F()
r158: eqt(request(),request()) -> T()
r159: eqt(request(),resource()) -> F()
r160: eqt(request(),tag()) -> F()
r161: eqt(request(),true()) -> F()
r162: eqt(request(),undefined()) -> F()
r163: eqt(request(),pid(N2)) -> F()
r164: eqt(request(),int(N2)) -> F()
r165: eqt(request(),cons(H2,T2)) -> F()
r166: eqt(request(),tuple(H2,T2)) -> F()
r167: eqt(request(),tuplenil(H2)) -> F()
r168: eqt(resource(),nil()) -> F()
r169: eqt(resource(),a()) -> F()
r170: eqt(resource(),excl()) -> F()
r171: eqt(resource(),false()) -> F()
r172: eqt(resource(),lock()) -> F()
r173: eqt(resource(),locker()) -> F()
r174: eqt(resource(),mcrlrecord()) -> F()
r175: eqt(resource(),ok()) -> F()
r176: eqt(resource(),pending()) -> F()
r177: eqt(resource(),release()) -> F()
r178: eqt(resource(),request()) -> F()
r179: eqt(resource(),resource()) -> T()
r180: eqt(resource(),tag()) -> F()
r181: eqt(resource(),true()) -> F()
r182: eqt(resource(),undefined()) -> F()
r183: eqt(resource(),pid(N2)) -> F()
r184: eqt(resource(),int(N2)) -> F()
r185: eqt(resource(),cons(H2,T2)) -> F()
r186: eqt(resource(),tuple(H2,T2)) -> F()
r187: eqt(resource(),tuplenil(H2)) -> F()
r188: eqt(tag(),nil()) -> F()
r189: eqt(tag(),a()) -> F()
r190: eqt(tag(),excl()) -> F()
r191: eqt(tag(),false()) -> F()
r192: eqt(tag(),lock()) -> F()
r193: eqt(tag(),locker()) -> F()
r194: eqt(tag(),mcrlrecord()) -> F()
r195: eqt(tag(),ok()) -> F()
r196: eqt(tag(),pending()) -> F()
r197: eqt(tag(),release()) -> F()
r198: eqt(tag(),request()) -> F()
r199: eqt(tag(),resource()) -> F()
r200: eqt(tag(),tag()) -> T()
r201: eqt(tag(),true()) -> F()
r202: eqt(tag(),undefined()) -> F()
r203: eqt(tag(),pid(N2)) -> F()
r204: eqt(tag(),int(N2)) -> F()
r205: eqt(tag(),cons(H2,T2)) -> F()
r206: eqt(tag(),tuple(H2,T2)) -> F()
r207: eqt(tag(),tuplenil(H2)) -> F()
r208: eqt(true(),nil()) -> F()
r209: eqt(true(),a()) -> F()
r210: eqt(true(),excl()) -> F()
r211: eqt(true(),false()) -> F()
r212: eqt(true(),lock()) -> F()
r213: eqt(true(),locker()) -> F()
r214: eqt(true(),mcrlrecord()) -> F()
r215: eqt(true(),ok()) -> F()
r216: eqt(true(),pending()) -> F()
r217: eqt(true(),release()) -> F()
r218: eqt(true(),request()) -> F()
r219: eqt(true(),resource()) -> F()
r220: eqt(true(),tag()) -> F()
r221: eqt(true(),true()) -> T()
r222: eqt(true(),undefined()) -> F()
r223: eqt(true(),pid(N2)) -> F()
r224: eqt(true(),int(N2)) -> F()
r225: eqt(true(),cons(H2,T2)) -> F()
r226: eqt(true(),tuple(H2,T2)) -> F()
r227: eqt(true(),tuplenil(H2)) -> F()
r228: eqt(undefined(),nil()) -> F()
r229: eqt(undefined(),a()) -> F()
r230: eqt(undefined(),tuplenil(H2)) -> F()
r231: eqt(pid(N1),nil()) -> F()
r232: eqt(pid(N1),a()) -> F()
r233: eqt(pid(N1),excl()) -> F()
r234: eqt(pid(N1),false()) -> F()
r235: eqt(pid(N1),lock()) -> F()
r236: eqt(pid(N1),locker()) -> F()
r237: eqt(pid(N1),mcrlrecord()) -> F()
r238: eqt(pid(N1),ok()) -> F()
r239: eqt(pid(N1),pending()) -> F()
r240: eqt(pid(N1),release()) -> F()
r241: eqt(pid(N1),request()) -> F()
r242: eqt(pid(N1),resource()) -> F()
r243: eqt(pid(N1),tag()) -> F()
r244: eqt(pid(N1),true()) -> F()
r245: eqt(pid(N1),undefined()) -> F()
r246: eqt(pid(N1),pid(N2)) -> eqt(N1,N2)
r247: eqt(pid(N1),int(N2)) -> F()
r248: eqt(pid(N1),cons(H2,T2)) -> F()
r249: eqt(pid(N1),tuple(H2,T2)) -> F()
r250: eqt(pid(N1),tuplenil(H2)) -> F()
r251: eqt(int(N1),nil()) -> F()
r252: eqt(int(N1),a()) -> F()
r253: eqt(int(N1),excl()) -> F()
r254: eqt(int(N1),false()) -> F()
r255: eqt(int(N1),lock()) -> F()
r256: eqt(int(N1),locker()) -> F()
r257: eqt(int(N1),mcrlrecord()) -> F()
r258: eqt(int(N1),ok()) -> F()
r259: eqt(int(N1),pending()) -> F()
r260: eqt(int(N1),release()) -> F()
r261: eqt(int(N1),request()) -> F()
r262: eqt(int(N1),resource()) -> F()
r263: eqt(int(N1),tag()) -> F()
r264: eqt(int(N1),true()) -> F()
r265: eqt(int(N1),undefined()) -> F()
r266: eqt(cons(H1,T1),resource()) -> F()
r267: eqt(cons(H1,T1),tag()) -> F()
r268: eqt(cons(H1,T1),true()) -> F()
r269: eqt(cons(H1,T1),undefined()) -> F()
r270: eqt(cons(H1,T1),pid(N2)) -> F()
r271: eqt(cons(H1,T1),int(N2)) -> F()
r272: eqt(cons(H1,T1),cons(H2,T2)) -> and(eqt(H1,H2),eqt(T1,T2))
r273: eqt(cons(H1,T1),tuple(H2,T2)) -> F()
r274: eqt(cons(H1,T1),tuplenil(H2)) -> F()
r275: eqt(tuple(H1,T1),nil()) -> F()
r276: eqt(tuple(H1,T1),a()) -> F()
r277: eqt(tuple(H1,T1),excl()) -> F()
r278: eqt(tuple(H1,T1),false()) -> F()
r279: eqt(tuple(H1,T1),lock()) -> F()
r280: eqt(tuple(H1,T1),locker()) -> F()
r281: eqt(tuple(H1,T1),mcrlrecord()) -> F()
r282: eqt(tuple(H1,T1),ok()) -> F()
r283: eqt(tuple(H1,T1),pending()) -> F()
r284: eqt(tuple(H1,T1),release()) -> F()
r285: eqt(tuple(H1,T1),request()) -> F()
r286: eqt(tuple(H1,T1),resource()) -> F()
r287: eqt(tuple(H1,T1),tag()) -> F()
r288: eqt(tuple(H1,T1),true()) -> F()
r289: eqt(tuple(H1,T1),undefined()) -> F()
r290: eqt(tuple(H1,T1),pid(N2)) -> F()
r291: eqt(tuple(H1,T1),int(N2)) -> F()
r292: eqt(tuple(H1,T1),cons(H2,T2)) -> F()
r293: eqt(tuple(H1,T1),tuple(H2,T2)) -> and(eqt(H1,H2),eqt(T1,T2))
r294: eqt(tuple(H1,T1),tuplenil(H2)) -> F()
r295: eqt(tuplenil(H1),nil()) -> F()
r296: eqt(tuplenil(H1),a()) -> F()
r297: eqt(tuplenil(H1),excl()) -> F()
r298: eqt(tuplenil(H1),false()) -> F()
r299: eqt(tuplenil(H1),lock()) -> F()
r300: eqt(tuplenil(H1),locker()) -> F()
r301: eqt(tuplenil(H1),mcrlrecord()) -> F()
r302: eqt(tuplenil(H1),ok()) -> F()
r303: eqt(tuplenil(H1),pending()) -> F()
r304: eqt(tuplenil(H1),release()) -> F()
r305: eqt(tuplenil(H1),request()) -> F()
r306: eqt(tuplenil(H1),resource()) -> F()
r307: eqt(tuplenil(H1),tag()) -> F()
r308: eqt(tuplenil(H1),true()) -> F()
r309: eqt(tuplenil(H1),undefined()) -> F()
r310: eqt(tuplenil(H1),pid(N2)) -> F()
r311: eqt(tuplenil(H1),int(N2)) -> F()
r312: eqt(tuplenil(H1),cons(H2,T2)) -> F()
r313: eqt(tuplenil(H1),tuple(H2,T2)) -> F()
r314: eqt(tuplenil(H1),tuplenil(H2)) -> eqt(H1,H2)
r315: element(int(s(|0|())),tuplenil(T1)) -> T1
r316: element(int(s(|0|())),tuple(T1,T2)) -> T1
r317: element(int(s(s(N1))),tuple(T1,T2)) -> element(int(s(N1)),T2)
r318: record_new(lock()) -> tuple(mcrlrecord(),tuple(lock(),tuple(undefined(),tuple(nil(),tuplenil(nil())))))
r319: record_extract(tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(F2))))),lock(),resource()) -> tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(F2)))))
r320: 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)))))
r321: record_updates(Record,Name,nil()) -> Record
r322: record_updates(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields)) -> record_updates(record_update(Record,Name,Field,NewF),Name,Fields)
r323: locker2_map_promote_pending(nil(),Pending) -> nil()
r324: locker2_map_promote_pending(cons(Lock,Locks),Pending) -> cons(locker2_promote_pending(Lock,Pending),locker2_map_promote_pending(Locks,Pending))
r325: locker2_map_claim_lock(nil(),Resources,Client) -> nil()
r326: locker2_map_claim_lock(cons(Lock,Locks),Resources,Client) -> cons(locker2_claim_lock(Lock,Resources,Client),locker2_map_claim_lock(Locks,Resources,Client))
r327: locker2_map_add_pending(nil(),Resources,Client) -> nil()
r328: locker2_promote_pending(Lock,Client) -> case0(Client,Lock,record_extract(Lock,lock(),pending()))
r329: case0(Client,Lock,cons(Client,Pendings)) -> record_updates(Lock,lock(),cons(tuple(excl(),tuplenil(Client)),cons(tuple(pending(),tuplenil(Pendings)),nil())))
r330: case0(Client,Lock,MCRLFree0) -> Lock
r331: locker2_remove_pending(Lock,Client) -> record_updates(Lock,lock(),cons(tuple(pending(),tuplenil(subtract(record_extract(Lock,lock(),pending()),cons(Client,nil())))),nil()))
r332: locker2_add_pending(Lock,Resources,Client) -> case1(Client,Resources,Lock,member(record_extract(Lock,lock(),resource()),Resources))
r333: case1(Client,Resources,Lock,true()) -> record_updates(Lock,lock(),cons(tuple(pending(),tuplenil(append(record_extract(Lock,lock(),pending()),cons(Client,nil())))),nil()))
r334: case1(Client,Resources,Lock,false()) -> Lock
r335: locker2_release_lock(Lock,Client) -> case2(Client,Lock,gen_modtageq(Client,record_extract(Lock,lock(),excl())))
r336: case2(Client,Lock,true()) -> record_updates(Lock,lock(),cons(tuple(excllock(),excl()),nil()))
r337: case4(Client,Lock,MCRLFree1) -> false()
r338: locker2_obtainables(nil(),Client) -> true()
r339: locker2_obtainables(cons(Lock,Locks),Client) -> case5(Client,Locks,Lock,member(Client,record_extract(Lock,lock(),pending())))
r340: case5(Client,Locks,Lock,true()) -> andt(locker2_obtainable(Lock,Client),locker2_obtainables(Locks,Client))
r341: case5(Client,Locks,Lock,false()) -> locker2_obtainables(Locks,Client)
r342: locker2_check_available(Resource,nil()) -> false()
r343: locker2_check_available(Resource,cons(Lock,Locks)) -> case6(Locks,Lock,Resource,equal(Resource,record_extract(Lock,lock(),resource())))
r344: case6(Locks,Lock,Resource,true()) -> andt(equal(record_extract(Lock,lock(),excl()),nil()),equal(record_extract(Lock,lock(),pending()),nil()))
r345: case6(Locks,Lock,Resource,false()) -> locker2_check_available(Resource,Locks)
r346: locker2_check_availables(nil(),Locks) -> true()
r347: locker2_check_availables(cons(Resource,Resources),Locks) -> andt(locker2_check_available(Resource,Locks),locker2_check_availables(Resources,Locks))
r348: locker2_adduniq(nil(),List) -> List
r349: append(cons(Head,Tail),List) -> cons(Head,append(Tail,List))
r350: subtract(List,nil()) -> List
r351: subtract(List,cons(Head,Tail)) -> subtract(delete(Head,List),Tail)
r352: delete(E,nil()) -> nil()
r353: delete(E,cons(Head,Tail)) -> case8(Tail,Head,E,equal(E,Head))
r354: case8(Tail,Head,E,true()) -> Tail
r355: case8(Tail,Head,E,false()) -> cons(Head,delete(E,Tail))
r356: gen_tag(Pid) -> tuple(Pid,tuplenil(tag()))
r357: gen_modtageq(Client1,Client2) -> equal(Client1,Client2)
r358: member(E,nil()) -> false()
r359: member(E,cons(Head,Tail)) -> case9(Tail,Head,E,equal(E,Head))
r360: case9(Tail,Head,E,true()) -> true()
r361: case9(Tail,Head,E,false()) -> member(E,Tail)
r362: eqs(empty(),empty()) -> T()
r363: eqs(empty(),stack(E2,S2)) -> F()
r364: eqs(stack(E1,S1),empty()) -> F()
r365: eqs(stack(E1,S1),stack(E2,S2)) -> and(eqt(E1,E2),eqs(S1,S2))
r366: pushs(E1,S1) -> stack(E1,S1)
r367: pops(stack(E1,S1)) -> S1
r368: tops(stack(E1,S1)) -> E1
r369: istops(E1,empty()) -> F()
r370: istops(E1,stack(E2,S1)) -> eqt(E1,E2)
r371: eqc(nocalls(),nocalls()) -> T()
r372: eqc(nocalls(),calls(E2,S2,CS2)) -> F()
r373: eqc(calls(E1,S1,CS1),nocalls()) -> F()
r374: eqc(calls(E1,S1,CS1),calls(E2,S2,CS2)) -> and(eqt(E1,E2),and(eqs(S1,S2),eqc(CS1,CS2)))
r375: push(E1,E2,nocalls()) -> calls(E1,stack(E2,empty()),nocalls())
r376: push(E1,E2,calls(E3,S1,CS1)) -> push1(E1,E2,E3,S1,CS1,eqt(E1,E3))
r377: push1(E1,E2,E3,S1,CS1,T()) -> calls(E3,pushs(E2,S1),CS1)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      eqc#_A(x1,x2) = ((1,0,0),(1,0,0),(0,1,0)) x1 + ((1,0,0),(0,0,0),(0,1,0)) x2
      calls_A(x1,x2,x3) = ((0,0,0),(0,0,0),(1,0,0)) x1 + ((1,0,0),(1,1,0),(1,1,1)) x2 + ((1,0,0),(1,1,0),(1,1,1)) x3 + (1,1,1)

The next rules are strictly ordered:

  p1

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: eqs#(stack(E1,S1),stack(E2,S2)) -> eqs#(S1,S2)

and R consists of:

r1: or(T(),T()) -> T()
r2: or(F(),T()) -> T()
r3: or(T(),F()) -> T()
r4: or(F(),F()) -> F()
r5: and(T(),B) -> B
r6: and(B,T()) -> B
r7: and(F(),B) -> F()
r8: and(B,F()) -> F()
r9: imp(T(),B) -> B
r10: imp(F(),B) -> T()
r11: not(T()) -> F()
r12: not(F()) -> T()
r13: if(T(),B1,B2) -> B1
r14: if(F(),B1,B2) -> B2
r15: eq(T(),T()) -> T()
r16: eq(F(),F()) -> T()
r17: eq(T(),F()) -> F()
r18: eq(F(),T()) -> F()
r19: eqt(nil(),undefined()) -> F()
r20: eqt(nil(),pid(N2)) -> F()
r21: eqt(nil(),int(N2)) -> F()
r22: eqt(nil(),cons(H2,T2)) -> F()
r23: eqt(nil(),tuple(H2,T2)) -> F()
r24: eqt(nil(),tuplenil(H2)) -> F()
r25: eqt(a(),nil()) -> F()
r26: eqt(a(),a()) -> T()
r27: eqt(a(),excl()) -> F()
r28: eqt(a(),false()) -> F()
r29: eqt(a(),lock()) -> F()
r30: eqt(a(),locker()) -> F()
r31: eqt(a(),mcrlrecord()) -> F()
r32: eqt(a(),ok()) -> F()
r33: eqt(a(),pending()) -> F()
r34: eqt(a(),release()) -> F()
r35: eqt(a(),request()) -> F()
r36: eqt(a(),resource()) -> F()
r37: eqt(a(),tag()) -> F()
r38: eqt(a(),true()) -> F()
r39: eqt(a(),undefined()) -> F()
r40: eqt(a(),pid(N2)) -> F()
r41: eqt(a(),int(N2)) -> F()
r42: eqt(a(),cons(H2,T2)) -> F()
r43: eqt(a(),tuple(H2,T2)) -> F()
r44: eqt(a(),tuplenil(H2)) -> F()
r45: eqt(excl(),nil()) -> F()
r46: eqt(excl(),a()) -> F()
r47: eqt(excl(),excl()) -> T()
r48: eqt(excl(),false()) -> F()
r49: eqt(excl(),lock()) -> F()
r50: eqt(excl(),locker()) -> F()
r51: eqt(excl(),mcrlrecord()) -> F()
r52: eqt(excl(),ok()) -> F()
r53: eqt(excl(),pending()) -> F()
r54: eqt(excl(),release()) -> F()
r55: eqt(excl(),request()) -> F()
r56: eqt(excl(),resource()) -> F()
r57: eqt(excl(),tag()) -> F()
r58: eqt(excl(),true()) -> F()
r59: eqt(excl(),undefined()) -> F()
r60: eqt(excl(),pid(N2)) -> F()
r61: eqt(excl(),eqt(false(),int(N2))) -> F()
r62: eqt(false(),cons(H2,T2)) -> F()
r63: eqt(false(),tuple(H2,T2)) -> F()
r64: eqt(false(),tuplenil(H2)) -> F()
r65: eqt(lock(),nil()) -> F()
r66: eqt(lock(),a()) -> F()
r67: eqt(lock(),excl()) -> F()
r68: eqt(lock(),false()) -> F()
r69: eqt(lock(),lock()) -> T()
r70: eqt(lock(),locker()) -> F()
r71: eqt(lock(),mcrlrecord()) -> F()
r72: eqt(lock(),ok()) -> F()
r73: eqt(lock(),pending()) -> F()
r74: eqt(lock(),release()) -> F()
r75: eqt(lock(),request()) -> F()
r76: eqt(lock(),resource()) -> F()
r77: eqt(lock(),tag()) -> F()
r78: eqt(lock(),true()) -> F()
r79: eqt(lock(),undefined()) -> F()
r80: eqt(lock(),pid(N2)) -> F()
r81: eqt(lock(),int(N2)) -> F()
r82: eqt(lock(),cons(H2,T2)) -> F()
r83: eqt(lock(),tuple(H2,T2)) -> F()
r84: eqt(lock(),tuplenil(H2)) -> F()
r85: eqt(locker(),nil()) -> F()
r86: eqt(locker(),a()) -> F()
r87: eqt(locker(),excl()) -> F()
r88: eqt(locker(),false()) -> F()
r89: eqt(locker(),lock()) -> F()
r90: eqt(locker(),locker()) -> T()
r91: eqt(locker(),mcrlrecord()) -> F()
r92: eqt(locker(),ok()) -> F()
r93: eqt(locker(),pending()) -> F()
r94: eqt(locker(),release()) -> F()
r95: eqt(locker(),request()) -> F()
r96: eqt(locker(),resource()) -> F()
r97: eqt(locker(),tag()) -> F()
r98: eqt(locker(),true()) -> F()
r99: eqt(locker(),undefined()) -> F()
r100: eqt(locker(),pid(N2)) -> F()
r101: eqt(locker(),int(N2)) -> F()
r102: eqt(locker(),cons(H2,T2)) -> F()
r103: eqt(locker(),tuple(H2,T2)) -> F()
r104: eqt(locker(),tuplenil(H2)) -> F()
r105: eqt(mcrlrecord(),nil()) -> F()
r106: eqt(mcrlrecord(),a()) -> F()
r107: eqt(mcrlrecord(),excl()) -> F()
r108: eqt(mcrlrecord(),false()) -> F()
r109: eqt(mcrlrecord(),lock()) -> F()
r110: eqt(mcrlrecord(),locker()) -> F()
r111: eqt(mcrlrecord(),mcrlrecord()) -> T()
r112: eqt(mcrlrecord(),ok()) -> F()
r113: eqt(mcrlrecord(),pending()) -> F()
r114: eqt(mcrlrecord(),release()) -> F()
r115: eqt(mcrlrecord(),request()) -> F()
r116: eqt(mcrlrecord(),resource()) -> F()
r117: eqt(ok(),resource()) -> F()
r118: eqt(ok(),tag()) -> F()
r119: eqt(ok(),true()) -> F()
r120: eqt(ok(),undefined()) -> F()
r121: eqt(ok(),pid(N2)) -> F()
r122: eqt(ok(),int(N2)) -> F()
r123: eqt(ok(),cons(H2,T2)) -> F()
r124: eqt(ok(),tuple(H2,T2)) -> F()
r125: eqt(ok(),tuplenil(H2)) -> F()
r126: eqt(pending(),nil()) -> F()
r127: eqt(pending(),a()) -> F()
r128: eqt(pending(),excl()) -> F()
r129: eqt(pending(),false()) -> F()
r130: eqt(pending(),lock()) -> F()
r131: eqt(pending(),locker()) -> F()
r132: eqt(pending(),mcrlrecord()) -> F()
r133: eqt(pending(),ok()) -> F()
r134: eqt(pending(),pending()) -> T()
r135: eqt(pending(),release()) -> F()
r136: eqt(pending(),request()) -> F()
r137: eqt(pending(),resource()) -> F()
r138: eqt(pending(),tag()) -> F()
r139: eqt(pending(),true()) -> F()
r140: eqt(pending(),undefined()) -> F()
r141: eqt(pending(),pid(N2)) -> F()
r142: eqt(pending(),int(N2)) -> F()
r143: eqt(pending(),cons(H2,T2)) -> F()
r144: eqt(pending(),tuple(H2,T2)) -> F()
r145: eqt(pending(),tuplenil(H2)) -> F()
r146: eqt(release(),nil()) -> F()
r147: eqt(release(),a()) -> F()
r148: eqt(release(),excl()) -> F()
r149: eqt(release(),false()) -> F()
r150: eqt(release(),lock()) -> F()
r151: eqt(release(),locker()) -> F()
r152: eqt(release(),mcrlrecord()) -> F()
r153: eqt(release(),ok()) -> F()
r154: eqt(request(),mcrlrecord()) -> F()
r155: eqt(request(),ok()) -> F()
r156: eqt(request(),pending()) -> F()
r157: eqt(request(),release()) -> F()
r158: eqt(request(),request()) -> T()
r159: eqt(request(),resource()) -> F()
r160: eqt(request(),tag()) -> F()
r161: eqt(request(),true()) -> F()
r162: eqt(request(),undefined()) -> F()
r163: eqt(request(),pid(N2)) -> F()
r164: eqt(request(),int(N2)) -> F()
r165: eqt(request(),cons(H2,T2)) -> F()
r166: eqt(request(),tuple(H2,T2)) -> F()
r167: eqt(request(),tuplenil(H2)) -> F()
r168: eqt(resource(),nil()) -> F()
r169: eqt(resource(),a()) -> F()
r170: eqt(resource(),excl()) -> F()
r171: eqt(resource(),false()) -> F()
r172: eqt(resource(),lock()) -> F()
r173: eqt(resource(),locker()) -> F()
r174: eqt(resource(),mcrlrecord()) -> F()
r175: eqt(resource(),ok()) -> F()
r176: eqt(resource(),pending()) -> F()
r177: eqt(resource(),release()) -> F()
r178: eqt(resource(),request()) -> F()
r179: eqt(resource(),resource()) -> T()
r180: eqt(resource(),tag()) -> F()
r181: eqt(resource(),true()) -> F()
r182: eqt(resource(),undefined()) -> F()
r183: eqt(resource(),pid(N2)) -> F()
r184: eqt(resource(),int(N2)) -> F()
r185: eqt(resource(),cons(H2,T2)) -> F()
r186: eqt(resource(),tuple(H2,T2)) -> F()
r187: eqt(resource(),tuplenil(H2)) -> F()
r188: eqt(tag(),nil()) -> F()
r189: eqt(tag(),a()) -> F()
r190: eqt(tag(),excl()) -> F()
r191: eqt(tag(),false()) -> F()
r192: eqt(tag(),lock()) -> F()
r193: eqt(tag(),locker()) -> F()
r194: eqt(tag(),mcrlrecord()) -> F()
r195: eqt(tag(),ok()) -> F()
r196: eqt(tag(),pending()) -> F()
r197: eqt(tag(),release()) -> F()
r198: eqt(tag(),request()) -> F()
r199: eqt(tag(),resource()) -> F()
r200: eqt(tag(),tag()) -> T()
r201: eqt(tag(),true()) -> F()
r202: eqt(tag(),undefined()) -> F()
r203: eqt(tag(),pid(N2)) -> F()
r204: eqt(tag(),int(N2)) -> F()
r205: eqt(tag(),cons(H2,T2)) -> F()
r206: eqt(tag(),tuple(H2,T2)) -> F()
r207: eqt(tag(),tuplenil(H2)) -> F()
r208: eqt(true(),nil()) -> F()
r209: eqt(true(),a()) -> F()
r210: eqt(true(),excl()) -> F()
r211: eqt(true(),false()) -> F()
r212: eqt(true(),lock()) -> F()
r213: eqt(true(),locker()) -> F()
r214: eqt(true(),mcrlrecord()) -> F()
r215: eqt(true(),ok()) -> F()
r216: eqt(true(),pending()) -> F()
r217: eqt(true(),release()) -> F()
r218: eqt(true(),request()) -> F()
r219: eqt(true(),resource()) -> F()
r220: eqt(true(),tag()) -> F()
r221: eqt(true(),true()) -> T()
r222: eqt(true(),undefined()) -> F()
r223: eqt(true(),pid(N2)) -> F()
r224: eqt(true(),int(N2)) -> F()
r225: eqt(true(),cons(H2,T2)) -> F()
r226: eqt(true(),tuple(H2,T2)) -> F()
r227: eqt(true(),tuplenil(H2)) -> F()
r228: eqt(undefined(),nil()) -> F()
r229: eqt(undefined(),a()) -> F()
r230: eqt(undefined(),tuplenil(H2)) -> F()
r231: eqt(pid(N1),nil()) -> F()
r232: eqt(pid(N1),a()) -> F()
r233: eqt(pid(N1),excl()) -> F()
r234: eqt(pid(N1),false()) -> F()
r235: eqt(pid(N1),lock()) -> F()
r236: eqt(pid(N1),locker()) -> F()
r237: eqt(pid(N1),mcrlrecord()) -> F()
r238: eqt(pid(N1),ok()) -> F()
r239: eqt(pid(N1),pending()) -> F()
r240: eqt(pid(N1),release()) -> F()
r241: eqt(pid(N1),request()) -> F()
r242: eqt(pid(N1),resource()) -> F()
r243: eqt(pid(N1),tag()) -> F()
r244: eqt(pid(N1),true()) -> F()
r245: eqt(pid(N1),undefined()) -> F()
r246: eqt(pid(N1),pid(N2)) -> eqt(N1,N2)
r247: eqt(pid(N1),int(N2)) -> F()
r248: eqt(pid(N1),cons(H2,T2)) -> F()
r249: eqt(pid(N1),tuple(H2,T2)) -> F()
r250: eqt(pid(N1),tuplenil(H2)) -> F()
r251: eqt(int(N1),nil()) -> F()
r252: eqt(int(N1),a()) -> F()
r253: eqt(int(N1),excl()) -> F()
r254: eqt(int(N1),false()) -> F()
r255: eqt(int(N1),lock()) -> F()
r256: eqt(int(N1),locker()) -> F()
r257: eqt(int(N1),mcrlrecord()) -> F()
r258: eqt(int(N1),ok()) -> F()
r259: eqt(int(N1),pending()) -> F()
r260: eqt(int(N1),release()) -> F()
r261: eqt(int(N1),request()) -> F()
r262: eqt(int(N1),resource()) -> F()
r263: eqt(int(N1),tag()) -> F()
r264: eqt(int(N1),true()) -> F()
r265: eqt(int(N1),undefined()) -> F()
r266: eqt(cons(H1,T1),resource()) -> F()
r267: eqt(cons(H1,T1),tag()) -> F()
r268: eqt(cons(H1,T1),true()) -> F()
r269: eqt(cons(H1,T1),undefined()) -> F()
r270: eqt(cons(H1,T1),pid(N2)) -> F()
r271: eqt(cons(H1,T1),int(N2)) -> F()
r272: eqt(cons(H1,T1),cons(H2,T2)) -> and(eqt(H1,H2),eqt(T1,T2))
r273: eqt(cons(H1,T1),tuple(H2,T2)) -> F()
r274: eqt(cons(H1,T1),tuplenil(H2)) -> F()
r275: eqt(tuple(H1,T1),nil()) -> F()
r276: eqt(tuple(H1,T1),a()) -> F()
r277: eqt(tuple(H1,T1),excl()) -> F()
r278: eqt(tuple(H1,T1),false()) -> F()
r279: eqt(tuple(H1,T1),lock()) -> F()
r280: eqt(tuple(H1,T1),locker()) -> F()
r281: eqt(tuple(H1,T1),mcrlrecord()) -> F()
r282: eqt(tuple(H1,T1),ok()) -> F()
r283: eqt(tuple(H1,T1),pending()) -> F()
r284: eqt(tuple(H1,T1),release()) -> F()
r285: eqt(tuple(H1,T1),request()) -> F()
r286: eqt(tuple(H1,T1),resource()) -> F()
r287: eqt(tuple(H1,T1),tag()) -> F()
r288: eqt(tuple(H1,T1),true()) -> F()
r289: eqt(tuple(H1,T1),undefined()) -> F()
r290: eqt(tuple(H1,T1),pid(N2)) -> F()
r291: eqt(tuple(H1,T1),int(N2)) -> F()
r292: eqt(tuple(H1,T1),cons(H2,T2)) -> F()
r293: eqt(tuple(H1,T1),tuple(H2,T2)) -> and(eqt(H1,H2),eqt(T1,T2))
r294: eqt(tuple(H1,T1),tuplenil(H2)) -> F()
r295: eqt(tuplenil(H1),nil()) -> F()
r296: eqt(tuplenil(H1),a()) -> F()
r297: eqt(tuplenil(H1),excl()) -> F()
r298: eqt(tuplenil(H1),false()) -> F()
r299: eqt(tuplenil(H1),lock()) -> F()
r300: eqt(tuplenil(H1),locker()) -> F()
r301: eqt(tuplenil(H1),mcrlrecord()) -> F()
r302: eqt(tuplenil(H1),ok()) -> F()
r303: eqt(tuplenil(H1),pending()) -> F()
r304: eqt(tuplenil(H1),release()) -> F()
r305: eqt(tuplenil(H1),request()) -> F()
r306: eqt(tuplenil(H1),resource()) -> F()
r307: eqt(tuplenil(H1),tag()) -> F()
r308: eqt(tuplenil(H1),true()) -> F()
r309: eqt(tuplenil(H1),undefined()) -> F()
r310: eqt(tuplenil(H1),pid(N2)) -> F()
r311: eqt(tuplenil(H1),int(N2)) -> F()
r312: eqt(tuplenil(H1),cons(H2,T2)) -> F()
r313: eqt(tuplenil(H1),tuple(H2,T2)) -> F()
r314: eqt(tuplenil(H1),tuplenil(H2)) -> eqt(H1,H2)
r315: element(int(s(|0|())),tuplenil(T1)) -> T1
r316: element(int(s(|0|())),tuple(T1,T2)) -> T1
r317: element(int(s(s(N1))),tuple(T1,T2)) -> element(int(s(N1)),T2)
r318: record_new(lock()) -> tuple(mcrlrecord(),tuple(lock(),tuple(undefined(),tuple(nil(),tuplenil(nil())))))
r319: record_extract(tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(F2))))),lock(),resource()) -> tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(F2)))))
r320: 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)))))
r321: record_updates(Record,Name,nil()) -> Record
r322: record_updates(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields)) -> record_updates(record_update(Record,Name,Field,NewF),Name,Fields)
r323: locker2_map_promote_pending(nil(),Pending) -> nil()
r324: locker2_map_promote_pending(cons(Lock,Locks),Pending) -> cons(locker2_promote_pending(Lock,Pending),locker2_map_promote_pending(Locks,Pending))
r325: locker2_map_claim_lock(nil(),Resources,Client) -> nil()
r326: locker2_map_claim_lock(cons(Lock,Locks),Resources,Client) -> cons(locker2_claim_lock(Lock,Resources,Client),locker2_map_claim_lock(Locks,Resources,Client))
r327: locker2_map_add_pending(nil(),Resources,Client) -> nil()
r328: locker2_promote_pending(Lock,Client) -> case0(Client,Lock,record_extract(Lock,lock(),pending()))
r329: case0(Client,Lock,cons(Client,Pendings)) -> record_updates(Lock,lock(),cons(tuple(excl(),tuplenil(Client)),cons(tuple(pending(),tuplenil(Pendings)),nil())))
r330: case0(Client,Lock,MCRLFree0) -> Lock
r331: locker2_remove_pending(Lock,Client) -> record_updates(Lock,lock(),cons(tuple(pending(),tuplenil(subtract(record_extract(Lock,lock(),pending()),cons(Client,nil())))),nil()))
r332: locker2_add_pending(Lock,Resources,Client) -> case1(Client,Resources,Lock,member(record_extract(Lock,lock(),resource()),Resources))
r333: case1(Client,Resources,Lock,true()) -> record_updates(Lock,lock(),cons(tuple(pending(),tuplenil(append(record_extract(Lock,lock(),pending()),cons(Client,nil())))),nil()))
r334: case1(Client,Resources,Lock,false()) -> Lock
r335: locker2_release_lock(Lock,Client) -> case2(Client,Lock,gen_modtageq(Client,record_extract(Lock,lock(),excl())))
r336: case2(Client,Lock,true()) -> record_updates(Lock,lock(),cons(tuple(excllock(),excl()),nil()))
r337: case4(Client,Lock,MCRLFree1) -> false()
r338: locker2_obtainables(nil(),Client) -> true()
r339: locker2_obtainables(cons(Lock,Locks),Client) -> case5(Client,Locks,Lock,member(Client,record_extract(Lock,lock(),pending())))
r340: case5(Client,Locks,Lock,true()) -> andt(locker2_obtainable(Lock,Client),locker2_obtainables(Locks,Client))
r341: case5(Client,Locks,Lock,false()) -> locker2_obtainables(Locks,Client)
r342: locker2_check_available(Resource,nil()) -> false()
r343: locker2_check_available(Resource,cons(Lock,Locks)) -> case6(Locks,Lock,Resource,equal(Resource,record_extract(Lock,lock(),resource())))
r344: case6(Locks,Lock,Resource,true()) -> andt(equal(record_extract(Lock,lock(),excl()),nil()),equal(record_extract(Lock,lock(),pending()),nil()))
r345: case6(Locks,Lock,Resource,false()) -> locker2_check_available(Resource,Locks)
r346: locker2_check_availables(nil(),Locks) -> true()
r347: locker2_check_availables(cons(Resource,Resources),Locks) -> andt(locker2_check_available(Resource,Locks),locker2_check_availables(Resources,Locks))
r348: locker2_adduniq(nil(),List) -> List
r349: append(cons(Head,Tail),List) -> cons(Head,append(Tail,List))
r350: subtract(List,nil()) -> List
r351: subtract(List,cons(Head,Tail)) -> subtract(delete(Head,List),Tail)
r352: delete(E,nil()) -> nil()
r353: delete(E,cons(Head,Tail)) -> case8(Tail,Head,E,equal(E,Head))
r354: case8(Tail,Head,E,true()) -> Tail
r355: case8(Tail,Head,E,false()) -> cons(Head,delete(E,Tail))
r356: gen_tag(Pid) -> tuple(Pid,tuplenil(tag()))
r357: gen_modtageq(Client1,Client2) -> equal(Client1,Client2)
r358: member(E,nil()) -> false()
r359: member(E,cons(Head,Tail)) -> case9(Tail,Head,E,equal(E,Head))
r360: case9(Tail,Head,E,true()) -> true()
r361: case9(Tail,Head,E,false()) -> member(E,Tail)
r362: eqs(empty(),empty()) -> T()
r363: eqs(empty(),stack(E2,S2)) -> F()
r364: eqs(stack(E1,S1),empty()) -> F()
r365: eqs(stack(E1,S1),stack(E2,S2)) -> and(eqt(E1,E2),eqs(S1,S2))
r366: pushs(E1,S1) -> stack(E1,S1)
r367: pops(stack(E1,S1)) -> S1
r368: tops(stack(E1,S1)) -> E1
r369: istops(E1,empty()) -> F()
r370: istops(E1,stack(E2,S1)) -> eqt(E1,E2)
r371: eqc(nocalls(),nocalls()) -> T()
r372: eqc(nocalls(),calls(E2,S2,CS2)) -> F()
r373: eqc(calls(E1,S1,CS1),nocalls()) -> F()
r374: eqc(calls(E1,S1,CS1),calls(E2,S2,CS2)) -> and(eqt(E1,E2),and(eqs(S1,S2),eqc(CS1,CS2)))
r375: push(E1,E2,nocalls()) -> calls(E1,stack(E2,empty()),nocalls())
r376: push(E1,E2,calls(E3,S1,CS1)) -> push1(E1,E2,E3,S1,CS1,eqt(E1,E3))
r377: push1(E1,E2,E3,S1,CS1,T()) -> calls(E3,pushs(E2,S1),CS1)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      eqs#_A(x1,x2) = ((1,0,0),(0,0,0),(1,0,0)) x1 + ((1,0,0),(0,0,0),(1,0,0)) x2
      stack_A(x1,x2) = ((1,0,0),(0,1,0),(1,1,1)) x1 + ((1,0,0),(0,0,0),(1,1,0)) x2 + (1,1,1)

The next rules are strictly ordered:

  p1

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: eqt#(pid(N1),pid(N2)) -> eqt#(N1,N2)
p2: eqt#(tuplenil(H1),tuplenil(H2)) -> eqt#(H1,H2)
p3: eqt#(tuple(H1,T1),tuple(H2,T2)) -> eqt#(T1,T2)
p4: eqt#(tuple(H1,T1),tuple(H2,T2)) -> eqt#(H1,H2)
p5: eqt#(cons(H1,T1),cons(H2,T2)) -> eqt#(T1,T2)
p6: eqt#(cons(H1,T1),cons(H2,T2)) -> eqt#(H1,H2)

and R consists of:

r1: or(T(),T()) -> T()
r2: or(F(),T()) -> T()
r3: or(T(),F()) -> T()
r4: or(F(),F()) -> F()
r5: and(T(),B) -> B
r6: and(B,T()) -> B
r7: and(F(),B) -> F()
r8: and(B,F()) -> F()
r9: imp(T(),B) -> B
r10: imp(F(),B) -> T()
r11: not(T()) -> F()
r12: not(F()) -> T()
r13: if(T(),B1,B2) -> B1
r14: if(F(),B1,B2) -> B2
r15: eq(T(),T()) -> T()
r16: eq(F(),F()) -> T()
r17: eq(T(),F()) -> F()
r18: eq(F(),T()) -> F()
r19: eqt(nil(),undefined()) -> F()
r20: eqt(nil(),pid(N2)) -> F()
r21: eqt(nil(),int(N2)) -> F()
r22: eqt(nil(),cons(H2,T2)) -> F()
r23: eqt(nil(),tuple(H2,T2)) -> F()
r24: eqt(nil(),tuplenil(H2)) -> F()
r25: eqt(a(),nil()) -> F()
r26: eqt(a(),a()) -> T()
r27: eqt(a(),excl()) -> F()
r28: eqt(a(),false()) -> F()
r29: eqt(a(),lock()) -> F()
r30: eqt(a(),locker()) -> F()
r31: eqt(a(),mcrlrecord()) -> F()
r32: eqt(a(),ok()) -> F()
r33: eqt(a(),pending()) -> F()
r34: eqt(a(),release()) -> F()
r35: eqt(a(),request()) -> F()
r36: eqt(a(),resource()) -> F()
r37: eqt(a(),tag()) -> F()
r38: eqt(a(),true()) -> F()
r39: eqt(a(),undefined()) -> F()
r40: eqt(a(),pid(N2)) -> F()
r41: eqt(a(),int(N2)) -> F()
r42: eqt(a(),cons(H2,T2)) -> F()
r43: eqt(a(),tuple(H2,T2)) -> F()
r44: eqt(a(),tuplenil(H2)) -> F()
r45: eqt(excl(),nil()) -> F()
r46: eqt(excl(),a()) -> F()
r47: eqt(excl(),excl()) -> T()
r48: eqt(excl(),false()) -> F()
r49: eqt(excl(),lock()) -> F()
r50: eqt(excl(),locker()) -> F()
r51: eqt(excl(),mcrlrecord()) -> F()
r52: eqt(excl(),ok()) -> F()
r53: eqt(excl(),pending()) -> F()
r54: eqt(excl(),release()) -> F()
r55: eqt(excl(),request()) -> F()
r56: eqt(excl(),resource()) -> F()
r57: eqt(excl(),tag()) -> F()
r58: eqt(excl(),true()) -> F()
r59: eqt(excl(),undefined()) -> F()
r60: eqt(excl(),pid(N2)) -> F()
r61: eqt(excl(),eqt(false(),int(N2))) -> F()
r62: eqt(false(),cons(H2,T2)) -> F()
r63: eqt(false(),tuple(H2,T2)) -> F()
r64: eqt(false(),tuplenil(H2)) -> F()
r65: eqt(lock(),nil()) -> F()
r66: eqt(lock(),a()) -> F()
r67: eqt(lock(),excl()) -> F()
r68: eqt(lock(),false()) -> F()
r69: eqt(lock(),lock()) -> T()
r70: eqt(lock(),locker()) -> F()
r71: eqt(lock(),mcrlrecord()) -> F()
r72: eqt(lock(),ok()) -> F()
r73: eqt(lock(),pending()) -> F()
r74: eqt(lock(),release()) -> F()
r75: eqt(lock(),request()) -> F()
r76: eqt(lock(),resource()) -> F()
r77: eqt(lock(),tag()) -> F()
r78: eqt(lock(),true()) -> F()
r79: eqt(lock(),undefined()) -> F()
r80: eqt(lock(),pid(N2)) -> F()
r81: eqt(lock(),int(N2)) -> F()
r82: eqt(lock(),cons(H2,T2)) -> F()
r83: eqt(lock(),tuple(H2,T2)) -> F()
r84: eqt(lock(),tuplenil(H2)) -> F()
r85: eqt(locker(),nil()) -> F()
r86: eqt(locker(),a()) -> F()
r87: eqt(locker(),excl()) -> F()
r88: eqt(locker(),false()) -> F()
r89: eqt(locker(),lock()) -> F()
r90: eqt(locker(),locker()) -> T()
r91: eqt(locker(),mcrlrecord()) -> F()
r92: eqt(locker(),ok()) -> F()
r93: eqt(locker(),pending()) -> F()
r94: eqt(locker(),release()) -> F()
r95: eqt(locker(),request()) -> F()
r96: eqt(locker(),resource()) -> F()
r97: eqt(locker(),tag()) -> F()
r98: eqt(locker(),true()) -> F()
r99: eqt(locker(),undefined()) -> F()
r100: eqt(locker(),pid(N2)) -> F()
r101: eqt(locker(),int(N2)) -> F()
r102: eqt(locker(),cons(H2,T2)) -> F()
r103: eqt(locker(),tuple(H2,T2)) -> F()
r104: eqt(locker(),tuplenil(H2)) -> F()
r105: eqt(mcrlrecord(),nil()) -> F()
r106: eqt(mcrlrecord(),a()) -> F()
r107: eqt(mcrlrecord(),excl()) -> F()
r108: eqt(mcrlrecord(),false()) -> F()
r109: eqt(mcrlrecord(),lock()) -> F()
r110: eqt(mcrlrecord(),locker()) -> F()
r111: eqt(mcrlrecord(),mcrlrecord()) -> T()
r112: eqt(mcrlrecord(),ok()) -> F()
r113: eqt(mcrlrecord(),pending()) -> F()
r114: eqt(mcrlrecord(),release()) -> F()
r115: eqt(mcrlrecord(),request()) -> F()
r116: eqt(mcrlrecord(),resource()) -> F()
r117: eqt(ok(),resource()) -> F()
r118: eqt(ok(),tag()) -> F()
r119: eqt(ok(),true()) -> F()
r120: eqt(ok(),undefined()) -> F()
r121: eqt(ok(),pid(N2)) -> F()
r122: eqt(ok(),int(N2)) -> F()
r123: eqt(ok(),cons(H2,T2)) -> F()
r124: eqt(ok(),tuple(H2,T2)) -> F()
r125: eqt(ok(),tuplenil(H2)) -> F()
r126: eqt(pending(),nil()) -> F()
r127: eqt(pending(),a()) -> F()
r128: eqt(pending(),excl()) -> F()
r129: eqt(pending(),false()) -> F()
r130: eqt(pending(),lock()) -> F()
r131: eqt(pending(),locker()) -> F()
r132: eqt(pending(),mcrlrecord()) -> F()
r133: eqt(pending(),ok()) -> F()
r134: eqt(pending(),pending()) -> T()
r135: eqt(pending(),release()) -> F()
r136: eqt(pending(),request()) -> F()
r137: eqt(pending(),resource()) -> F()
r138: eqt(pending(),tag()) -> F()
r139: eqt(pending(),true()) -> F()
r140: eqt(pending(),undefined()) -> F()
r141: eqt(pending(),pid(N2)) -> F()
r142: eqt(pending(),int(N2)) -> F()
r143: eqt(pending(),cons(H2,T2)) -> F()
r144: eqt(pending(),tuple(H2,T2)) -> F()
r145: eqt(pending(),tuplenil(H2)) -> F()
r146: eqt(release(),nil()) -> F()
r147: eqt(release(),a()) -> F()
r148: eqt(release(),excl()) -> F()
r149: eqt(release(),false()) -> F()
r150: eqt(release(),lock()) -> F()
r151: eqt(release(),locker()) -> F()
r152: eqt(release(),mcrlrecord()) -> F()
r153: eqt(release(),ok()) -> F()
r154: eqt(request(),mcrlrecord()) -> F()
r155: eqt(request(),ok()) -> F()
r156: eqt(request(),pending()) -> F()
r157: eqt(request(),release()) -> F()
r158: eqt(request(),request()) -> T()
r159: eqt(request(),resource()) -> F()
r160: eqt(request(),tag()) -> F()
r161: eqt(request(),true()) -> F()
r162: eqt(request(),undefined()) -> F()
r163: eqt(request(),pid(N2)) -> F()
r164: eqt(request(),int(N2)) -> F()
r165: eqt(request(),cons(H2,T2)) -> F()
r166: eqt(request(),tuple(H2,T2)) -> F()
r167: eqt(request(),tuplenil(H2)) -> F()
r168: eqt(resource(),nil()) -> F()
r169: eqt(resource(),a()) -> F()
r170: eqt(resource(),excl()) -> F()
r171: eqt(resource(),false()) -> F()
r172: eqt(resource(),lock()) -> F()
r173: eqt(resource(),locker()) -> F()
r174: eqt(resource(),mcrlrecord()) -> F()
r175: eqt(resource(),ok()) -> F()
r176: eqt(resource(),pending()) -> F()
r177: eqt(resource(),release()) -> F()
r178: eqt(resource(),request()) -> F()
r179: eqt(resource(),resource()) -> T()
r180: eqt(resource(),tag()) -> F()
r181: eqt(resource(),true()) -> F()
r182: eqt(resource(),undefined()) -> F()
r183: eqt(resource(),pid(N2)) -> F()
r184: eqt(resource(),int(N2)) -> F()
r185: eqt(resource(),cons(H2,T2)) -> F()
r186: eqt(resource(),tuple(H2,T2)) -> F()
r187: eqt(resource(),tuplenil(H2)) -> F()
r188: eqt(tag(),nil()) -> F()
r189: eqt(tag(),a()) -> F()
r190: eqt(tag(),excl()) -> F()
r191: eqt(tag(),false()) -> F()
r192: eqt(tag(),lock()) -> F()
r193: eqt(tag(),locker()) -> F()
r194: eqt(tag(),mcrlrecord()) -> F()
r195: eqt(tag(),ok()) -> F()
r196: eqt(tag(),pending()) -> F()
r197: eqt(tag(),release()) -> F()
r198: eqt(tag(),request()) -> F()
r199: eqt(tag(),resource()) -> F()
r200: eqt(tag(),tag()) -> T()
r201: eqt(tag(),true()) -> F()
r202: eqt(tag(),undefined()) -> F()
r203: eqt(tag(),pid(N2)) -> F()
r204: eqt(tag(),int(N2)) -> F()
r205: eqt(tag(),cons(H2,T2)) -> F()
r206: eqt(tag(),tuple(H2,T2)) -> F()
r207: eqt(tag(),tuplenil(H2)) -> F()
r208: eqt(true(),nil()) -> F()
r209: eqt(true(),a()) -> F()
r210: eqt(true(),excl()) -> F()
r211: eqt(true(),false()) -> F()
r212: eqt(true(),lock()) -> F()
r213: eqt(true(),locker()) -> F()
r214: eqt(true(),mcrlrecord()) -> F()
r215: eqt(true(),ok()) -> F()
r216: eqt(true(),pending()) -> F()
r217: eqt(true(),release()) -> F()
r218: eqt(true(),request()) -> F()
r219: eqt(true(),resource()) -> F()
r220: eqt(true(),tag()) -> F()
r221: eqt(true(),true()) -> T()
r222: eqt(true(),undefined()) -> F()
r223: eqt(true(),pid(N2)) -> F()
r224: eqt(true(),int(N2)) -> F()
r225: eqt(true(),cons(H2,T2)) -> F()
r226: eqt(true(),tuple(H2,T2)) -> F()
r227: eqt(true(),tuplenil(H2)) -> F()
r228: eqt(undefined(),nil()) -> F()
r229: eqt(undefined(),a()) -> F()
r230: eqt(undefined(),tuplenil(H2)) -> F()
r231: eqt(pid(N1),nil()) -> F()
r232: eqt(pid(N1),a()) -> F()
r233: eqt(pid(N1),excl()) -> F()
r234: eqt(pid(N1),false()) -> F()
r235: eqt(pid(N1),lock()) -> F()
r236: eqt(pid(N1),locker()) -> F()
r237: eqt(pid(N1),mcrlrecord()) -> F()
r238: eqt(pid(N1),ok()) -> F()
r239: eqt(pid(N1),pending()) -> F()
r240: eqt(pid(N1),release()) -> F()
r241: eqt(pid(N1),request()) -> F()
r242: eqt(pid(N1),resource()) -> F()
r243: eqt(pid(N1),tag()) -> F()
r244: eqt(pid(N1),true()) -> F()
r245: eqt(pid(N1),undefined()) -> F()
r246: eqt(pid(N1),pid(N2)) -> eqt(N1,N2)
r247: eqt(pid(N1),int(N2)) -> F()
r248: eqt(pid(N1),cons(H2,T2)) -> F()
r249: eqt(pid(N1),tuple(H2,T2)) -> F()
r250: eqt(pid(N1),tuplenil(H2)) -> F()
r251: eqt(int(N1),nil()) -> F()
r252: eqt(int(N1),a()) -> F()
r253: eqt(int(N1),excl()) -> F()
r254: eqt(int(N1),false()) -> F()
r255: eqt(int(N1),lock()) -> F()
r256: eqt(int(N1),locker()) -> F()
r257: eqt(int(N1),mcrlrecord()) -> F()
r258: eqt(int(N1),ok()) -> F()
r259: eqt(int(N1),pending()) -> F()
r260: eqt(int(N1),release()) -> F()
r261: eqt(int(N1),request()) -> F()
r262: eqt(int(N1),resource()) -> F()
r263: eqt(int(N1),tag()) -> F()
r264: eqt(int(N1),true()) -> F()
r265: eqt(int(N1),undefined()) -> F()
r266: eqt(cons(H1,T1),resource()) -> F()
r267: eqt(cons(H1,T1),tag()) -> F()
r268: eqt(cons(H1,T1),true()) -> F()
r269: eqt(cons(H1,T1),undefined()) -> F()
r270: eqt(cons(H1,T1),pid(N2)) -> F()
r271: eqt(cons(H1,T1),int(N2)) -> F()
r272: eqt(cons(H1,T1),cons(H2,T2)) -> and(eqt(H1,H2),eqt(T1,T2))
r273: eqt(cons(H1,T1),tuple(H2,T2)) -> F()
r274: eqt(cons(H1,T1),tuplenil(H2)) -> F()
r275: eqt(tuple(H1,T1),nil()) -> F()
r276: eqt(tuple(H1,T1),a()) -> F()
r277: eqt(tuple(H1,T1),excl()) -> F()
r278: eqt(tuple(H1,T1),false()) -> F()
r279: eqt(tuple(H1,T1),lock()) -> F()
r280: eqt(tuple(H1,T1),locker()) -> F()
r281: eqt(tuple(H1,T1),mcrlrecord()) -> F()
r282: eqt(tuple(H1,T1),ok()) -> F()
r283: eqt(tuple(H1,T1),pending()) -> F()
r284: eqt(tuple(H1,T1),release()) -> F()
r285: eqt(tuple(H1,T1),request()) -> F()
r286: eqt(tuple(H1,T1),resource()) -> F()
r287: eqt(tuple(H1,T1),tag()) -> F()
r288: eqt(tuple(H1,T1),true()) -> F()
r289: eqt(tuple(H1,T1),undefined()) -> F()
r290: eqt(tuple(H1,T1),pid(N2)) -> F()
r291: eqt(tuple(H1,T1),int(N2)) -> F()
r292: eqt(tuple(H1,T1),cons(H2,T2)) -> F()
r293: eqt(tuple(H1,T1),tuple(H2,T2)) -> and(eqt(H1,H2),eqt(T1,T2))
r294: eqt(tuple(H1,T1),tuplenil(H2)) -> F()
r295: eqt(tuplenil(H1),nil()) -> F()
r296: eqt(tuplenil(H1),a()) -> F()
r297: eqt(tuplenil(H1),excl()) -> F()
r298: eqt(tuplenil(H1),false()) -> F()
r299: eqt(tuplenil(H1),lock()) -> F()
r300: eqt(tuplenil(H1),locker()) -> F()
r301: eqt(tuplenil(H1),mcrlrecord()) -> F()
r302: eqt(tuplenil(H1),ok()) -> F()
r303: eqt(tuplenil(H1),pending()) -> F()
r304: eqt(tuplenil(H1),release()) -> F()
r305: eqt(tuplenil(H1),request()) -> F()
r306: eqt(tuplenil(H1),resource()) -> F()
r307: eqt(tuplenil(H1),tag()) -> F()
r308: eqt(tuplenil(H1),true()) -> F()
r309: eqt(tuplenil(H1),undefined()) -> F()
r310: eqt(tuplenil(H1),pid(N2)) -> F()
r311: eqt(tuplenil(H1),int(N2)) -> F()
r312: eqt(tuplenil(H1),cons(H2,T2)) -> F()
r313: eqt(tuplenil(H1),tuple(H2,T2)) -> F()
r314: eqt(tuplenil(H1),tuplenil(H2)) -> eqt(H1,H2)
r315: element(int(s(|0|())),tuplenil(T1)) -> T1
r316: element(int(s(|0|())),tuple(T1,T2)) -> T1
r317: element(int(s(s(N1))),tuple(T1,T2)) -> element(int(s(N1)),T2)
r318: record_new(lock()) -> tuple(mcrlrecord(),tuple(lock(),tuple(undefined(),tuple(nil(),tuplenil(nil())))))
r319: record_extract(tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(F2))))),lock(),resource()) -> tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(F2)))))
r320: 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)))))
r321: record_updates(Record,Name,nil()) -> Record
r322: record_updates(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields)) -> record_updates(record_update(Record,Name,Field,NewF),Name,Fields)
r323: locker2_map_promote_pending(nil(),Pending) -> nil()
r324: locker2_map_promote_pending(cons(Lock,Locks),Pending) -> cons(locker2_promote_pending(Lock,Pending),locker2_map_promote_pending(Locks,Pending))
r325: locker2_map_claim_lock(nil(),Resources,Client) -> nil()
r326: locker2_map_claim_lock(cons(Lock,Locks),Resources,Client) -> cons(locker2_claim_lock(Lock,Resources,Client),locker2_map_claim_lock(Locks,Resources,Client))
r327: locker2_map_add_pending(nil(),Resources,Client) -> nil()
r328: locker2_promote_pending(Lock,Client) -> case0(Client,Lock,record_extract(Lock,lock(),pending()))
r329: case0(Client,Lock,cons(Client,Pendings)) -> record_updates(Lock,lock(),cons(tuple(excl(),tuplenil(Client)),cons(tuple(pending(),tuplenil(Pendings)),nil())))
r330: case0(Client,Lock,MCRLFree0) -> Lock
r331: locker2_remove_pending(Lock,Client) -> record_updates(Lock,lock(),cons(tuple(pending(),tuplenil(subtract(record_extract(Lock,lock(),pending()),cons(Client,nil())))),nil()))
r332: locker2_add_pending(Lock,Resources,Client) -> case1(Client,Resources,Lock,member(record_extract(Lock,lock(),resource()),Resources))
r333: case1(Client,Resources,Lock,true()) -> record_updates(Lock,lock(),cons(tuple(pending(),tuplenil(append(record_extract(Lock,lock(),pending()),cons(Client,nil())))),nil()))
r334: case1(Client,Resources,Lock,false()) -> Lock
r335: locker2_release_lock(Lock,Client) -> case2(Client,Lock,gen_modtageq(Client,record_extract(Lock,lock(),excl())))
r336: case2(Client,Lock,true()) -> record_updates(Lock,lock(),cons(tuple(excllock(),excl()),nil()))
r337: case4(Client,Lock,MCRLFree1) -> false()
r338: locker2_obtainables(nil(),Client) -> true()
r339: locker2_obtainables(cons(Lock,Locks),Client) -> case5(Client,Locks,Lock,member(Client,record_extract(Lock,lock(),pending())))
r340: case5(Client,Locks,Lock,true()) -> andt(locker2_obtainable(Lock,Client),locker2_obtainables(Locks,Client))
r341: case5(Client,Locks,Lock,false()) -> locker2_obtainables(Locks,Client)
r342: locker2_check_available(Resource,nil()) -> false()
r343: locker2_check_available(Resource,cons(Lock,Locks)) -> case6(Locks,Lock,Resource,equal(Resource,record_extract(Lock,lock(),resource())))
r344: case6(Locks,Lock,Resource,true()) -> andt(equal(record_extract(Lock,lock(),excl()),nil()),equal(record_extract(Lock,lock(),pending()),nil()))
r345: case6(Locks,Lock,Resource,false()) -> locker2_check_available(Resource,Locks)
r346: locker2_check_availables(nil(),Locks) -> true()
r347: locker2_check_availables(cons(Resource,Resources),Locks) -> andt(locker2_check_available(Resource,Locks),locker2_check_availables(Resources,Locks))
r348: locker2_adduniq(nil(),List) -> List
r349: append(cons(Head,Tail),List) -> cons(Head,append(Tail,List))
r350: subtract(List,nil()) -> List
r351: subtract(List,cons(Head,Tail)) -> subtract(delete(Head,List),Tail)
r352: delete(E,nil()) -> nil()
r353: delete(E,cons(Head,Tail)) -> case8(Tail,Head,E,equal(E,Head))
r354: case8(Tail,Head,E,true()) -> Tail
r355: case8(Tail,Head,E,false()) -> cons(Head,delete(E,Tail))
r356: gen_tag(Pid) -> tuple(Pid,tuplenil(tag()))
r357: gen_modtageq(Client1,Client2) -> equal(Client1,Client2)
r358: member(E,nil()) -> false()
r359: member(E,cons(Head,Tail)) -> case9(Tail,Head,E,equal(E,Head))
r360: case9(Tail,Head,E,true()) -> true()
r361: case9(Tail,Head,E,false()) -> member(E,Tail)
r362: eqs(empty(),empty()) -> T()
r363: eqs(empty(),stack(E2,S2)) -> F()
r364: eqs(stack(E1,S1),empty()) -> F()
r365: eqs(stack(E1,S1),stack(E2,S2)) -> and(eqt(E1,E2),eqs(S1,S2))
r366: pushs(E1,S1) -> stack(E1,S1)
r367: pops(stack(E1,S1)) -> S1
r368: tops(stack(E1,S1)) -> E1
r369: istops(E1,empty()) -> F()
r370: istops(E1,stack(E2,S1)) -> eqt(E1,E2)
r371: eqc(nocalls(),nocalls()) -> T()
r372: eqc(nocalls(),calls(E2,S2,CS2)) -> F()
r373: eqc(calls(E1,S1,CS1),nocalls()) -> F()
r374: eqc(calls(E1,S1,CS1),calls(E2,S2,CS2)) -> and(eqt(E1,E2),and(eqs(S1,S2),eqc(CS1,CS2)))
r375: push(E1,E2,nocalls()) -> calls(E1,stack(E2,empty()),nocalls())
r376: push(E1,E2,calls(E3,S1,CS1)) -> push1(E1,E2,E3,S1,CS1,eqt(E1,E3))
r377: push1(E1,E2,E3,S1,CS1,T()) -> calls(E3,pushs(E2,S1),CS1)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      eqt#_A(x1,x2) = ((1,0,0),(0,1,0),(1,1,1)) x1 + ((1,0,0),(1,1,0),(1,1,1)) x2
      pid_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)
      tuplenil_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)
      tuple_A(x1,x2) = ((1,0,0),(1,1,0),(1,1,1)) x1 + ((1,0,0),(1,1,0),(1,1,1)) x2 + (1,1,1)
      cons_A(x1,x2) = ((1,0,0),(1,1,0),(1,1,1)) x1 + ((1,0,0),(1,1,0),(1,1,1)) x2 + (1,1,1)

The next rules are strictly ordered:

  p1, p2, p3, p4, p5, p6
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68, r69, r70, r71, r72, r73, r74, r75, r76, r77, r78, r79, r80, r81, r82, r83, r84, r85, r86, r87, r88, r89, r90, r91, r92, r93, r94, r95, r96, r97, r98, r99, r100, r101, r102, r103, r104, r105, r106, r107, r108, r109, r110, r111, r112, r113, r114, r115, r116, r117, r118, r119, r120, r121, r122, r123, r124, r125, r126, r127, r128, r129, r130, r131, r132, r133, r134, r135, r136, r137, r138, r139, r140, r141, r142, r143, r144, r145, r146, r147, r148, r149, r150, r151, r152, r153, r154, r155, r156, r157, r158, r159, r160, r161, r162, r163, r164, r165, r166, r167, r168, r169, r170, r171, r172, r173, r174, r175, r176, r177, r178, r179, r180, r181, r182, r183, r184, r185, r186, r187, r188, r189, r190, r191, r192, r193, r194, r195, r196, r197, r198, r199, r200, r201, r202, r203, r204, r205, r206, r207, r208, r209, r210, r211, r212, r213, r214, r215, r216, r217, r218, r219, r220, r221, r222, r223, r224, r225, r226, r227, r228, r229, r230, r231, r232, r233, r234, r235, r236, r237, r238, r239, r240, r241, r242, r243, r244, r245, r246, r247, r248, r249, r250, r251, r252, r253, r254, r255, r256, r257, r258, r259, r260, r261, r262, r263, r264, r265, r266, r267, r268, r269, r270, r271, r272, r273, r274, r275, r276, r277, r278, r279, r280, r281, r282, r283, r284, r285, r286, r287, r288, r289, r290, r291, r292, r293, r294, r295, r296, r297, r298, r299, r300, r301, r302, r303, r304, r305, r306, r307, r308, r309, r310, r311, r312, r313, r314, r315, r316, r317, r318, r319, r320, r321, r322, r323, r324, r325, r326, r327, r328, r329, r330, r331, r332, r333, r334, r335, r336, r337, r338, r339, r340, r341, r342, r343, r344, r345, r346, r347, r348, r349, r350, r351, r352, r353, r354, r355, r356, r357, r358, r359, r360, r361, r362, r363, r364, r365, r366, r367, r368, r369, r370, r371, r372, r373, r374, r375, r376, r377

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: element#(int(s(s(N1))),tuple(T1,T2)) -> element#(int(s(N1)),T2)

and R consists of:

r1: or(T(),T()) -> T()
r2: or(F(),T()) -> T()
r3: or(T(),F()) -> T()
r4: or(F(),F()) -> F()
r5: and(T(),B) -> B
r6: and(B,T()) -> B
r7: and(F(),B) -> F()
r8: and(B,F()) -> F()
r9: imp(T(),B) -> B
r10: imp(F(),B) -> T()
r11: not(T()) -> F()
r12: not(F()) -> T()
r13: if(T(),B1,B2) -> B1
r14: if(F(),B1,B2) -> B2
r15: eq(T(),T()) -> T()
r16: eq(F(),F()) -> T()
r17: eq(T(),F()) -> F()
r18: eq(F(),T()) -> F()
r19: eqt(nil(),undefined()) -> F()
r20: eqt(nil(),pid(N2)) -> F()
r21: eqt(nil(),int(N2)) -> F()
r22: eqt(nil(),cons(H2,T2)) -> F()
r23: eqt(nil(),tuple(H2,T2)) -> F()
r24: eqt(nil(),tuplenil(H2)) -> F()
r25: eqt(a(),nil()) -> F()
r26: eqt(a(),a()) -> T()
r27: eqt(a(),excl()) -> F()
r28: eqt(a(),false()) -> F()
r29: eqt(a(),lock()) -> F()
r30: eqt(a(),locker()) -> F()
r31: eqt(a(),mcrlrecord()) -> F()
r32: eqt(a(),ok()) -> F()
r33: eqt(a(),pending()) -> F()
r34: eqt(a(),release()) -> F()
r35: eqt(a(),request()) -> F()
r36: eqt(a(),resource()) -> F()
r37: eqt(a(),tag()) -> F()
r38: eqt(a(),true()) -> F()
r39: eqt(a(),undefined()) -> F()
r40: eqt(a(),pid(N2)) -> F()
r41: eqt(a(),int(N2)) -> F()
r42: eqt(a(),cons(H2,T2)) -> F()
r43: eqt(a(),tuple(H2,T2)) -> F()
r44: eqt(a(),tuplenil(H2)) -> F()
r45: eqt(excl(),nil()) -> F()
r46: eqt(excl(),a()) -> F()
r47: eqt(excl(),excl()) -> T()
r48: eqt(excl(),false()) -> F()
r49: eqt(excl(),lock()) -> F()
r50: eqt(excl(),locker()) -> F()
r51: eqt(excl(),mcrlrecord()) -> F()
r52: eqt(excl(),ok()) -> F()
r53: eqt(excl(),pending()) -> F()
r54: eqt(excl(),release()) -> F()
r55: eqt(excl(),request()) -> F()
r56: eqt(excl(),resource()) -> F()
r57: eqt(excl(),tag()) -> F()
r58: eqt(excl(),true()) -> F()
r59: eqt(excl(),undefined()) -> F()
r60: eqt(excl(),pid(N2)) -> F()
r61: eqt(excl(),eqt(false(),int(N2))) -> F()
r62: eqt(false(),cons(H2,T2)) -> F()
r63: eqt(false(),tuple(H2,T2)) -> F()
r64: eqt(false(),tuplenil(H2)) -> F()
r65: eqt(lock(),nil()) -> F()
r66: eqt(lock(),a()) -> F()
r67: eqt(lock(),excl()) -> F()
r68: eqt(lock(),false()) -> F()
r69: eqt(lock(),lock()) -> T()
r70: eqt(lock(),locker()) -> F()
r71: eqt(lock(),mcrlrecord()) -> F()
r72: eqt(lock(),ok()) -> F()
r73: eqt(lock(),pending()) -> F()
r74: eqt(lock(),release()) -> F()
r75: eqt(lock(),request()) -> F()
r76: eqt(lock(),resource()) -> F()
r77: eqt(lock(),tag()) -> F()
r78: eqt(lock(),true()) -> F()
r79: eqt(lock(),undefined()) -> F()
r80: eqt(lock(),pid(N2)) -> F()
r81: eqt(lock(),int(N2)) -> F()
r82: eqt(lock(),cons(H2,T2)) -> F()
r83: eqt(lock(),tuple(H2,T2)) -> F()
r84: eqt(lock(),tuplenil(H2)) -> F()
r85: eqt(locker(),nil()) -> F()
r86: eqt(locker(),a()) -> F()
r87: eqt(locker(),excl()) -> F()
r88: eqt(locker(),false()) -> F()
r89: eqt(locker(),lock()) -> F()
r90: eqt(locker(),locker()) -> T()
r91: eqt(locker(),mcrlrecord()) -> F()
r92: eqt(locker(),ok()) -> F()
r93: eqt(locker(),pending()) -> F()
r94: eqt(locker(),release()) -> F()
r95: eqt(locker(),request()) -> F()
r96: eqt(locker(),resource()) -> F()
r97: eqt(locker(),tag()) -> F()
r98: eqt(locker(),true()) -> F()
r99: eqt(locker(),undefined()) -> F()
r100: eqt(locker(),pid(N2)) -> F()
r101: eqt(locker(),int(N2)) -> F()
r102: eqt(locker(),cons(H2,T2)) -> F()
r103: eqt(locker(),tuple(H2,T2)) -> F()
r104: eqt(locker(),tuplenil(H2)) -> F()
r105: eqt(mcrlrecord(),nil()) -> F()
r106: eqt(mcrlrecord(),a()) -> F()
r107: eqt(mcrlrecord(),excl()) -> F()
r108: eqt(mcrlrecord(),false()) -> F()
r109: eqt(mcrlrecord(),lock()) -> F()
r110: eqt(mcrlrecord(),locker()) -> F()
r111: eqt(mcrlrecord(),mcrlrecord()) -> T()
r112: eqt(mcrlrecord(),ok()) -> F()
r113: eqt(mcrlrecord(),pending()) -> F()
r114: eqt(mcrlrecord(),release()) -> F()
r115: eqt(mcrlrecord(),request()) -> F()
r116: eqt(mcrlrecord(),resource()) -> F()
r117: eqt(ok(),resource()) -> F()
r118: eqt(ok(),tag()) -> F()
r119: eqt(ok(),true()) -> F()
r120: eqt(ok(),undefined()) -> F()
r121: eqt(ok(),pid(N2)) -> F()
r122: eqt(ok(),int(N2)) -> F()
r123: eqt(ok(),cons(H2,T2)) -> F()
r124: eqt(ok(),tuple(H2,T2)) -> F()
r125: eqt(ok(),tuplenil(H2)) -> F()
r126: eqt(pending(),nil()) -> F()
r127: eqt(pending(),a()) -> F()
r128: eqt(pending(),excl()) -> F()
r129: eqt(pending(),false()) -> F()
r130: eqt(pending(),lock()) -> F()
r131: eqt(pending(),locker()) -> F()
r132: eqt(pending(),mcrlrecord()) -> F()
r133: eqt(pending(),ok()) -> F()
r134: eqt(pending(),pending()) -> T()
r135: eqt(pending(),release()) -> F()
r136: eqt(pending(),request()) -> F()
r137: eqt(pending(),resource()) -> F()
r138: eqt(pending(),tag()) -> F()
r139: eqt(pending(),true()) -> F()
r140: eqt(pending(),undefined()) -> F()
r141: eqt(pending(),pid(N2)) -> F()
r142: eqt(pending(),int(N2)) -> F()
r143: eqt(pending(),cons(H2,T2)) -> F()
r144: eqt(pending(),tuple(H2,T2)) -> F()
r145: eqt(pending(),tuplenil(H2)) -> F()
r146: eqt(release(),nil()) -> F()
r147: eqt(release(),a()) -> F()
r148: eqt(release(),excl()) -> F()
r149: eqt(release(),false()) -> F()
r150: eqt(release(),lock()) -> F()
r151: eqt(release(),locker()) -> F()
r152: eqt(release(),mcrlrecord()) -> F()
r153: eqt(release(),ok()) -> F()
r154: eqt(request(),mcrlrecord()) -> F()
r155: eqt(request(),ok()) -> F()
r156: eqt(request(),pending()) -> F()
r157: eqt(request(),release()) -> F()
r158: eqt(request(),request()) -> T()
r159: eqt(request(),resource()) -> F()
r160: eqt(request(),tag()) -> F()
r161: eqt(request(),true()) -> F()
r162: eqt(request(),undefined()) -> F()
r163: eqt(request(),pid(N2)) -> F()
r164: eqt(request(),int(N2)) -> F()
r165: eqt(request(),cons(H2,T2)) -> F()
r166: eqt(request(),tuple(H2,T2)) -> F()
r167: eqt(request(),tuplenil(H2)) -> F()
r168: eqt(resource(),nil()) -> F()
r169: eqt(resource(),a()) -> F()
r170: eqt(resource(),excl()) -> F()
r171: eqt(resource(),false()) -> F()
r172: eqt(resource(),lock()) -> F()
r173: eqt(resource(),locker()) -> F()
r174: eqt(resource(),mcrlrecord()) -> F()
r175: eqt(resource(),ok()) -> F()
r176: eqt(resource(),pending()) -> F()
r177: eqt(resource(),release()) -> F()
r178: eqt(resource(),request()) -> F()
r179: eqt(resource(),resource()) -> T()
r180: eqt(resource(),tag()) -> F()
r181: eqt(resource(),true()) -> F()
r182: eqt(resource(),undefined()) -> F()
r183: eqt(resource(),pid(N2)) -> F()
r184: eqt(resource(),int(N2)) -> F()
r185: eqt(resource(),cons(H2,T2)) -> F()
r186: eqt(resource(),tuple(H2,T2)) -> F()
r187: eqt(resource(),tuplenil(H2)) -> F()
r188: eqt(tag(),nil()) -> F()
r189: eqt(tag(),a()) -> F()
r190: eqt(tag(),excl()) -> F()
r191: eqt(tag(),false()) -> F()
r192: eqt(tag(),lock()) -> F()
r193: eqt(tag(),locker()) -> F()
r194: eqt(tag(),mcrlrecord()) -> F()
r195: eqt(tag(),ok()) -> F()
r196: eqt(tag(),pending()) -> F()
r197: eqt(tag(),release()) -> F()
r198: eqt(tag(),request()) -> F()
r199: eqt(tag(),resource()) -> F()
r200: eqt(tag(),tag()) -> T()
r201: eqt(tag(),true()) -> F()
r202: eqt(tag(),undefined()) -> F()
r203: eqt(tag(),pid(N2)) -> F()
r204: eqt(tag(),int(N2)) -> F()
r205: eqt(tag(),cons(H2,T2)) -> F()
r206: eqt(tag(),tuple(H2,T2)) -> F()
r207: eqt(tag(),tuplenil(H2)) -> F()
r208: eqt(true(),nil()) -> F()
r209: eqt(true(),a()) -> F()
r210: eqt(true(),excl()) -> F()
r211: eqt(true(),false()) -> F()
r212: eqt(true(),lock()) -> F()
r213: eqt(true(),locker()) -> F()
r214: eqt(true(),mcrlrecord()) -> F()
r215: eqt(true(),ok()) -> F()
r216: eqt(true(),pending()) -> F()
r217: eqt(true(),release()) -> F()
r218: eqt(true(),request()) -> F()
r219: eqt(true(),resource()) -> F()
r220: eqt(true(),tag()) -> F()
r221: eqt(true(),true()) -> T()
r222: eqt(true(),undefined()) -> F()
r223: eqt(true(),pid(N2)) -> F()
r224: eqt(true(),int(N2)) -> F()
r225: eqt(true(),cons(H2,T2)) -> F()
r226: eqt(true(),tuple(H2,T2)) -> F()
r227: eqt(true(),tuplenil(H2)) -> F()
r228: eqt(undefined(),nil()) -> F()
r229: eqt(undefined(),a()) -> F()
r230: eqt(undefined(),tuplenil(H2)) -> F()
r231: eqt(pid(N1),nil()) -> F()
r232: eqt(pid(N1),a()) -> F()
r233: eqt(pid(N1),excl()) -> F()
r234: eqt(pid(N1),false()) -> F()
r235: eqt(pid(N1),lock()) -> F()
r236: eqt(pid(N1),locker()) -> F()
r237: eqt(pid(N1),mcrlrecord()) -> F()
r238: eqt(pid(N1),ok()) -> F()
r239: eqt(pid(N1),pending()) -> F()
r240: eqt(pid(N1),release()) -> F()
r241: eqt(pid(N1),request()) -> F()
r242: eqt(pid(N1),resource()) -> F()
r243: eqt(pid(N1),tag()) -> F()
r244: eqt(pid(N1),true()) -> F()
r245: eqt(pid(N1),undefined()) -> F()
r246: eqt(pid(N1),pid(N2)) -> eqt(N1,N2)
r247: eqt(pid(N1),int(N2)) -> F()
r248: eqt(pid(N1),cons(H2,T2)) -> F()
r249: eqt(pid(N1),tuple(H2,T2)) -> F()
r250: eqt(pid(N1),tuplenil(H2)) -> F()
r251: eqt(int(N1),nil()) -> F()
r252: eqt(int(N1),a()) -> F()
r253: eqt(int(N1),excl()) -> F()
r254: eqt(int(N1),false()) -> F()
r255: eqt(int(N1),lock()) -> F()
r256: eqt(int(N1),locker()) -> F()
r257: eqt(int(N1),mcrlrecord()) -> F()
r258: eqt(int(N1),ok()) -> F()
r259: eqt(int(N1),pending()) -> F()
r260: eqt(int(N1),release()) -> F()
r261: eqt(int(N1),request()) -> F()
r262: eqt(int(N1),resource()) -> F()
r263: eqt(int(N1),tag()) -> F()
r264: eqt(int(N1),true()) -> F()
r265: eqt(int(N1),undefined()) -> F()
r266: eqt(cons(H1,T1),resource()) -> F()
r267: eqt(cons(H1,T1),tag()) -> F()
r268: eqt(cons(H1,T1),true()) -> F()
r269: eqt(cons(H1,T1),undefined()) -> F()
r270: eqt(cons(H1,T1),pid(N2)) -> F()
r271: eqt(cons(H1,T1),int(N2)) -> F()
r272: eqt(cons(H1,T1),cons(H2,T2)) -> and(eqt(H1,H2),eqt(T1,T2))
r273: eqt(cons(H1,T1),tuple(H2,T2)) -> F()
r274: eqt(cons(H1,T1),tuplenil(H2)) -> F()
r275: eqt(tuple(H1,T1),nil()) -> F()
r276: eqt(tuple(H1,T1),a()) -> F()
r277: eqt(tuple(H1,T1),excl()) -> F()
r278: eqt(tuple(H1,T1),false()) -> F()
r279: eqt(tuple(H1,T1),lock()) -> F()
r280: eqt(tuple(H1,T1),locker()) -> F()
r281: eqt(tuple(H1,T1),mcrlrecord()) -> F()
r282: eqt(tuple(H1,T1),ok()) -> F()
r283: eqt(tuple(H1,T1),pending()) -> F()
r284: eqt(tuple(H1,T1),release()) -> F()
r285: eqt(tuple(H1,T1),request()) -> F()
r286: eqt(tuple(H1,T1),resource()) -> F()
r287: eqt(tuple(H1,T1),tag()) -> F()
r288: eqt(tuple(H1,T1),true()) -> F()
r289: eqt(tuple(H1,T1),undefined()) -> F()
r290: eqt(tuple(H1,T1),pid(N2)) -> F()
r291: eqt(tuple(H1,T1),int(N2)) -> F()
r292: eqt(tuple(H1,T1),cons(H2,T2)) -> F()
r293: eqt(tuple(H1,T1),tuple(H2,T2)) -> and(eqt(H1,H2),eqt(T1,T2))
r294: eqt(tuple(H1,T1),tuplenil(H2)) -> F()
r295: eqt(tuplenil(H1),nil()) -> F()
r296: eqt(tuplenil(H1),a()) -> F()
r297: eqt(tuplenil(H1),excl()) -> F()
r298: eqt(tuplenil(H1),false()) -> F()
r299: eqt(tuplenil(H1),lock()) -> F()
r300: eqt(tuplenil(H1),locker()) -> F()
r301: eqt(tuplenil(H1),mcrlrecord()) -> F()
r302: eqt(tuplenil(H1),ok()) -> F()
r303: eqt(tuplenil(H1),pending()) -> F()
r304: eqt(tuplenil(H1),release()) -> F()
r305: eqt(tuplenil(H1),request()) -> F()
r306: eqt(tuplenil(H1),resource()) -> F()
r307: eqt(tuplenil(H1),tag()) -> F()
r308: eqt(tuplenil(H1),true()) -> F()
r309: eqt(tuplenil(H1),undefined()) -> F()
r310: eqt(tuplenil(H1),pid(N2)) -> F()
r311: eqt(tuplenil(H1),int(N2)) -> F()
r312: eqt(tuplenil(H1),cons(H2,T2)) -> F()
r313: eqt(tuplenil(H1),tuple(H2,T2)) -> F()
r314: eqt(tuplenil(H1),tuplenil(H2)) -> eqt(H1,H2)
r315: element(int(s(|0|())),tuplenil(T1)) -> T1
r316: element(int(s(|0|())),tuple(T1,T2)) -> T1
r317: element(int(s(s(N1))),tuple(T1,T2)) -> element(int(s(N1)),T2)
r318: record_new(lock()) -> tuple(mcrlrecord(),tuple(lock(),tuple(undefined(),tuple(nil(),tuplenil(nil())))))
r319: record_extract(tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(F2))))),lock(),resource()) -> tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(F2)))))
r320: 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)))))
r321: record_updates(Record,Name,nil()) -> Record
r322: record_updates(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields)) -> record_updates(record_update(Record,Name,Field,NewF),Name,Fields)
r323: locker2_map_promote_pending(nil(),Pending) -> nil()
r324: locker2_map_promote_pending(cons(Lock,Locks),Pending) -> cons(locker2_promote_pending(Lock,Pending),locker2_map_promote_pending(Locks,Pending))
r325: locker2_map_claim_lock(nil(),Resources,Client) -> nil()
r326: locker2_map_claim_lock(cons(Lock,Locks),Resources,Client) -> cons(locker2_claim_lock(Lock,Resources,Client),locker2_map_claim_lock(Locks,Resources,Client))
r327: locker2_map_add_pending(nil(),Resources,Client) -> nil()
r328: locker2_promote_pending(Lock,Client) -> case0(Client,Lock,record_extract(Lock,lock(),pending()))
r329: case0(Client,Lock,cons(Client,Pendings)) -> record_updates(Lock,lock(),cons(tuple(excl(),tuplenil(Client)),cons(tuple(pending(),tuplenil(Pendings)),nil())))
r330: case0(Client,Lock,MCRLFree0) -> Lock
r331: locker2_remove_pending(Lock,Client) -> record_updates(Lock,lock(),cons(tuple(pending(),tuplenil(subtract(record_extract(Lock,lock(),pending()),cons(Client,nil())))),nil()))
r332: locker2_add_pending(Lock,Resources,Client) -> case1(Client,Resources,Lock,member(record_extract(Lock,lock(),resource()),Resources))
r333: case1(Client,Resources,Lock,true()) -> record_updates(Lock,lock(),cons(tuple(pending(),tuplenil(append(record_extract(Lock,lock(),pending()),cons(Client,nil())))),nil()))
r334: case1(Client,Resources,Lock,false()) -> Lock
r335: locker2_release_lock(Lock,Client) -> case2(Client,Lock,gen_modtageq(Client,record_extract(Lock,lock(),excl())))
r336: case2(Client,Lock,true()) -> record_updates(Lock,lock(),cons(tuple(excllock(),excl()),nil()))
r337: case4(Client,Lock,MCRLFree1) -> false()
r338: locker2_obtainables(nil(),Client) -> true()
r339: locker2_obtainables(cons(Lock,Locks),Client) -> case5(Client,Locks,Lock,member(Client,record_extract(Lock,lock(),pending())))
r340: case5(Client,Locks,Lock,true()) -> andt(locker2_obtainable(Lock,Client),locker2_obtainables(Locks,Client))
r341: case5(Client,Locks,Lock,false()) -> locker2_obtainables(Locks,Client)
r342: locker2_check_available(Resource,nil()) -> false()
r343: locker2_check_available(Resource,cons(Lock,Locks)) -> case6(Locks,Lock,Resource,equal(Resource,record_extract(Lock,lock(),resource())))
r344: case6(Locks,Lock,Resource,true()) -> andt(equal(record_extract(Lock,lock(),excl()),nil()),equal(record_extract(Lock,lock(),pending()),nil()))
r345: case6(Locks,Lock,Resource,false()) -> locker2_check_available(Resource,Locks)
r346: locker2_check_availables(nil(),Locks) -> true()
r347: locker2_check_availables(cons(Resource,Resources),Locks) -> andt(locker2_check_available(Resource,Locks),locker2_check_availables(Resources,Locks))
r348: locker2_adduniq(nil(),List) -> List
r349: append(cons(Head,Tail),List) -> cons(Head,append(Tail,List))
r350: subtract(List,nil()) -> List
r351: subtract(List,cons(Head,Tail)) -> subtract(delete(Head,List),Tail)
r352: delete(E,nil()) -> nil()
r353: delete(E,cons(Head,Tail)) -> case8(Tail,Head,E,equal(E,Head))
r354: case8(Tail,Head,E,true()) -> Tail
r355: case8(Tail,Head,E,false()) -> cons(Head,delete(E,Tail))
r356: gen_tag(Pid) -> tuple(Pid,tuplenil(tag()))
r357: gen_modtageq(Client1,Client2) -> equal(Client1,Client2)
r358: member(E,nil()) -> false()
r359: member(E,cons(Head,Tail)) -> case9(Tail,Head,E,equal(E,Head))
r360: case9(Tail,Head,E,true()) -> true()
r361: case9(Tail,Head,E,false()) -> member(E,Tail)
r362: eqs(empty(),empty()) -> T()
r363: eqs(empty(),stack(E2,S2)) -> F()
r364: eqs(stack(E1,S1),empty()) -> F()
r365: eqs(stack(E1,S1),stack(E2,S2)) -> and(eqt(E1,E2),eqs(S1,S2))
r366: pushs(E1,S1) -> stack(E1,S1)
r367: pops(stack(E1,S1)) -> S1
r368: tops(stack(E1,S1)) -> E1
r369: istops(E1,empty()) -> F()
r370: istops(E1,stack(E2,S1)) -> eqt(E1,E2)
r371: eqc(nocalls(),nocalls()) -> T()
r372: eqc(nocalls(),calls(E2,S2,CS2)) -> F()
r373: eqc(calls(E1,S1,CS1),nocalls()) -> F()
r374: eqc(calls(E1,S1,CS1),calls(E2,S2,CS2)) -> and(eqt(E1,E2),and(eqs(S1,S2),eqc(CS1,CS2)))
r375: push(E1,E2,nocalls()) -> calls(E1,stack(E2,empty()),nocalls())
r376: push(E1,E2,calls(E3,S1,CS1)) -> push1(E1,E2,E3,S1,CS1,eqt(E1,E3))
r377: push1(E1,E2,E3,S1,CS1,T()) -> calls(E3,pushs(E2,S1),CS1)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      element#_A(x1,x2) = x1 + ((1,0,0),(1,1,0),(1,1,1)) x2
      int_A(x1) = ((1,0,0),(0,1,0),(0,1,1)) x1
      s_A(x1) = ((0,0,0),(1,0,0),(1,1,0)) x1 + (1,1,1)
      tuple_A(x1,x2) = ((1,0,0),(1,1,0),(1,1,1)) x1 + ((1,0,0),(1,1,0),(1,1,1)) x2 + (1,1,1)

The next rules are strictly ordered:

  p1

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: record_updates#(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields)) -> record_updates#(record_update(Record,Name,Field,NewF),Name,Fields)

and R consists of:

r1: or(T(),T()) -> T()
r2: or(F(),T()) -> T()
r3: or(T(),F()) -> T()
r4: or(F(),F()) -> F()
r5: and(T(),B) -> B
r6: and(B,T()) -> B
r7: and(F(),B) -> F()
r8: and(B,F()) -> F()
r9: imp(T(),B) -> B
r10: imp(F(),B) -> T()
r11: not(T()) -> F()
r12: not(F()) -> T()
r13: if(T(),B1,B2) -> B1
r14: if(F(),B1,B2) -> B2
r15: eq(T(),T()) -> T()
r16: eq(F(),F()) -> T()
r17: eq(T(),F()) -> F()
r18: eq(F(),T()) -> F()
r19: eqt(nil(),undefined()) -> F()
r20: eqt(nil(),pid(N2)) -> F()
r21: eqt(nil(),int(N2)) -> F()
r22: eqt(nil(),cons(H2,T2)) -> F()
r23: eqt(nil(),tuple(H2,T2)) -> F()
r24: eqt(nil(),tuplenil(H2)) -> F()
r25: eqt(a(),nil()) -> F()
r26: eqt(a(),a()) -> T()
r27: eqt(a(),excl()) -> F()
r28: eqt(a(),false()) -> F()
r29: eqt(a(),lock()) -> F()
r30: eqt(a(),locker()) -> F()
r31: eqt(a(),mcrlrecord()) -> F()
r32: eqt(a(),ok()) -> F()
r33: eqt(a(),pending()) -> F()
r34: eqt(a(),release()) -> F()
r35: eqt(a(),request()) -> F()
r36: eqt(a(),resource()) -> F()
r37: eqt(a(),tag()) -> F()
r38: eqt(a(),true()) -> F()
r39: eqt(a(),undefined()) -> F()
r40: eqt(a(),pid(N2)) -> F()
r41: eqt(a(),int(N2)) -> F()
r42: eqt(a(),cons(H2,T2)) -> F()
r43: eqt(a(),tuple(H2,T2)) -> F()
r44: eqt(a(),tuplenil(H2)) -> F()
r45: eqt(excl(),nil()) -> F()
r46: eqt(excl(),a()) -> F()
r47: eqt(excl(),excl()) -> T()
r48: eqt(excl(),false()) -> F()
r49: eqt(excl(),lock()) -> F()
r50: eqt(excl(),locker()) -> F()
r51: eqt(excl(),mcrlrecord()) -> F()
r52: eqt(excl(),ok()) -> F()
r53: eqt(excl(),pending()) -> F()
r54: eqt(excl(),release()) -> F()
r55: eqt(excl(),request()) -> F()
r56: eqt(excl(),resource()) -> F()
r57: eqt(excl(),tag()) -> F()
r58: eqt(excl(),true()) -> F()
r59: eqt(excl(),undefined()) -> F()
r60: eqt(excl(),pid(N2)) -> F()
r61: eqt(excl(),eqt(false(),int(N2))) -> F()
r62: eqt(false(),cons(H2,T2)) -> F()
r63: eqt(false(),tuple(H2,T2)) -> F()
r64: eqt(false(),tuplenil(H2)) -> F()
r65: eqt(lock(),nil()) -> F()
r66: eqt(lock(),a()) -> F()
r67: eqt(lock(),excl()) -> F()
r68: eqt(lock(),false()) -> F()
r69: eqt(lock(),lock()) -> T()
r70: eqt(lock(),locker()) -> F()
r71: eqt(lock(),mcrlrecord()) -> F()
r72: eqt(lock(),ok()) -> F()
r73: eqt(lock(),pending()) -> F()
r74: eqt(lock(),release()) -> F()
r75: eqt(lock(),request()) -> F()
r76: eqt(lock(),resource()) -> F()
r77: eqt(lock(),tag()) -> F()
r78: eqt(lock(),true()) -> F()
r79: eqt(lock(),undefined()) -> F()
r80: eqt(lock(),pid(N2)) -> F()
r81: eqt(lock(),int(N2)) -> F()
r82: eqt(lock(),cons(H2,T2)) -> F()
r83: eqt(lock(),tuple(H2,T2)) -> F()
r84: eqt(lock(),tuplenil(H2)) -> F()
r85: eqt(locker(),nil()) -> F()
r86: eqt(locker(),a()) -> F()
r87: eqt(locker(),excl()) -> F()
r88: eqt(locker(),false()) -> F()
r89: eqt(locker(),lock()) -> F()
r90: eqt(locker(),locker()) -> T()
r91: eqt(locker(),mcrlrecord()) -> F()
r92: eqt(locker(),ok()) -> F()
r93: eqt(locker(),pending()) -> F()
r94: eqt(locker(),release()) -> F()
r95: eqt(locker(),request()) -> F()
r96: eqt(locker(),resource()) -> F()
r97: eqt(locker(),tag()) -> F()
r98: eqt(locker(),true()) -> F()
r99: eqt(locker(),undefined()) -> F()
r100: eqt(locker(),pid(N2)) -> F()
r101: eqt(locker(),int(N2)) -> F()
r102: eqt(locker(),cons(H2,T2)) -> F()
r103: eqt(locker(),tuple(H2,T2)) -> F()
r104: eqt(locker(),tuplenil(H2)) -> F()
r105: eqt(mcrlrecord(),nil()) -> F()
r106: eqt(mcrlrecord(),a()) -> F()
r107: eqt(mcrlrecord(),excl()) -> F()
r108: eqt(mcrlrecord(),false()) -> F()
r109: eqt(mcrlrecord(),lock()) -> F()
r110: eqt(mcrlrecord(),locker()) -> F()
r111: eqt(mcrlrecord(),mcrlrecord()) -> T()
r112: eqt(mcrlrecord(),ok()) -> F()
r113: eqt(mcrlrecord(),pending()) -> F()
r114: eqt(mcrlrecord(),release()) -> F()
r115: eqt(mcrlrecord(),request()) -> F()
r116: eqt(mcrlrecord(),resource()) -> F()
r117: eqt(ok(),resource()) -> F()
r118: eqt(ok(),tag()) -> F()
r119: eqt(ok(),true()) -> F()
r120: eqt(ok(),undefined()) -> F()
r121: eqt(ok(),pid(N2)) -> F()
r122: eqt(ok(),int(N2)) -> F()
r123: eqt(ok(),cons(H2,T2)) -> F()
r124: eqt(ok(),tuple(H2,T2)) -> F()
r125: eqt(ok(),tuplenil(H2)) -> F()
r126: eqt(pending(),nil()) -> F()
r127: eqt(pending(),a()) -> F()
r128: eqt(pending(),excl()) -> F()
r129: eqt(pending(),false()) -> F()
r130: eqt(pending(),lock()) -> F()
r131: eqt(pending(),locker()) -> F()
r132: eqt(pending(),mcrlrecord()) -> F()
r133: eqt(pending(),ok()) -> F()
r134: eqt(pending(),pending()) -> T()
r135: eqt(pending(),release()) -> F()
r136: eqt(pending(),request()) -> F()
r137: eqt(pending(),resource()) -> F()
r138: eqt(pending(),tag()) -> F()
r139: eqt(pending(),true()) -> F()
r140: eqt(pending(),undefined()) -> F()
r141: eqt(pending(),pid(N2)) -> F()
r142: eqt(pending(),int(N2)) -> F()
r143: eqt(pending(),cons(H2,T2)) -> F()
r144: eqt(pending(),tuple(H2,T2)) -> F()
r145: eqt(pending(),tuplenil(H2)) -> F()
r146: eqt(release(),nil()) -> F()
r147: eqt(release(),a()) -> F()
r148: eqt(release(),excl()) -> F()
r149: eqt(release(),false()) -> F()
r150: eqt(release(),lock()) -> F()
r151: eqt(release(),locker()) -> F()
r152: eqt(release(),mcrlrecord()) -> F()
r153: eqt(release(),ok()) -> F()
r154: eqt(request(),mcrlrecord()) -> F()
r155: eqt(request(),ok()) -> F()
r156: eqt(request(),pending()) -> F()
r157: eqt(request(),release()) -> F()
r158: eqt(request(),request()) -> T()
r159: eqt(request(),resource()) -> F()
r160: eqt(request(),tag()) -> F()
r161: eqt(request(),true()) -> F()
r162: eqt(request(),undefined()) -> F()
r163: eqt(request(),pid(N2)) -> F()
r164: eqt(request(),int(N2)) -> F()
r165: eqt(request(),cons(H2,T2)) -> F()
r166: eqt(request(),tuple(H2,T2)) -> F()
r167: eqt(request(),tuplenil(H2)) -> F()
r168: eqt(resource(),nil()) -> F()
r169: eqt(resource(),a()) -> F()
r170: eqt(resource(),excl()) -> F()
r171: eqt(resource(),false()) -> F()
r172: eqt(resource(),lock()) -> F()
r173: eqt(resource(),locker()) -> F()
r174: eqt(resource(),mcrlrecord()) -> F()
r175: eqt(resource(),ok()) -> F()
r176: eqt(resource(),pending()) -> F()
r177: eqt(resource(),release()) -> F()
r178: eqt(resource(),request()) -> F()
r179: eqt(resource(),resource()) -> T()
r180: eqt(resource(),tag()) -> F()
r181: eqt(resource(),true()) -> F()
r182: eqt(resource(),undefined()) -> F()
r183: eqt(resource(),pid(N2)) -> F()
r184: eqt(resource(),int(N2)) -> F()
r185: eqt(resource(),cons(H2,T2)) -> F()
r186: eqt(resource(),tuple(H2,T2)) -> F()
r187: eqt(resource(),tuplenil(H2)) -> F()
r188: eqt(tag(),nil()) -> F()
r189: eqt(tag(),a()) -> F()
r190: eqt(tag(),excl()) -> F()
r191: eqt(tag(),false()) -> F()
r192: eqt(tag(),lock()) -> F()
r193: eqt(tag(),locker()) -> F()
r194: eqt(tag(),mcrlrecord()) -> F()
r195: eqt(tag(),ok()) -> F()
r196: eqt(tag(),pending()) -> F()
r197: eqt(tag(),release()) -> F()
r198: eqt(tag(),request()) -> F()
r199: eqt(tag(),resource()) -> F()
r200: eqt(tag(),tag()) -> T()
r201: eqt(tag(),true()) -> F()
r202: eqt(tag(),undefined()) -> F()
r203: eqt(tag(),pid(N2)) -> F()
r204: eqt(tag(),int(N2)) -> F()
r205: eqt(tag(),cons(H2,T2)) -> F()
r206: eqt(tag(),tuple(H2,T2)) -> F()
r207: eqt(tag(),tuplenil(H2)) -> F()
r208: eqt(true(),nil()) -> F()
r209: eqt(true(),a()) -> F()
r210: eqt(true(),excl()) -> F()
r211: eqt(true(),false()) -> F()
r212: eqt(true(),lock()) -> F()
r213: eqt(true(),locker()) -> F()
r214: eqt(true(),mcrlrecord()) -> F()
r215: eqt(true(),ok()) -> F()
r216: eqt(true(),pending()) -> F()
r217: eqt(true(),release()) -> F()
r218: eqt(true(),request()) -> F()
r219: eqt(true(),resource()) -> F()
r220: eqt(true(),tag()) -> F()
r221: eqt(true(),true()) -> T()
r222: eqt(true(),undefined()) -> F()
r223: eqt(true(),pid(N2)) -> F()
r224: eqt(true(),int(N2)) -> F()
r225: eqt(true(),cons(H2,T2)) -> F()
r226: eqt(true(),tuple(H2,T2)) -> F()
r227: eqt(true(),tuplenil(H2)) -> F()
r228: eqt(undefined(),nil()) -> F()
r229: eqt(undefined(),a()) -> F()
r230: eqt(undefined(),tuplenil(H2)) -> F()
r231: eqt(pid(N1),nil()) -> F()
r232: eqt(pid(N1),a()) -> F()
r233: eqt(pid(N1),excl()) -> F()
r234: eqt(pid(N1),false()) -> F()
r235: eqt(pid(N1),lock()) -> F()
r236: eqt(pid(N1),locker()) -> F()
r237: eqt(pid(N1),mcrlrecord()) -> F()
r238: eqt(pid(N1),ok()) -> F()
r239: eqt(pid(N1),pending()) -> F()
r240: eqt(pid(N1),release()) -> F()
r241: eqt(pid(N1),request()) -> F()
r242: eqt(pid(N1),resource()) -> F()
r243: eqt(pid(N1),tag()) -> F()
r244: eqt(pid(N1),true()) -> F()
r245: eqt(pid(N1),undefined()) -> F()
r246: eqt(pid(N1),pid(N2)) -> eqt(N1,N2)
r247: eqt(pid(N1),int(N2)) -> F()
r248: eqt(pid(N1),cons(H2,T2)) -> F()
r249: eqt(pid(N1),tuple(H2,T2)) -> F()
r250: eqt(pid(N1),tuplenil(H2)) -> F()
r251: eqt(int(N1),nil()) -> F()
r252: eqt(int(N1),a()) -> F()
r253: eqt(int(N1),excl()) -> F()
r254: eqt(int(N1),false()) -> F()
r255: eqt(int(N1),lock()) -> F()
r256: eqt(int(N1),locker()) -> F()
r257: eqt(int(N1),mcrlrecord()) -> F()
r258: eqt(int(N1),ok()) -> F()
r259: eqt(int(N1),pending()) -> F()
r260: eqt(int(N1),release()) -> F()
r261: eqt(int(N1),request()) -> F()
r262: eqt(int(N1),resource()) -> F()
r263: eqt(int(N1),tag()) -> F()
r264: eqt(int(N1),true()) -> F()
r265: eqt(int(N1),undefined()) -> F()
r266: eqt(cons(H1,T1),resource()) -> F()
r267: eqt(cons(H1,T1),tag()) -> F()
r268: eqt(cons(H1,T1),true()) -> F()
r269: eqt(cons(H1,T1),undefined()) -> F()
r270: eqt(cons(H1,T1),pid(N2)) -> F()
r271: eqt(cons(H1,T1),int(N2)) -> F()
r272: eqt(cons(H1,T1),cons(H2,T2)) -> and(eqt(H1,H2),eqt(T1,T2))
r273: eqt(cons(H1,T1),tuple(H2,T2)) -> F()
r274: eqt(cons(H1,T1),tuplenil(H2)) -> F()
r275: eqt(tuple(H1,T1),nil()) -> F()
r276: eqt(tuple(H1,T1),a()) -> F()
r277: eqt(tuple(H1,T1),excl()) -> F()
r278: eqt(tuple(H1,T1),false()) -> F()
r279: eqt(tuple(H1,T1),lock()) -> F()
r280: eqt(tuple(H1,T1),locker()) -> F()
r281: eqt(tuple(H1,T1),mcrlrecord()) -> F()
r282: eqt(tuple(H1,T1),ok()) -> F()
r283: eqt(tuple(H1,T1),pending()) -> F()
r284: eqt(tuple(H1,T1),release()) -> F()
r285: eqt(tuple(H1,T1),request()) -> F()
r286: eqt(tuple(H1,T1),resource()) -> F()
r287: eqt(tuple(H1,T1),tag()) -> F()
r288: eqt(tuple(H1,T1),true()) -> F()
r289: eqt(tuple(H1,T1),undefined()) -> F()
r290: eqt(tuple(H1,T1),pid(N2)) -> F()
r291: eqt(tuple(H1,T1),int(N2)) -> F()
r292: eqt(tuple(H1,T1),cons(H2,T2)) -> F()
r293: eqt(tuple(H1,T1),tuple(H2,T2)) -> and(eqt(H1,H2),eqt(T1,T2))
r294: eqt(tuple(H1,T1),tuplenil(H2)) -> F()
r295: eqt(tuplenil(H1),nil()) -> F()
r296: eqt(tuplenil(H1),a()) -> F()
r297: eqt(tuplenil(H1),excl()) -> F()
r298: eqt(tuplenil(H1),false()) -> F()
r299: eqt(tuplenil(H1),lock()) -> F()
r300: eqt(tuplenil(H1),locker()) -> F()
r301: eqt(tuplenil(H1),mcrlrecord()) -> F()
r302: eqt(tuplenil(H1),ok()) -> F()
r303: eqt(tuplenil(H1),pending()) -> F()
r304: eqt(tuplenil(H1),release()) -> F()
r305: eqt(tuplenil(H1),request()) -> F()
r306: eqt(tuplenil(H1),resource()) -> F()
r307: eqt(tuplenil(H1),tag()) -> F()
r308: eqt(tuplenil(H1),true()) -> F()
r309: eqt(tuplenil(H1),undefined()) -> F()
r310: eqt(tuplenil(H1),pid(N2)) -> F()
r311: eqt(tuplenil(H1),int(N2)) -> F()
r312: eqt(tuplenil(H1),cons(H2,T2)) -> F()
r313: eqt(tuplenil(H1),tuple(H2,T2)) -> F()
r314: eqt(tuplenil(H1),tuplenil(H2)) -> eqt(H1,H2)
r315: element(int(s(|0|())),tuplenil(T1)) -> T1
r316: element(int(s(|0|())),tuple(T1,T2)) -> T1
r317: element(int(s(s(N1))),tuple(T1,T2)) -> element(int(s(N1)),T2)
r318: record_new(lock()) -> tuple(mcrlrecord(),tuple(lock(),tuple(undefined(),tuple(nil(),tuplenil(nil())))))
r319: record_extract(tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(F2))))),lock(),resource()) -> tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(F2)))))
r320: 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)))))
r321: record_updates(Record,Name,nil()) -> Record
r322: record_updates(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields)) -> record_updates(record_update(Record,Name,Field,NewF),Name,Fields)
r323: locker2_map_promote_pending(nil(),Pending) -> nil()
r324: locker2_map_promote_pending(cons(Lock,Locks),Pending) -> cons(locker2_promote_pending(Lock,Pending),locker2_map_promote_pending(Locks,Pending))
r325: locker2_map_claim_lock(nil(),Resources,Client) -> nil()
r326: locker2_map_claim_lock(cons(Lock,Locks),Resources,Client) -> cons(locker2_claim_lock(Lock,Resources,Client),locker2_map_claim_lock(Locks,Resources,Client))
r327: locker2_map_add_pending(nil(),Resources,Client) -> nil()
r328: locker2_promote_pending(Lock,Client) -> case0(Client,Lock,record_extract(Lock,lock(),pending()))
r329: case0(Client,Lock,cons(Client,Pendings)) -> record_updates(Lock,lock(),cons(tuple(excl(),tuplenil(Client)),cons(tuple(pending(),tuplenil(Pendings)),nil())))
r330: case0(Client,Lock,MCRLFree0) -> Lock
r331: locker2_remove_pending(Lock,Client) -> record_updates(Lock,lock(),cons(tuple(pending(),tuplenil(subtract(record_extract(Lock,lock(),pending()),cons(Client,nil())))),nil()))
r332: locker2_add_pending(Lock,Resources,Client) -> case1(Client,Resources,Lock,member(record_extract(Lock,lock(),resource()),Resources))
r333: case1(Client,Resources,Lock,true()) -> record_updates(Lock,lock(),cons(tuple(pending(),tuplenil(append(record_extract(Lock,lock(),pending()),cons(Client,nil())))),nil()))
r334: case1(Client,Resources,Lock,false()) -> Lock
r335: locker2_release_lock(Lock,Client) -> case2(Client,Lock,gen_modtageq(Client,record_extract(Lock,lock(),excl())))
r336: case2(Client,Lock,true()) -> record_updates(Lock,lock(),cons(tuple(excllock(),excl()),nil()))
r337: case4(Client,Lock,MCRLFree1) -> false()
r338: locker2_obtainables(nil(),Client) -> true()
r339: locker2_obtainables(cons(Lock,Locks),Client) -> case5(Client,Locks,Lock,member(Client,record_extract(Lock,lock(),pending())))
r340: case5(Client,Locks,Lock,true()) -> andt(locker2_obtainable(Lock,Client),locker2_obtainables(Locks,Client))
r341: case5(Client,Locks,Lock,false()) -> locker2_obtainables(Locks,Client)
r342: locker2_check_available(Resource,nil()) -> false()
r343: locker2_check_available(Resource,cons(Lock,Locks)) -> case6(Locks,Lock,Resource,equal(Resource,record_extract(Lock,lock(),resource())))
r344: case6(Locks,Lock,Resource,true()) -> andt(equal(record_extract(Lock,lock(),excl()),nil()),equal(record_extract(Lock,lock(),pending()),nil()))
r345: case6(Locks,Lock,Resource,false()) -> locker2_check_available(Resource,Locks)
r346: locker2_check_availables(nil(),Locks) -> true()
r347: locker2_check_availables(cons(Resource,Resources),Locks) -> andt(locker2_check_available(Resource,Locks),locker2_check_availables(Resources,Locks))
r348: locker2_adduniq(nil(),List) -> List
r349: append(cons(Head,Tail),List) -> cons(Head,append(Tail,List))
r350: subtract(List,nil()) -> List
r351: subtract(List,cons(Head,Tail)) -> subtract(delete(Head,List),Tail)
r352: delete(E,nil()) -> nil()
r353: delete(E,cons(Head,Tail)) -> case8(Tail,Head,E,equal(E,Head))
r354: case8(Tail,Head,E,true()) -> Tail
r355: case8(Tail,Head,E,false()) -> cons(Head,delete(E,Tail))
r356: gen_tag(Pid) -> tuple(Pid,tuplenil(tag()))
r357: gen_modtageq(Client1,Client2) -> equal(Client1,Client2)
r358: member(E,nil()) -> false()
r359: member(E,cons(Head,Tail)) -> case9(Tail,Head,E,equal(E,Head))
r360: case9(Tail,Head,E,true()) -> true()
r361: case9(Tail,Head,E,false()) -> member(E,Tail)
r362: eqs(empty(),empty()) -> T()
r363: eqs(empty(),stack(E2,S2)) -> F()
r364: eqs(stack(E1,S1),empty()) -> F()
r365: eqs(stack(E1,S1),stack(E2,S2)) -> and(eqt(E1,E2),eqs(S1,S2))
r366: pushs(E1,S1) -> stack(E1,S1)
r367: pops(stack(E1,S1)) -> S1
r368: tops(stack(E1,S1)) -> E1
r369: istops(E1,empty()) -> F()
r370: istops(E1,stack(E2,S1)) -> eqt(E1,E2)
r371: eqc(nocalls(),nocalls()) -> T()
r372: eqc(nocalls(),calls(E2,S2,CS2)) -> F()
r373: eqc(calls(E1,S1,CS1),nocalls()) -> F()
r374: eqc(calls(E1,S1,CS1),calls(E2,S2,CS2)) -> and(eqt(E1,E2),and(eqs(S1,S2),eqc(CS1,CS2)))
r375: push(E1,E2,nocalls()) -> calls(E1,stack(E2,empty()),nocalls())
r376: push(E1,E2,calls(E3,S1,CS1)) -> push1(E1,E2,E3,S1,CS1,eqt(E1,E3))
r377: push1(E1,E2,E3,S1,CS1,T()) -> calls(E3,pushs(E2,S1),CS1)

The set of usable rules consists of

  r320

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      record_updates#_A(x1,x2,x3) = x1 + ((1,0,0),(1,0,0),(1,0,0)) x3
      cons_A(x1,x2) = ((1,0,0),(1,0,0),(0,0,0)) x1 + ((1,0,0),(0,1,0),(1,1,1)) x2 + (1,0,1)
      tuple_A(x1,x2) = x1 + (1,6,1)
      tuplenil_A(x1) = ((0,0,0),(0,0,0),(1,0,0)) x1 + (1,1,1)
      record_update_A(x1,x2,x3,x4) = ((1,0,0),(0,0,0),(0,1,0)) x1 + ((1,0,0),(1,1,0),(0,1,1)) x3 + (1,3,3)
      mcrlrecord_A() = (1,1,1)
      lock_A() = (1,1,1)
      pending_A() = (1,1,1)

The next rules are strictly ordered:

  p1

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: locker2_map_promote_pending#(cons(Lock,Locks),Pending) -> locker2_map_promote_pending#(Locks,Pending)

and R consists of:

r1: or(T(),T()) -> T()
r2: or(F(),T()) -> T()
r3: or(T(),F()) -> T()
r4: or(F(),F()) -> F()
r5: and(T(),B) -> B
r6: and(B,T()) -> B
r7: and(F(),B) -> F()
r8: and(B,F()) -> F()
r9: imp(T(),B) -> B
r10: imp(F(),B) -> T()
r11: not(T()) -> F()
r12: not(F()) -> T()
r13: if(T(),B1,B2) -> B1
r14: if(F(),B1,B2) -> B2
r15: eq(T(),T()) -> T()
r16: eq(F(),F()) -> T()
r17: eq(T(),F()) -> F()
r18: eq(F(),T()) -> F()
r19: eqt(nil(),undefined()) -> F()
r20: eqt(nil(),pid(N2)) -> F()
r21: eqt(nil(),int(N2)) -> F()
r22: eqt(nil(),cons(H2,T2)) -> F()
r23: eqt(nil(),tuple(H2,T2)) -> F()
r24: eqt(nil(),tuplenil(H2)) -> F()
r25: eqt(a(),nil()) -> F()
r26: eqt(a(),a()) -> T()
r27: eqt(a(),excl()) -> F()
r28: eqt(a(),false()) -> F()
r29: eqt(a(),lock()) -> F()
r30: eqt(a(),locker()) -> F()
r31: eqt(a(),mcrlrecord()) -> F()
r32: eqt(a(),ok()) -> F()
r33: eqt(a(),pending()) -> F()
r34: eqt(a(),release()) -> F()
r35: eqt(a(),request()) -> F()
r36: eqt(a(),resource()) -> F()
r37: eqt(a(),tag()) -> F()
r38: eqt(a(),true()) -> F()
r39: eqt(a(),undefined()) -> F()
r40: eqt(a(),pid(N2)) -> F()
r41: eqt(a(),int(N2)) -> F()
r42: eqt(a(),cons(H2,T2)) -> F()
r43: eqt(a(),tuple(H2,T2)) -> F()
r44: eqt(a(),tuplenil(H2)) -> F()
r45: eqt(excl(),nil()) -> F()
r46: eqt(excl(),a()) -> F()
r47: eqt(excl(),excl()) -> T()
r48: eqt(excl(),false()) -> F()
r49: eqt(excl(),lock()) -> F()
r50: eqt(excl(),locker()) -> F()
r51: eqt(excl(),mcrlrecord()) -> F()
r52: eqt(excl(),ok()) -> F()
r53: eqt(excl(),pending()) -> F()
r54: eqt(excl(),release()) -> F()
r55: eqt(excl(),request()) -> F()
r56: eqt(excl(),resource()) -> F()
r57: eqt(excl(),tag()) -> F()
r58: eqt(excl(),true()) -> F()
r59: eqt(excl(),undefined()) -> F()
r60: eqt(excl(),pid(N2)) -> F()
r61: eqt(excl(),eqt(false(),int(N2))) -> F()
r62: eqt(false(),cons(H2,T2)) -> F()
r63: eqt(false(),tuple(H2,T2)) -> F()
r64: eqt(false(),tuplenil(H2)) -> F()
r65: eqt(lock(),nil()) -> F()
r66: eqt(lock(),a()) -> F()
r67: eqt(lock(),excl()) -> F()
r68: eqt(lock(),false()) -> F()
r69: eqt(lock(),lock()) -> T()
r70: eqt(lock(),locker()) -> F()
r71: eqt(lock(),mcrlrecord()) -> F()
r72: eqt(lock(),ok()) -> F()
r73: eqt(lock(),pending()) -> F()
r74: eqt(lock(),release()) -> F()
r75: eqt(lock(),request()) -> F()
r76: eqt(lock(),resource()) -> F()
r77: eqt(lock(),tag()) -> F()
r78: eqt(lock(),true()) -> F()
r79: eqt(lock(),undefined()) -> F()
r80: eqt(lock(),pid(N2)) -> F()
r81: eqt(lock(),int(N2)) -> F()
r82: eqt(lock(),cons(H2,T2)) -> F()
r83: eqt(lock(),tuple(H2,T2)) -> F()
r84: eqt(lock(),tuplenil(H2)) -> F()
r85: eqt(locker(),nil()) -> F()
r86: eqt(locker(),a()) -> F()
r87: eqt(locker(),excl()) -> F()
r88: eqt(locker(),false()) -> F()
r89: eqt(locker(),lock()) -> F()
r90: eqt(locker(),locker()) -> T()
r91: eqt(locker(),mcrlrecord()) -> F()
r92: eqt(locker(),ok()) -> F()
r93: eqt(locker(),pending()) -> F()
r94: eqt(locker(),release()) -> F()
r95: eqt(locker(),request()) -> F()
r96: eqt(locker(),resource()) -> F()
r97: eqt(locker(),tag()) -> F()
r98: eqt(locker(),true()) -> F()
r99: eqt(locker(),undefined()) -> F()
r100: eqt(locker(),pid(N2)) -> F()
r101: eqt(locker(),int(N2)) -> F()
r102: eqt(locker(),cons(H2,T2)) -> F()
r103: eqt(locker(),tuple(H2,T2)) -> F()
r104: eqt(locker(),tuplenil(H2)) -> F()
r105: eqt(mcrlrecord(),nil()) -> F()
r106: eqt(mcrlrecord(),a()) -> F()
r107: eqt(mcrlrecord(),excl()) -> F()
r108: eqt(mcrlrecord(),false()) -> F()
r109: eqt(mcrlrecord(),lock()) -> F()
r110: eqt(mcrlrecord(),locker()) -> F()
r111: eqt(mcrlrecord(),mcrlrecord()) -> T()
r112: eqt(mcrlrecord(),ok()) -> F()
r113: eqt(mcrlrecord(),pending()) -> F()
r114: eqt(mcrlrecord(),release()) -> F()
r115: eqt(mcrlrecord(),request()) -> F()
r116: eqt(mcrlrecord(),resource()) -> F()
r117: eqt(ok(),resource()) -> F()
r118: eqt(ok(),tag()) -> F()
r119: eqt(ok(),true()) -> F()
r120: eqt(ok(),undefined()) -> F()
r121: eqt(ok(),pid(N2)) -> F()
r122: eqt(ok(),int(N2)) -> F()
r123: eqt(ok(),cons(H2,T2)) -> F()
r124: eqt(ok(),tuple(H2,T2)) -> F()
r125: eqt(ok(),tuplenil(H2)) -> F()
r126: eqt(pending(),nil()) -> F()
r127: eqt(pending(),a()) -> F()
r128: eqt(pending(),excl()) -> F()
r129: eqt(pending(),false()) -> F()
r130: eqt(pending(),lock()) -> F()
r131: eqt(pending(),locker()) -> F()
r132: eqt(pending(),mcrlrecord()) -> F()
r133: eqt(pending(),ok()) -> F()
r134: eqt(pending(),pending()) -> T()
r135: eqt(pending(),release()) -> F()
r136: eqt(pending(),request()) -> F()
r137: eqt(pending(),resource()) -> F()
r138: eqt(pending(),tag()) -> F()
r139: eqt(pending(),true()) -> F()
r140: eqt(pending(),undefined()) -> F()
r141: eqt(pending(),pid(N2)) -> F()
r142: eqt(pending(),int(N2)) -> F()
r143: eqt(pending(),cons(H2,T2)) -> F()
r144: eqt(pending(),tuple(H2,T2)) -> F()
r145: eqt(pending(),tuplenil(H2)) -> F()
r146: eqt(release(),nil()) -> F()
r147: eqt(release(),a()) -> F()
r148: eqt(release(),excl()) -> F()
r149: eqt(release(),false()) -> F()
r150: eqt(release(),lock()) -> F()
r151: eqt(release(),locker()) -> F()
r152: eqt(release(),mcrlrecord()) -> F()
r153: eqt(release(),ok()) -> F()
r154: eqt(request(),mcrlrecord()) -> F()
r155: eqt(request(),ok()) -> F()
r156: eqt(request(),pending()) -> F()
r157: eqt(request(),release()) -> F()
r158: eqt(request(),request()) -> T()
r159: eqt(request(),resource()) -> F()
r160: eqt(request(),tag()) -> F()
r161: eqt(request(),true()) -> F()
r162: eqt(request(),undefined()) -> F()
r163: eqt(request(),pid(N2)) -> F()
r164: eqt(request(),int(N2)) -> F()
r165: eqt(request(),cons(H2,T2)) -> F()
r166: eqt(request(),tuple(H2,T2)) -> F()
r167: eqt(request(),tuplenil(H2)) -> F()
r168: eqt(resource(),nil()) -> F()
r169: eqt(resource(),a()) -> F()
r170: eqt(resource(),excl()) -> F()
r171: eqt(resource(),false()) -> F()
r172: eqt(resource(),lock()) -> F()
r173: eqt(resource(),locker()) -> F()
r174: eqt(resource(),mcrlrecord()) -> F()
r175: eqt(resource(),ok()) -> F()
r176: eqt(resource(),pending()) -> F()
r177: eqt(resource(),release()) -> F()
r178: eqt(resource(),request()) -> F()
r179: eqt(resource(),resource()) -> T()
r180: eqt(resource(),tag()) -> F()
r181: eqt(resource(),true()) -> F()
r182: eqt(resource(),undefined()) -> F()
r183: eqt(resource(),pid(N2)) -> F()
r184: eqt(resource(),int(N2)) -> F()
r185: eqt(resource(),cons(H2,T2)) -> F()
r186: eqt(resource(),tuple(H2,T2)) -> F()
r187: eqt(resource(),tuplenil(H2)) -> F()
r188: eqt(tag(),nil()) -> F()
r189: eqt(tag(),a()) -> F()
r190: eqt(tag(),excl()) -> F()
r191: eqt(tag(),false()) -> F()
r192: eqt(tag(),lock()) -> F()
r193: eqt(tag(),locker()) -> F()
r194: eqt(tag(),mcrlrecord()) -> F()
r195: eqt(tag(),ok()) -> F()
r196: eqt(tag(),pending()) -> F()
r197: eqt(tag(),release()) -> F()
r198: eqt(tag(),request()) -> F()
r199: eqt(tag(),resource()) -> F()
r200: eqt(tag(),tag()) -> T()
r201: eqt(tag(),true()) -> F()
r202: eqt(tag(),undefined()) -> F()
r203: eqt(tag(),pid(N2)) -> F()
r204: eqt(tag(),int(N2)) -> F()
r205: eqt(tag(),cons(H2,T2)) -> F()
r206: eqt(tag(),tuple(H2,T2)) -> F()
r207: eqt(tag(),tuplenil(H2)) -> F()
r208: eqt(true(),nil()) -> F()
r209: eqt(true(),a()) -> F()
r210: eqt(true(),excl()) -> F()
r211: eqt(true(),false()) -> F()
r212: eqt(true(),lock()) -> F()
r213: eqt(true(),locker()) -> F()
r214: eqt(true(),mcrlrecord()) -> F()
r215: eqt(true(),ok()) -> F()
r216: eqt(true(),pending()) -> F()
r217: eqt(true(),release()) -> F()
r218: eqt(true(),request()) -> F()
r219: eqt(true(),resource()) -> F()
r220: eqt(true(),tag()) -> F()
r221: eqt(true(),true()) -> T()
r222: eqt(true(),undefined()) -> F()
r223: eqt(true(),pid(N2)) -> F()
r224: eqt(true(),int(N2)) -> F()
r225: eqt(true(),cons(H2,T2)) -> F()
r226: eqt(true(),tuple(H2,T2)) -> F()
r227: eqt(true(),tuplenil(H2)) -> F()
r228: eqt(undefined(),nil()) -> F()
r229: eqt(undefined(),a()) -> F()
r230: eqt(undefined(),tuplenil(H2)) -> F()
r231: eqt(pid(N1),nil()) -> F()
r232: eqt(pid(N1),a()) -> F()
r233: eqt(pid(N1),excl()) -> F()
r234: eqt(pid(N1),false()) -> F()
r235: eqt(pid(N1),lock()) -> F()
r236: eqt(pid(N1),locker()) -> F()
r237: eqt(pid(N1),mcrlrecord()) -> F()
r238: eqt(pid(N1),ok()) -> F()
r239: eqt(pid(N1),pending()) -> F()
r240: eqt(pid(N1),release()) -> F()
r241: eqt(pid(N1),request()) -> F()
r242: eqt(pid(N1),resource()) -> F()
r243: eqt(pid(N1),tag()) -> F()
r244: eqt(pid(N1),true()) -> F()
r245: eqt(pid(N1),undefined()) -> F()
r246: eqt(pid(N1),pid(N2)) -> eqt(N1,N2)
r247: eqt(pid(N1),int(N2)) -> F()
r248: eqt(pid(N1),cons(H2,T2)) -> F()
r249: eqt(pid(N1),tuple(H2,T2)) -> F()
r250: eqt(pid(N1),tuplenil(H2)) -> F()
r251: eqt(int(N1),nil()) -> F()
r252: eqt(int(N1),a()) -> F()
r253: eqt(int(N1),excl()) -> F()
r254: eqt(int(N1),false()) -> F()
r255: eqt(int(N1),lock()) -> F()
r256: eqt(int(N1),locker()) -> F()
r257: eqt(int(N1),mcrlrecord()) -> F()
r258: eqt(int(N1),ok()) -> F()
r259: eqt(int(N1),pending()) -> F()
r260: eqt(int(N1),release()) -> F()
r261: eqt(int(N1),request()) -> F()
r262: eqt(int(N1),resource()) -> F()
r263: eqt(int(N1),tag()) -> F()
r264: eqt(int(N1),true()) -> F()
r265: eqt(int(N1),undefined()) -> F()
r266: eqt(cons(H1,T1),resource()) -> F()
r267: eqt(cons(H1,T1),tag()) -> F()
r268: eqt(cons(H1,T1),true()) -> F()
r269: eqt(cons(H1,T1),undefined()) -> F()
r270: eqt(cons(H1,T1),pid(N2)) -> F()
r271: eqt(cons(H1,T1),int(N2)) -> F()
r272: eqt(cons(H1,T1),cons(H2,T2)) -> and(eqt(H1,H2),eqt(T1,T2))
r273: eqt(cons(H1,T1),tuple(H2,T2)) -> F()
r274: eqt(cons(H1,T1),tuplenil(H2)) -> F()
r275: eqt(tuple(H1,T1),nil()) -> F()
r276: eqt(tuple(H1,T1),a()) -> F()
r277: eqt(tuple(H1,T1),excl()) -> F()
r278: eqt(tuple(H1,T1),false()) -> F()
r279: eqt(tuple(H1,T1),lock()) -> F()
r280: eqt(tuple(H1,T1),locker()) -> F()
r281: eqt(tuple(H1,T1),mcrlrecord()) -> F()
r282: eqt(tuple(H1,T1),ok()) -> F()
r283: eqt(tuple(H1,T1),pending()) -> F()
r284: eqt(tuple(H1,T1),release()) -> F()
r285: eqt(tuple(H1,T1),request()) -> F()
r286: eqt(tuple(H1,T1),resource()) -> F()
r287: eqt(tuple(H1,T1),tag()) -> F()
r288: eqt(tuple(H1,T1),true()) -> F()
r289: eqt(tuple(H1,T1),undefined()) -> F()
r290: eqt(tuple(H1,T1),pid(N2)) -> F()
r291: eqt(tuple(H1,T1),int(N2)) -> F()
r292: eqt(tuple(H1,T1),cons(H2,T2)) -> F()
r293: eqt(tuple(H1,T1),tuple(H2,T2)) -> and(eqt(H1,H2),eqt(T1,T2))
r294: eqt(tuple(H1,T1),tuplenil(H2)) -> F()
r295: eqt(tuplenil(H1),nil()) -> F()
r296: eqt(tuplenil(H1),a()) -> F()
r297: eqt(tuplenil(H1),excl()) -> F()
r298: eqt(tuplenil(H1),false()) -> F()
r299: eqt(tuplenil(H1),lock()) -> F()
r300: eqt(tuplenil(H1),locker()) -> F()
r301: eqt(tuplenil(H1),mcrlrecord()) -> F()
r302: eqt(tuplenil(H1),ok()) -> F()
r303: eqt(tuplenil(H1),pending()) -> F()
r304: eqt(tuplenil(H1),release()) -> F()
r305: eqt(tuplenil(H1),request()) -> F()
r306: eqt(tuplenil(H1),resource()) -> F()
r307: eqt(tuplenil(H1),tag()) -> F()
r308: eqt(tuplenil(H1),true()) -> F()
r309: eqt(tuplenil(H1),undefined()) -> F()
r310: eqt(tuplenil(H1),pid(N2)) -> F()
r311: eqt(tuplenil(H1),int(N2)) -> F()
r312: eqt(tuplenil(H1),cons(H2,T2)) -> F()
r313: eqt(tuplenil(H1),tuple(H2,T2)) -> F()
r314: eqt(tuplenil(H1),tuplenil(H2)) -> eqt(H1,H2)
r315: element(int(s(|0|())),tuplenil(T1)) -> T1
r316: element(int(s(|0|())),tuple(T1,T2)) -> T1
r317: element(int(s(s(N1))),tuple(T1,T2)) -> element(int(s(N1)),T2)
r318: record_new(lock()) -> tuple(mcrlrecord(),tuple(lock(),tuple(undefined(),tuple(nil(),tuplenil(nil())))))
r319: record_extract(tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(F2))))),lock(),resource()) -> tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(F2)))))
r320: 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)))))
r321: record_updates(Record,Name,nil()) -> Record
r322: record_updates(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields)) -> record_updates(record_update(Record,Name,Field,NewF),Name,Fields)
r323: locker2_map_promote_pending(nil(),Pending) -> nil()
r324: locker2_map_promote_pending(cons(Lock,Locks),Pending) -> cons(locker2_promote_pending(Lock,Pending),locker2_map_promote_pending(Locks,Pending))
r325: locker2_map_claim_lock(nil(),Resources,Client) -> nil()
r326: locker2_map_claim_lock(cons(Lock,Locks),Resources,Client) -> cons(locker2_claim_lock(Lock,Resources,Client),locker2_map_claim_lock(Locks,Resources,Client))
r327: locker2_map_add_pending(nil(),Resources,Client) -> nil()
r328: locker2_promote_pending(Lock,Client) -> case0(Client,Lock,record_extract(Lock,lock(),pending()))
r329: case0(Client,Lock,cons(Client,Pendings)) -> record_updates(Lock,lock(),cons(tuple(excl(),tuplenil(Client)),cons(tuple(pending(),tuplenil(Pendings)),nil())))
r330: case0(Client,Lock,MCRLFree0) -> Lock
r331: locker2_remove_pending(Lock,Client) -> record_updates(Lock,lock(),cons(tuple(pending(),tuplenil(subtract(record_extract(Lock,lock(),pending()),cons(Client,nil())))),nil()))
r332: locker2_add_pending(Lock,Resources,Client) -> case1(Client,Resources,Lock,member(record_extract(Lock,lock(),resource()),Resources))
r333: case1(Client,Resources,Lock,true()) -> record_updates(Lock,lock(),cons(tuple(pending(),tuplenil(append(record_extract(Lock,lock(),pending()),cons(Client,nil())))),nil()))
r334: case1(Client,Resources,Lock,false()) -> Lock
r335: locker2_release_lock(Lock,Client) -> case2(Client,Lock,gen_modtageq(Client,record_extract(Lock,lock(),excl())))
r336: case2(Client,Lock,true()) -> record_updates(Lock,lock(),cons(tuple(excllock(),excl()),nil()))
r337: case4(Client,Lock,MCRLFree1) -> false()
r338: locker2_obtainables(nil(),Client) -> true()
r339: locker2_obtainables(cons(Lock,Locks),Client) -> case5(Client,Locks,Lock,member(Client,record_extract(Lock,lock(),pending())))
r340: case5(Client,Locks,Lock,true()) -> andt(locker2_obtainable(Lock,Client),locker2_obtainables(Locks,Client))
r341: case5(Client,Locks,Lock,false()) -> locker2_obtainables(Locks,Client)
r342: locker2_check_available(Resource,nil()) -> false()
r343: locker2_check_available(Resource,cons(Lock,Locks)) -> case6(Locks,Lock,Resource,equal(Resource,record_extract(Lock,lock(),resource())))
r344: case6(Locks,Lock,Resource,true()) -> andt(equal(record_extract(Lock,lock(),excl()),nil()),equal(record_extract(Lock,lock(),pending()),nil()))
r345: case6(Locks,Lock,Resource,false()) -> locker2_check_available(Resource,Locks)
r346: locker2_check_availables(nil(),Locks) -> true()
r347: locker2_check_availables(cons(Resource,Resources),Locks) -> andt(locker2_check_available(Resource,Locks),locker2_check_availables(Resources,Locks))
r348: locker2_adduniq(nil(),List) -> List
r349: append(cons(Head,Tail),List) -> cons(Head,append(Tail,List))
r350: subtract(List,nil()) -> List
r351: subtract(List,cons(Head,Tail)) -> subtract(delete(Head,List),Tail)
r352: delete(E,nil()) -> nil()
r353: delete(E,cons(Head,Tail)) -> case8(Tail,Head,E,equal(E,Head))
r354: case8(Tail,Head,E,true()) -> Tail
r355: case8(Tail,Head,E,false()) -> cons(Head,delete(E,Tail))
r356: gen_tag(Pid) -> tuple(Pid,tuplenil(tag()))
r357: gen_modtageq(Client1,Client2) -> equal(Client1,Client2)
r358: member(E,nil()) -> false()
r359: member(E,cons(Head,Tail)) -> case9(Tail,Head,E,equal(E,Head))
r360: case9(Tail,Head,E,true()) -> true()
r361: case9(Tail,Head,E,false()) -> member(E,Tail)
r362: eqs(empty(),empty()) -> T()
r363: eqs(empty(),stack(E2,S2)) -> F()
r364: eqs(stack(E1,S1),empty()) -> F()
r365: eqs(stack(E1,S1),stack(E2,S2)) -> and(eqt(E1,E2),eqs(S1,S2))
r366: pushs(E1,S1) -> stack(E1,S1)
r367: pops(stack(E1,S1)) -> S1
r368: tops(stack(E1,S1)) -> E1
r369: istops(E1,empty()) -> F()
r370: istops(E1,stack(E2,S1)) -> eqt(E1,E2)
r371: eqc(nocalls(),nocalls()) -> T()
r372: eqc(nocalls(),calls(E2,S2,CS2)) -> F()
r373: eqc(calls(E1,S1,CS1),nocalls()) -> F()
r374: eqc(calls(E1,S1,CS1),calls(E2,S2,CS2)) -> and(eqt(E1,E2),and(eqs(S1,S2),eqc(CS1,CS2)))
r375: push(E1,E2,nocalls()) -> calls(E1,stack(E2,empty()),nocalls())
r376: push(E1,E2,calls(E3,S1,CS1)) -> push1(E1,E2,E3,S1,CS1,eqt(E1,E3))
r377: push1(E1,E2,E3,S1,CS1,T()) -> calls(E3,pushs(E2,S1),CS1)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      locker2_map_promote_pending#_A(x1,x2) = ((0,0,0),(1,0,0),(1,1,0)) x1 + ((1,0,0),(0,1,0),(0,1,1)) x2
      cons_A(x1,x2) = ((1,0,0),(1,1,0),(1,1,1)) x1 + ((1,0,0),(1,1,0),(1,1,1)) x2 + (1,1,1)

The next rules are strictly ordered:

  p1

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: locker2_map_claim_lock#(cons(Lock,Locks),Resources,Client) -> locker2_map_claim_lock#(Locks,Resources,Client)

and R consists of:

r1: or(T(),T()) -> T()
r2: or(F(),T()) -> T()
r3: or(T(),F()) -> T()
r4: or(F(),F()) -> F()
r5: and(T(),B) -> B
r6: and(B,T()) -> B
r7: and(F(),B) -> F()
r8: and(B,F()) -> F()
r9: imp(T(),B) -> B
r10: imp(F(),B) -> T()
r11: not(T()) -> F()
r12: not(F()) -> T()
r13: if(T(),B1,B2) -> B1
r14: if(F(),B1,B2) -> B2
r15: eq(T(),T()) -> T()
r16: eq(F(),F()) -> T()
r17: eq(T(),F()) -> F()
r18: eq(F(),T()) -> F()
r19: eqt(nil(),undefined()) -> F()
r20: eqt(nil(),pid(N2)) -> F()
r21: eqt(nil(),int(N2)) -> F()
r22: eqt(nil(),cons(H2,T2)) -> F()
r23: eqt(nil(),tuple(H2,T2)) -> F()
r24: eqt(nil(),tuplenil(H2)) -> F()
r25: eqt(a(),nil()) -> F()
r26: eqt(a(),a()) -> T()
r27: eqt(a(),excl()) -> F()
r28: eqt(a(),false()) -> F()
r29: eqt(a(),lock()) -> F()
r30: eqt(a(),locker()) -> F()
r31: eqt(a(),mcrlrecord()) -> F()
r32: eqt(a(),ok()) -> F()
r33: eqt(a(),pending()) -> F()
r34: eqt(a(),release()) -> F()
r35: eqt(a(),request()) -> F()
r36: eqt(a(),resource()) -> F()
r37: eqt(a(),tag()) -> F()
r38: eqt(a(),true()) -> F()
r39: eqt(a(),undefined()) -> F()
r40: eqt(a(),pid(N2)) -> F()
r41: eqt(a(),int(N2)) -> F()
r42: eqt(a(),cons(H2,T2)) -> F()
r43: eqt(a(),tuple(H2,T2)) -> F()
r44: eqt(a(),tuplenil(H2)) -> F()
r45: eqt(excl(),nil()) -> F()
r46: eqt(excl(),a()) -> F()
r47: eqt(excl(),excl()) -> T()
r48: eqt(excl(),false()) -> F()
r49: eqt(excl(),lock()) -> F()
r50: eqt(excl(),locker()) -> F()
r51: eqt(excl(),mcrlrecord()) -> F()
r52: eqt(excl(),ok()) -> F()
r53: eqt(excl(),pending()) -> F()
r54: eqt(excl(),release()) -> F()
r55: eqt(excl(),request()) -> F()
r56: eqt(excl(),resource()) -> F()
r57: eqt(excl(),tag()) -> F()
r58: eqt(excl(),true()) -> F()
r59: eqt(excl(),undefined()) -> F()
r60: eqt(excl(),pid(N2)) -> F()
r61: eqt(excl(),eqt(false(),int(N2))) -> F()
r62: eqt(false(),cons(H2,T2)) -> F()
r63: eqt(false(),tuple(H2,T2)) -> F()
r64: eqt(false(),tuplenil(H2)) -> F()
r65: eqt(lock(),nil()) -> F()
r66: eqt(lock(),a()) -> F()
r67: eqt(lock(),excl()) -> F()
r68: eqt(lock(),false()) -> F()
r69: eqt(lock(),lock()) -> T()
r70: eqt(lock(),locker()) -> F()
r71: eqt(lock(),mcrlrecord()) -> F()
r72: eqt(lock(),ok()) -> F()
r73: eqt(lock(),pending()) -> F()
r74: eqt(lock(),release()) -> F()
r75: eqt(lock(),request()) -> F()
r76: eqt(lock(),resource()) -> F()
r77: eqt(lock(),tag()) -> F()
r78: eqt(lock(),true()) -> F()
r79: eqt(lock(),undefined()) -> F()
r80: eqt(lock(),pid(N2)) -> F()
r81: eqt(lock(),int(N2)) -> F()
r82: eqt(lock(),cons(H2,T2)) -> F()
r83: eqt(lock(),tuple(H2,T2)) -> F()
r84: eqt(lock(),tuplenil(H2)) -> F()
r85: eqt(locker(),nil()) -> F()
r86: eqt(locker(),a()) -> F()
r87: eqt(locker(),excl()) -> F()
r88: eqt(locker(),false()) -> F()
r89: eqt(locker(),lock()) -> F()
r90: eqt(locker(),locker()) -> T()
r91: eqt(locker(),mcrlrecord()) -> F()
r92: eqt(locker(),ok()) -> F()
r93: eqt(locker(),pending()) -> F()
r94: eqt(locker(),release()) -> F()
r95: eqt(locker(),request()) -> F()
r96: eqt(locker(),resource()) -> F()
r97: eqt(locker(),tag()) -> F()
r98: eqt(locker(),true()) -> F()
r99: eqt(locker(),undefined()) -> F()
r100: eqt(locker(),pid(N2)) -> F()
r101: eqt(locker(),int(N2)) -> F()
r102: eqt(locker(),cons(H2,T2)) -> F()
r103: eqt(locker(),tuple(H2,T2)) -> F()
r104: eqt(locker(),tuplenil(H2)) -> F()
r105: eqt(mcrlrecord(),nil()) -> F()
r106: eqt(mcrlrecord(),a()) -> F()
r107: eqt(mcrlrecord(),excl()) -> F()
r108: eqt(mcrlrecord(),false()) -> F()
r109: eqt(mcrlrecord(),lock()) -> F()
r110: eqt(mcrlrecord(),locker()) -> F()
r111: eqt(mcrlrecord(),mcrlrecord()) -> T()
r112: eqt(mcrlrecord(),ok()) -> F()
r113: eqt(mcrlrecord(),pending()) -> F()
r114: eqt(mcrlrecord(),release()) -> F()
r115: eqt(mcrlrecord(),request()) -> F()
r116: eqt(mcrlrecord(),resource()) -> F()
r117: eqt(ok(),resource()) -> F()
r118: eqt(ok(),tag()) -> F()
r119: eqt(ok(),true()) -> F()
r120: eqt(ok(),undefined()) -> F()
r121: eqt(ok(),pid(N2)) -> F()
r122: eqt(ok(),int(N2)) -> F()
r123: eqt(ok(),cons(H2,T2)) -> F()
r124: eqt(ok(),tuple(H2,T2)) -> F()
r125: eqt(ok(),tuplenil(H2)) -> F()
r126: eqt(pending(),nil()) -> F()
r127: eqt(pending(),a()) -> F()
r128: eqt(pending(),excl()) -> F()
r129: eqt(pending(),false()) -> F()
r130: eqt(pending(),lock()) -> F()
r131: eqt(pending(),locker()) -> F()
r132: eqt(pending(),mcrlrecord()) -> F()
r133: eqt(pending(),ok()) -> F()
r134: eqt(pending(),pending()) -> T()
r135: eqt(pending(),release()) -> F()
r136: eqt(pending(),request()) -> F()
r137: eqt(pending(),resource()) -> F()
r138: eqt(pending(),tag()) -> F()
r139: eqt(pending(),true()) -> F()
r140: eqt(pending(),undefined()) -> F()
r141: eqt(pending(),pid(N2)) -> F()
r142: eqt(pending(),int(N2)) -> F()
r143: eqt(pending(),cons(H2,T2)) -> F()
r144: eqt(pending(),tuple(H2,T2)) -> F()
r145: eqt(pending(),tuplenil(H2)) -> F()
r146: eqt(release(),nil()) -> F()
r147: eqt(release(),a()) -> F()
r148: eqt(release(),excl()) -> F()
r149: eqt(release(),false()) -> F()
r150: eqt(release(),lock()) -> F()
r151: eqt(release(),locker()) -> F()
r152: eqt(release(),mcrlrecord()) -> F()
r153: eqt(release(),ok()) -> F()
r154: eqt(request(),mcrlrecord()) -> F()
r155: eqt(request(),ok()) -> F()
r156: eqt(request(),pending()) -> F()
r157: eqt(request(),release()) -> F()
r158: eqt(request(),request()) -> T()
r159: eqt(request(),resource()) -> F()
r160: eqt(request(),tag()) -> F()
r161: eqt(request(),true()) -> F()
r162: eqt(request(),undefined()) -> F()
r163: eqt(request(),pid(N2)) -> F()
r164: eqt(request(),int(N2)) -> F()
r165: eqt(request(),cons(H2,T2)) -> F()
r166: eqt(request(),tuple(H2,T2)) -> F()
r167: eqt(request(),tuplenil(H2)) -> F()
r168: eqt(resource(),nil()) -> F()
r169: eqt(resource(),a()) -> F()
r170: eqt(resource(),excl()) -> F()
r171: eqt(resource(),false()) -> F()
r172: eqt(resource(),lock()) -> F()
r173: eqt(resource(),locker()) -> F()
r174: eqt(resource(),mcrlrecord()) -> F()
r175: eqt(resource(),ok()) -> F()
r176: eqt(resource(),pending()) -> F()
r177: eqt(resource(),release()) -> F()
r178: eqt(resource(),request()) -> F()
r179: eqt(resource(),resource()) -> T()
r180: eqt(resource(),tag()) -> F()
r181: eqt(resource(),true()) -> F()
r182: eqt(resource(),undefined()) -> F()
r183: eqt(resource(),pid(N2)) -> F()
r184: eqt(resource(),int(N2)) -> F()
r185: eqt(resource(),cons(H2,T2)) -> F()
r186: eqt(resource(),tuple(H2,T2)) -> F()
r187: eqt(resource(),tuplenil(H2)) -> F()
r188: eqt(tag(),nil()) -> F()
r189: eqt(tag(),a()) -> F()
r190: eqt(tag(),excl()) -> F()
r191: eqt(tag(),false()) -> F()
r192: eqt(tag(),lock()) -> F()
r193: eqt(tag(),locker()) -> F()
r194: eqt(tag(),mcrlrecord()) -> F()
r195: eqt(tag(),ok()) -> F()
r196: eqt(tag(),pending()) -> F()
r197: eqt(tag(),release()) -> F()
r198: eqt(tag(),request()) -> F()
r199: eqt(tag(),resource()) -> F()
r200: eqt(tag(),tag()) -> T()
r201: eqt(tag(),true()) -> F()
r202: eqt(tag(),undefined()) -> F()
r203: eqt(tag(),pid(N2)) -> F()
r204: eqt(tag(),int(N2)) -> F()
r205: eqt(tag(),cons(H2,T2)) -> F()
r206: eqt(tag(),tuple(H2,T2)) -> F()
r207: eqt(tag(),tuplenil(H2)) -> F()
r208: eqt(true(),nil()) -> F()
r209: eqt(true(),a()) -> F()
r210: eqt(true(),excl()) -> F()
r211: eqt(true(),false()) -> F()
r212: eqt(true(),lock()) -> F()
r213: eqt(true(),locker()) -> F()
r214: eqt(true(),mcrlrecord()) -> F()
r215: eqt(true(),ok()) -> F()
r216: eqt(true(),pending()) -> F()
r217: eqt(true(),release()) -> F()
r218: eqt(true(),request()) -> F()
r219: eqt(true(),resource()) -> F()
r220: eqt(true(),tag()) -> F()
r221: eqt(true(),true()) -> T()
r222: eqt(true(),undefined()) -> F()
r223: eqt(true(),pid(N2)) -> F()
r224: eqt(true(),int(N2)) -> F()
r225: eqt(true(),cons(H2,T2)) -> F()
r226: eqt(true(),tuple(H2,T2)) -> F()
r227: eqt(true(),tuplenil(H2)) -> F()
r228: eqt(undefined(),nil()) -> F()
r229: eqt(undefined(),a()) -> F()
r230: eqt(undefined(),tuplenil(H2)) -> F()
r231: eqt(pid(N1),nil()) -> F()
r232: eqt(pid(N1),a()) -> F()
r233: eqt(pid(N1),excl()) -> F()
r234: eqt(pid(N1),false()) -> F()
r235: eqt(pid(N1),lock()) -> F()
r236: eqt(pid(N1),locker()) -> F()
r237: eqt(pid(N1),mcrlrecord()) -> F()
r238: eqt(pid(N1),ok()) -> F()
r239: eqt(pid(N1),pending()) -> F()
r240: eqt(pid(N1),release()) -> F()
r241: eqt(pid(N1),request()) -> F()
r242: eqt(pid(N1),resource()) -> F()
r243: eqt(pid(N1),tag()) -> F()
r244: eqt(pid(N1),true()) -> F()
r245: eqt(pid(N1),undefined()) -> F()
r246: eqt(pid(N1),pid(N2)) -> eqt(N1,N2)
r247: eqt(pid(N1),int(N2)) -> F()
r248: eqt(pid(N1),cons(H2,T2)) -> F()
r249: eqt(pid(N1),tuple(H2,T2)) -> F()
r250: eqt(pid(N1),tuplenil(H2)) -> F()
r251: eqt(int(N1),nil()) -> F()
r252: eqt(int(N1),a()) -> F()
r253: eqt(int(N1),excl()) -> F()
r254: eqt(int(N1),false()) -> F()
r255: eqt(int(N1),lock()) -> F()
r256: eqt(int(N1),locker()) -> F()
r257: eqt(int(N1),mcrlrecord()) -> F()
r258: eqt(int(N1),ok()) -> F()
r259: eqt(int(N1),pending()) -> F()
r260: eqt(int(N1),release()) -> F()
r261: eqt(int(N1),request()) -> F()
r262: eqt(int(N1),resource()) -> F()
r263: eqt(int(N1),tag()) -> F()
r264: eqt(int(N1),true()) -> F()
r265: eqt(int(N1),undefined()) -> F()
r266: eqt(cons(H1,T1),resource()) -> F()
r267: eqt(cons(H1,T1),tag()) -> F()
r268: eqt(cons(H1,T1),true()) -> F()
r269: eqt(cons(H1,T1),undefined()) -> F()
r270: eqt(cons(H1,T1),pid(N2)) -> F()
r271: eqt(cons(H1,T1),int(N2)) -> F()
r272: eqt(cons(H1,T1),cons(H2,T2)) -> and(eqt(H1,H2),eqt(T1,T2))
r273: eqt(cons(H1,T1),tuple(H2,T2)) -> F()
r274: eqt(cons(H1,T1),tuplenil(H2)) -> F()
r275: eqt(tuple(H1,T1),nil()) -> F()
r276: eqt(tuple(H1,T1),a()) -> F()
r277: eqt(tuple(H1,T1),excl()) -> F()
r278: eqt(tuple(H1,T1),false()) -> F()
r279: eqt(tuple(H1,T1),lock()) -> F()
r280: eqt(tuple(H1,T1),locker()) -> F()
r281: eqt(tuple(H1,T1),mcrlrecord()) -> F()
r282: eqt(tuple(H1,T1),ok()) -> F()
r283: eqt(tuple(H1,T1),pending()) -> F()
r284: eqt(tuple(H1,T1),release()) -> F()
r285: eqt(tuple(H1,T1),request()) -> F()
r286: eqt(tuple(H1,T1),resource()) -> F()
r287: eqt(tuple(H1,T1),tag()) -> F()
r288: eqt(tuple(H1,T1),true()) -> F()
r289: eqt(tuple(H1,T1),undefined()) -> F()
r290: eqt(tuple(H1,T1),pid(N2)) -> F()
r291: eqt(tuple(H1,T1),int(N2)) -> F()
r292: eqt(tuple(H1,T1),cons(H2,T2)) -> F()
r293: eqt(tuple(H1,T1),tuple(H2,T2)) -> and(eqt(H1,H2),eqt(T1,T2))
r294: eqt(tuple(H1,T1),tuplenil(H2)) -> F()
r295: eqt(tuplenil(H1),nil()) -> F()
r296: eqt(tuplenil(H1),a()) -> F()
r297: eqt(tuplenil(H1),excl()) -> F()
r298: eqt(tuplenil(H1),false()) -> F()
r299: eqt(tuplenil(H1),lock()) -> F()
r300: eqt(tuplenil(H1),locker()) -> F()
r301: eqt(tuplenil(H1),mcrlrecord()) -> F()
r302: eqt(tuplenil(H1),ok()) -> F()
r303: eqt(tuplenil(H1),pending()) -> F()
r304: eqt(tuplenil(H1),release()) -> F()
r305: eqt(tuplenil(H1),request()) -> F()
r306: eqt(tuplenil(H1),resource()) -> F()
r307: eqt(tuplenil(H1),tag()) -> F()
r308: eqt(tuplenil(H1),true()) -> F()
r309: eqt(tuplenil(H1),undefined()) -> F()
r310: eqt(tuplenil(H1),pid(N2)) -> F()
r311: eqt(tuplenil(H1),int(N2)) -> F()
r312: eqt(tuplenil(H1),cons(H2,T2)) -> F()
r313: eqt(tuplenil(H1),tuple(H2,T2)) -> F()
r314: eqt(tuplenil(H1),tuplenil(H2)) -> eqt(H1,H2)
r315: element(int(s(|0|())),tuplenil(T1)) -> T1
r316: element(int(s(|0|())),tuple(T1,T2)) -> T1
r317: element(int(s(s(N1))),tuple(T1,T2)) -> element(int(s(N1)),T2)
r318: record_new(lock()) -> tuple(mcrlrecord(),tuple(lock(),tuple(undefined(),tuple(nil(),tuplenil(nil())))))
r319: record_extract(tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(F2))))),lock(),resource()) -> tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(F2)))))
r320: 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)))))
r321: record_updates(Record,Name,nil()) -> Record
r322: record_updates(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields)) -> record_updates(record_update(Record,Name,Field,NewF),Name,Fields)
r323: locker2_map_promote_pending(nil(),Pending) -> nil()
r324: locker2_map_promote_pending(cons(Lock,Locks),Pending) -> cons(locker2_promote_pending(Lock,Pending),locker2_map_promote_pending(Locks,Pending))
r325: locker2_map_claim_lock(nil(),Resources,Client) -> nil()
r326: locker2_map_claim_lock(cons(Lock,Locks),Resources,Client) -> cons(locker2_claim_lock(Lock,Resources,Client),locker2_map_claim_lock(Locks,Resources,Client))
r327: locker2_map_add_pending(nil(),Resources,Client) -> nil()
r328: locker2_promote_pending(Lock,Client) -> case0(Client,Lock,record_extract(Lock,lock(),pending()))
r329: case0(Client,Lock,cons(Client,Pendings)) -> record_updates(Lock,lock(),cons(tuple(excl(),tuplenil(Client)),cons(tuple(pending(),tuplenil(Pendings)),nil())))
r330: case0(Client,Lock,MCRLFree0) -> Lock
r331: locker2_remove_pending(Lock,Client) -> record_updates(Lock,lock(),cons(tuple(pending(),tuplenil(subtract(record_extract(Lock,lock(),pending()),cons(Client,nil())))),nil()))
r332: locker2_add_pending(Lock,Resources,Client) -> case1(Client,Resources,Lock,member(record_extract(Lock,lock(),resource()),Resources))
r333: case1(Client,Resources,Lock,true()) -> record_updates(Lock,lock(),cons(tuple(pending(),tuplenil(append(record_extract(Lock,lock(),pending()),cons(Client,nil())))),nil()))
r334: case1(Client,Resources,Lock,false()) -> Lock
r335: locker2_release_lock(Lock,Client) -> case2(Client,Lock,gen_modtageq(Client,record_extract(Lock,lock(),excl())))
r336: case2(Client,Lock,true()) -> record_updates(Lock,lock(),cons(tuple(excllock(),excl()),nil()))
r337: case4(Client,Lock,MCRLFree1) -> false()
r338: locker2_obtainables(nil(),Client) -> true()
r339: locker2_obtainables(cons(Lock,Locks),Client) -> case5(Client,Locks,Lock,member(Client,record_extract(Lock,lock(),pending())))
r340: case5(Client,Locks,Lock,true()) -> andt(locker2_obtainable(Lock,Client),locker2_obtainables(Locks,Client))
r341: case5(Client,Locks,Lock,false()) -> locker2_obtainables(Locks,Client)
r342: locker2_check_available(Resource,nil()) -> false()
r343: locker2_check_available(Resource,cons(Lock,Locks)) -> case6(Locks,Lock,Resource,equal(Resource,record_extract(Lock,lock(),resource())))
r344: case6(Locks,Lock,Resource,true()) -> andt(equal(record_extract(Lock,lock(),excl()),nil()),equal(record_extract(Lock,lock(),pending()),nil()))
r345: case6(Locks,Lock,Resource,false()) -> locker2_check_available(Resource,Locks)
r346: locker2_check_availables(nil(),Locks) -> true()
r347: locker2_check_availables(cons(Resource,Resources),Locks) -> andt(locker2_check_available(Resource,Locks),locker2_check_availables(Resources,Locks))
r348: locker2_adduniq(nil(),List) -> List
r349: append(cons(Head,Tail),List) -> cons(Head,append(Tail,List))
r350: subtract(List,nil()) -> List
r351: subtract(List,cons(Head,Tail)) -> subtract(delete(Head,List),Tail)
r352: delete(E,nil()) -> nil()
r353: delete(E,cons(Head,Tail)) -> case8(Tail,Head,E,equal(E,Head))
r354: case8(Tail,Head,E,true()) -> Tail
r355: case8(Tail,Head,E,false()) -> cons(Head,delete(E,Tail))
r356: gen_tag(Pid) -> tuple(Pid,tuplenil(tag()))
r357: gen_modtageq(Client1,Client2) -> equal(Client1,Client2)
r358: member(E,nil()) -> false()
r359: member(E,cons(Head,Tail)) -> case9(Tail,Head,E,equal(E,Head))
r360: case9(Tail,Head,E,true()) -> true()
r361: case9(Tail,Head,E,false()) -> member(E,Tail)
r362: eqs(empty(),empty()) -> T()
r363: eqs(empty(),stack(E2,S2)) -> F()
r364: eqs(stack(E1,S1),empty()) -> F()
r365: eqs(stack(E1,S1),stack(E2,S2)) -> and(eqt(E1,E2),eqs(S1,S2))
r366: pushs(E1,S1) -> stack(E1,S1)
r367: pops(stack(E1,S1)) -> S1
r368: tops(stack(E1,S1)) -> E1
r369: istops(E1,empty()) -> F()
r370: istops(E1,stack(E2,S1)) -> eqt(E1,E2)
r371: eqc(nocalls(),nocalls()) -> T()
r372: eqc(nocalls(),calls(E2,S2,CS2)) -> F()
r373: eqc(calls(E1,S1,CS1),nocalls()) -> F()
r374: eqc(calls(E1,S1,CS1),calls(E2,S2,CS2)) -> and(eqt(E1,E2),and(eqs(S1,S2),eqc(CS1,CS2)))
r375: push(E1,E2,nocalls()) -> calls(E1,stack(E2,empty()),nocalls())
r376: push(E1,E2,calls(E3,S1,CS1)) -> push1(E1,E2,E3,S1,CS1,eqt(E1,E3))
r377: push1(E1,E2,E3,S1,CS1,T()) -> calls(E3,pushs(E2,S1),CS1)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      locker2_map_claim_lock#_A(x1,x2,x3) = ((1,0,0),(0,1,0),(1,1,1)) x1 + ((1,0,0),(0,1,0),(0,1,1)) x2 + ((1,0,0),(0,1,0),(0,1,1)) x3
      cons_A(x1,x2) = ((1,0,0),(1,1,0),(1,1,1)) x1 + ((1,0,0),(1,1,0),(1,1,1)) x2 + (1,1,1)

The next rules are strictly ordered:

  p1
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68, r69, r70, r71, r72, r73, r74, r75, r76, r77, r78, r79, r80, r81, r82, r83, r84, r85, r86, r87, r88, r89, r90, r91, r92, r93, r94, r95, r96, r97, r98, r99, r100, r101, r102, r103, r104, r105, r106, r107, r108, r109, r110, r111, r112, r113, r114, r115, r116, r117, r118, r119, r120, r121, r122, r123, r124, r125, r126, r127, r128, r129, r130, r131, r132, r133, r134, r135, r136, r137, r138, r139, r140, r141, r142, r143, r144, r145, r146, r147, r148, r149, r150, r151, r152, r153, r154, r155, r156, r157, r158, r159, r160, r161, r162, r163, r164, r165, r166, r167, r168, r169, r170, r171, r172, r173, r174, r175, r176, r177, r178, r179, r180, r181, r182, r183, r184, r185, r186, r187, r188, r189, r190, r191, r192, r193, r194, r195, r196, r197, r198, r199, r200, r201, r202, r203, r204, r205, r206, r207, r208, r209, r210, r211, r212, r213, r214, r215, r216, r217, r218, r219, r220, r221, r222, r223, r224, r225, r226, r227, r228, r229, r230, r231, r232, r233, r234, r235, r236, r237, r238, r239, r240, r241, r242, r243, r244, r245, r246, r247, r248, r249, r250, r251, r252, r253, r254, r255, r256, r257, r258, r259, r260, r261, r262, r263, r264, r265, r266, r267, r268, r269, r270, r271, r272, r273, r274, r275, r276, r277, r278, r279, r280, r281, r282, r283, r284, r285, r286, r287, r288, r289, r290, r291, r292, r293, r294, r295, r296, r297, r298, r299, r300, r301, r302, r303, r304, r305, r306, r307, r308, r309, r310, r311, r312, r313, r314, r315, r316, r317, r318, r319, r320, r321, r322, r323, r324, r325, r326, r327, r328, r329, r330, r331, r332, r333, r334, r335, r336, r337, r338, r339, r340, r341, r342, r343, r344, r345, r346, r347, r348, r349, r350, r351, r352, r353, r354, r355, r356, r357, r358, r359, r360, r361, r362, r363, r364, r365, r366, r367, r368, r369, r370, r371, r372, r373, r374, r375, r376, r377

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: subtract#(List,cons(Head,Tail)) -> subtract#(delete(Head,List),Tail)

and R consists of:

r1: or(T(),T()) -> T()
r2: or(F(),T()) -> T()
r3: or(T(),F()) -> T()
r4: or(F(),F()) -> F()
r5: and(T(),B) -> B
r6: and(B,T()) -> B
r7: and(F(),B) -> F()
r8: and(B,F()) -> F()
r9: imp(T(),B) -> B
r10: imp(F(),B) -> T()
r11: not(T()) -> F()
r12: not(F()) -> T()
r13: if(T(),B1,B2) -> B1
r14: if(F(),B1,B2) -> B2
r15: eq(T(),T()) -> T()
r16: eq(F(),F()) -> T()
r17: eq(T(),F()) -> F()
r18: eq(F(),T()) -> F()
r19: eqt(nil(),undefined()) -> F()
r20: eqt(nil(),pid(N2)) -> F()
r21: eqt(nil(),int(N2)) -> F()
r22: eqt(nil(),cons(H2,T2)) -> F()
r23: eqt(nil(),tuple(H2,T2)) -> F()
r24: eqt(nil(),tuplenil(H2)) -> F()
r25: eqt(a(),nil()) -> F()
r26: eqt(a(),a()) -> T()
r27: eqt(a(),excl()) -> F()
r28: eqt(a(),false()) -> F()
r29: eqt(a(),lock()) -> F()
r30: eqt(a(),locker()) -> F()
r31: eqt(a(),mcrlrecord()) -> F()
r32: eqt(a(),ok()) -> F()
r33: eqt(a(),pending()) -> F()
r34: eqt(a(),release()) -> F()
r35: eqt(a(),request()) -> F()
r36: eqt(a(),resource()) -> F()
r37: eqt(a(),tag()) -> F()
r38: eqt(a(),true()) -> F()
r39: eqt(a(),undefined()) -> F()
r40: eqt(a(),pid(N2)) -> F()
r41: eqt(a(),int(N2)) -> F()
r42: eqt(a(),cons(H2,T2)) -> F()
r43: eqt(a(),tuple(H2,T2)) -> F()
r44: eqt(a(),tuplenil(H2)) -> F()
r45: eqt(excl(),nil()) -> F()
r46: eqt(excl(),a()) -> F()
r47: eqt(excl(),excl()) -> T()
r48: eqt(excl(),false()) -> F()
r49: eqt(excl(),lock()) -> F()
r50: eqt(excl(),locker()) -> F()
r51: eqt(excl(),mcrlrecord()) -> F()
r52: eqt(excl(),ok()) -> F()
r53: eqt(excl(),pending()) -> F()
r54: eqt(excl(),release()) -> F()
r55: eqt(excl(),request()) -> F()
r56: eqt(excl(),resource()) -> F()
r57: eqt(excl(),tag()) -> F()
r58: eqt(excl(),true()) -> F()
r59: eqt(excl(),undefined()) -> F()
r60: eqt(excl(),pid(N2)) -> F()
r61: eqt(excl(),eqt(false(),int(N2))) -> F()
r62: eqt(false(),cons(H2,T2)) -> F()
r63: eqt(false(),tuple(H2,T2)) -> F()
r64: eqt(false(),tuplenil(H2)) -> F()
r65: eqt(lock(),nil()) -> F()
r66: eqt(lock(),a()) -> F()
r67: eqt(lock(),excl()) -> F()
r68: eqt(lock(),false()) -> F()
r69: eqt(lock(),lock()) -> T()
r70: eqt(lock(),locker()) -> F()
r71: eqt(lock(),mcrlrecord()) -> F()
r72: eqt(lock(),ok()) -> F()
r73: eqt(lock(),pending()) -> F()
r74: eqt(lock(),release()) -> F()
r75: eqt(lock(),request()) -> F()
r76: eqt(lock(),resource()) -> F()
r77: eqt(lock(),tag()) -> F()
r78: eqt(lock(),true()) -> F()
r79: eqt(lock(),undefined()) -> F()
r80: eqt(lock(),pid(N2)) -> F()
r81: eqt(lock(),int(N2)) -> F()
r82: eqt(lock(),cons(H2,T2)) -> F()
r83: eqt(lock(),tuple(H2,T2)) -> F()
r84: eqt(lock(),tuplenil(H2)) -> F()
r85: eqt(locker(),nil()) -> F()
r86: eqt(locker(),a()) -> F()
r87: eqt(locker(),excl()) -> F()
r88: eqt(locker(),false()) -> F()
r89: eqt(locker(),lock()) -> F()
r90: eqt(locker(),locker()) -> T()
r91: eqt(locker(),mcrlrecord()) -> F()
r92: eqt(locker(),ok()) -> F()
r93: eqt(locker(),pending()) -> F()
r94: eqt(locker(),release()) -> F()
r95: eqt(locker(),request()) -> F()
r96: eqt(locker(),resource()) -> F()
r97: eqt(locker(),tag()) -> F()
r98: eqt(locker(),true()) -> F()
r99: eqt(locker(),undefined()) -> F()
r100: eqt(locker(),pid(N2)) -> F()
r101: eqt(locker(),int(N2)) -> F()
r102: eqt(locker(),cons(H2,T2)) -> F()
r103: eqt(locker(),tuple(H2,T2)) -> F()
r104: eqt(locker(),tuplenil(H2)) -> F()
r105: eqt(mcrlrecord(),nil()) -> F()
r106: eqt(mcrlrecord(),a()) -> F()
r107: eqt(mcrlrecord(),excl()) -> F()
r108: eqt(mcrlrecord(),false()) -> F()
r109: eqt(mcrlrecord(),lock()) -> F()
r110: eqt(mcrlrecord(),locker()) -> F()
r111: eqt(mcrlrecord(),mcrlrecord()) -> T()
r112: eqt(mcrlrecord(),ok()) -> F()
r113: eqt(mcrlrecord(),pending()) -> F()
r114: eqt(mcrlrecord(),release()) -> F()
r115: eqt(mcrlrecord(),request()) -> F()
r116: eqt(mcrlrecord(),resource()) -> F()
r117: eqt(ok(),resource()) -> F()
r118: eqt(ok(),tag()) -> F()
r119: eqt(ok(),true()) -> F()
r120: eqt(ok(),undefined()) -> F()
r121: eqt(ok(),pid(N2)) -> F()
r122: eqt(ok(),int(N2)) -> F()
r123: eqt(ok(),cons(H2,T2)) -> F()
r124: eqt(ok(),tuple(H2,T2)) -> F()
r125: eqt(ok(),tuplenil(H2)) -> F()
r126: eqt(pending(),nil()) -> F()
r127: eqt(pending(),a()) -> F()
r128: eqt(pending(),excl()) -> F()
r129: eqt(pending(),false()) -> F()
r130: eqt(pending(),lock()) -> F()
r131: eqt(pending(),locker()) -> F()
r132: eqt(pending(),mcrlrecord()) -> F()
r133: eqt(pending(),ok()) -> F()
r134: eqt(pending(),pending()) -> T()
r135: eqt(pending(),release()) -> F()
r136: eqt(pending(),request()) -> F()
r137: eqt(pending(),resource()) -> F()
r138: eqt(pending(),tag()) -> F()
r139: eqt(pending(),true()) -> F()
r140: eqt(pending(),undefined()) -> F()
r141: eqt(pending(),pid(N2)) -> F()
r142: eqt(pending(),int(N2)) -> F()
r143: eqt(pending(),cons(H2,T2)) -> F()
r144: eqt(pending(),tuple(H2,T2)) -> F()
r145: eqt(pending(),tuplenil(H2)) -> F()
r146: eqt(release(),nil()) -> F()
r147: eqt(release(),a()) -> F()
r148: eqt(release(),excl()) -> F()
r149: eqt(release(),false()) -> F()
r150: eqt(release(),lock()) -> F()
r151: eqt(release(),locker()) -> F()
r152: eqt(release(),mcrlrecord()) -> F()
r153: eqt(release(),ok()) -> F()
r154: eqt(request(),mcrlrecord()) -> F()
r155: eqt(request(),ok()) -> F()
r156: eqt(request(),pending()) -> F()
r157: eqt(request(),release()) -> F()
r158: eqt(request(),request()) -> T()
r159: eqt(request(),resource()) -> F()
r160: eqt(request(),tag()) -> F()
r161: eqt(request(),true()) -> F()
r162: eqt(request(),undefined()) -> F()
r163: eqt(request(),pid(N2)) -> F()
r164: eqt(request(),int(N2)) -> F()
r165: eqt(request(),cons(H2,T2)) -> F()
r166: eqt(request(),tuple(H2,T2)) -> F()
r167: eqt(request(),tuplenil(H2)) -> F()
r168: eqt(resource(),nil()) -> F()
r169: eqt(resource(),a()) -> F()
r170: eqt(resource(),excl()) -> F()
r171: eqt(resource(),false()) -> F()
r172: eqt(resource(),lock()) -> F()
r173: eqt(resource(),locker()) -> F()
r174: eqt(resource(),mcrlrecord()) -> F()
r175: eqt(resource(),ok()) -> F()
r176: eqt(resource(),pending()) -> F()
r177: eqt(resource(),release()) -> F()
r178: eqt(resource(),request()) -> F()
r179: eqt(resource(),resource()) -> T()
r180: eqt(resource(),tag()) -> F()
r181: eqt(resource(),true()) -> F()
r182: eqt(resource(),undefined()) -> F()
r183: eqt(resource(),pid(N2)) -> F()
r184: eqt(resource(),int(N2)) -> F()
r185: eqt(resource(),cons(H2,T2)) -> F()
r186: eqt(resource(),tuple(H2,T2)) -> F()
r187: eqt(resource(),tuplenil(H2)) -> F()
r188: eqt(tag(),nil()) -> F()
r189: eqt(tag(),a()) -> F()
r190: eqt(tag(),excl()) -> F()
r191: eqt(tag(),false()) -> F()
r192: eqt(tag(),lock()) -> F()
r193: eqt(tag(),locker()) -> F()
r194: eqt(tag(),mcrlrecord()) -> F()
r195: eqt(tag(),ok()) -> F()
r196: eqt(tag(),pending()) -> F()
r197: eqt(tag(),release()) -> F()
r198: eqt(tag(),request()) -> F()
r199: eqt(tag(),resource()) -> F()
r200: eqt(tag(),tag()) -> T()
r201: eqt(tag(),true()) -> F()
r202: eqt(tag(),undefined()) -> F()
r203: eqt(tag(),pid(N2)) -> F()
r204: eqt(tag(),int(N2)) -> F()
r205: eqt(tag(),cons(H2,T2)) -> F()
r206: eqt(tag(),tuple(H2,T2)) -> F()
r207: eqt(tag(),tuplenil(H2)) -> F()
r208: eqt(true(),nil()) -> F()
r209: eqt(true(),a()) -> F()
r210: eqt(true(),excl()) -> F()
r211: eqt(true(),false()) -> F()
r212: eqt(true(),lock()) -> F()
r213: eqt(true(),locker()) -> F()
r214: eqt(true(),mcrlrecord()) -> F()
r215: eqt(true(),ok()) -> F()
r216: eqt(true(),pending()) -> F()
r217: eqt(true(),release()) -> F()
r218: eqt(true(),request()) -> F()
r219: eqt(true(),resource()) -> F()
r220: eqt(true(),tag()) -> F()
r221: eqt(true(),true()) -> T()
r222: eqt(true(),undefined()) -> F()
r223: eqt(true(),pid(N2)) -> F()
r224: eqt(true(),int(N2)) -> F()
r225: eqt(true(),cons(H2,T2)) -> F()
r226: eqt(true(),tuple(H2,T2)) -> F()
r227: eqt(true(),tuplenil(H2)) -> F()
r228: eqt(undefined(),nil()) -> F()
r229: eqt(undefined(),a()) -> F()
r230: eqt(undefined(),tuplenil(H2)) -> F()
r231: eqt(pid(N1),nil()) -> F()
r232: eqt(pid(N1),a()) -> F()
r233: eqt(pid(N1),excl()) -> F()
r234: eqt(pid(N1),false()) -> F()
r235: eqt(pid(N1),lock()) -> F()
r236: eqt(pid(N1),locker()) -> F()
r237: eqt(pid(N1),mcrlrecord()) -> F()
r238: eqt(pid(N1),ok()) -> F()
r239: eqt(pid(N1),pending()) -> F()
r240: eqt(pid(N1),release()) -> F()
r241: eqt(pid(N1),request()) -> F()
r242: eqt(pid(N1),resource()) -> F()
r243: eqt(pid(N1),tag()) -> F()
r244: eqt(pid(N1),true()) -> F()
r245: eqt(pid(N1),undefined()) -> F()
r246: eqt(pid(N1),pid(N2)) -> eqt(N1,N2)
r247: eqt(pid(N1),int(N2)) -> F()
r248: eqt(pid(N1),cons(H2,T2)) -> F()
r249: eqt(pid(N1),tuple(H2,T2)) -> F()
r250: eqt(pid(N1),tuplenil(H2)) -> F()
r251: eqt(int(N1),nil()) -> F()
r252: eqt(int(N1),a()) -> F()
r253: eqt(int(N1),excl()) -> F()
r254: eqt(int(N1),false()) -> F()
r255: eqt(int(N1),lock()) -> F()
r256: eqt(int(N1),locker()) -> F()
r257: eqt(int(N1),mcrlrecord()) -> F()
r258: eqt(int(N1),ok()) -> F()
r259: eqt(int(N1),pending()) -> F()
r260: eqt(int(N1),release()) -> F()
r261: eqt(int(N1),request()) -> F()
r262: eqt(int(N1),resource()) -> F()
r263: eqt(int(N1),tag()) -> F()
r264: eqt(int(N1),true()) -> F()
r265: eqt(int(N1),undefined()) -> F()
r266: eqt(cons(H1,T1),resource()) -> F()
r267: eqt(cons(H1,T1),tag()) -> F()
r268: eqt(cons(H1,T1),true()) -> F()
r269: eqt(cons(H1,T1),undefined()) -> F()
r270: eqt(cons(H1,T1),pid(N2)) -> F()
r271: eqt(cons(H1,T1),int(N2)) -> F()
r272: eqt(cons(H1,T1),cons(H2,T2)) -> and(eqt(H1,H2),eqt(T1,T2))
r273: eqt(cons(H1,T1),tuple(H2,T2)) -> F()
r274: eqt(cons(H1,T1),tuplenil(H2)) -> F()
r275: eqt(tuple(H1,T1),nil()) -> F()
r276: eqt(tuple(H1,T1),a()) -> F()
r277: eqt(tuple(H1,T1),excl()) -> F()
r278: eqt(tuple(H1,T1),false()) -> F()
r279: eqt(tuple(H1,T1),lock()) -> F()
r280: eqt(tuple(H1,T1),locker()) -> F()
r281: eqt(tuple(H1,T1),mcrlrecord()) -> F()
r282: eqt(tuple(H1,T1),ok()) -> F()
r283: eqt(tuple(H1,T1),pending()) -> F()
r284: eqt(tuple(H1,T1),release()) -> F()
r285: eqt(tuple(H1,T1),request()) -> F()
r286: eqt(tuple(H1,T1),resource()) -> F()
r287: eqt(tuple(H1,T1),tag()) -> F()
r288: eqt(tuple(H1,T1),true()) -> F()
r289: eqt(tuple(H1,T1),undefined()) -> F()
r290: eqt(tuple(H1,T1),pid(N2)) -> F()
r291: eqt(tuple(H1,T1),int(N2)) -> F()
r292: eqt(tuple(H1,T1),cons(H2,T2)) -> F()
r293: eqt(tuple(H1,T1),tuple(H2,T2)) -> and(eqt(H1,H2),eqt(T1,T2))
r294: eqt(tuple(H1,T1),tuplenil(H2)) -> F()
r295: eqt(tuplenil(H1),nil()) -> F()
r296: eqt(tuplenil(H1),a()) -> F()
r297: eqt(tuplenil(H1),excl()) -> F()
r298: eqt(tuplenil(H1),false()) -> F()
r299: eqt(tuplenil(H1),lock()) -> F()
r300: eqt(tuplenil(H1),locker()) -> F()
r301: eqt(tuplenil(H1),mcrlrecord()) -> F()
r302: eqt(tuplenil(H1),ok()) -> F()
r303: eqt(tuplenil(H1),pending()) -> F()
r304: eqt(tuplenil(H1),release()) -> F()
r305: eqt(tuplenil(H1),request()) -> F()
r306: eqt(tuplenil(H1),resource()) -> F()
r307: eqt(tuplenil(H1),tag()) -> F()
r308: eqt(tuplenil(H1),true()) -> F()
r309: eqt(tuplenil(H1),undefined()) -> F()
r310: eqt(tuplenil(H1),pid(N2)) -> F()
r311: eqt(tuplenil(H1),int(N2)) -> F()
r312: eqt(tuplenil(H1),cons(H2,T2)) -> F()
r313: eqt(tuplenil(H1),tuple(H2,T2)) -> F()
r314: eqt(tuplenil(H1),tuplenil(H2)) -> eqt(H1,H2)
r315: element(int(s(|0|())),tuplenil(T1)) -> T1
r316: element(int(s(|0|())),tuple(T1,T2)) -> T1
r317: element(int(s(s(N1))),tuple(T1,T2)) -> element(int(s(N1)),T2)
r318: record_new(lock()) -> tuple(mcrlrecord(),tuple(lock(),tuple(undefined(),tuple(nil(),tuplenil(nil())))))
r319: record_extract(tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(F2))))),lock(),resource()) -> tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(F2)))))
r320: 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)))))
r321: record_updates(Record,Name,nil()) -> Record
r322: record_updates(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields)) -> record_updates(record_update(Record,Name,Field,NewF),Name,Fields)
r323: locker2_map_promote_pending(nil(),Pending) -> nil()
r324: locker2_map_promote_pending(cons(Lock,Locks),Pending) -> cons(locker2_promote_pending(Lock,Pending),locker2_map_promote_pending(Locks,Pending))
r325: locker2_map_claim_lock(nil(),Resources,Client) -> nil()
r326: locker2_map_claim_lock(cons(Lock,Locks),Resources,Client) -> cons(locker2_claim_lock(Lock,Resources,Client),locker2_map_claim_lock(Locks,Resources,Client))
r327: locker2_map_add_pending(nil(),Resources,Client) -> nil()
r328: locker2_promote_pending(Lock,Client) -> case0(Client,Lock,record_extract(Lock,lock(),pending()))
r329: case0(Client,Lock,cons(Client,Pendings)) -> record_updates(Lock,lock(),cons(tuple(excl(),tuplenil(Client)),cons(tuple(pending(),tuplenil(Pendings)),nil())))
r330: case0(Client,Lock,MCRLFree0) -> Lock
r331: locker2_remove_pending(Lock,Client) -> record_updates(Lock,lock(),cons(tuple(pending(),tuplenil(subtract(record_extract(Lock,lock(),pending()),cons(Client,nil())))),nil()))
r332: locker2_add_pending(Lock,Resources,Client) -> case1(Client,Resources,Lock,member(record_extract(Lock,lock(),resource()),Resources))
r333: case1(Client,Resources,Lock,true()) -> record_updates(Lock,lock(),cons(tuple(pending(),tuplenil(append(record_extract(Lock,lock(),pending()),cons(Client,nil())))),nil()))
r334: case1(Client,Resources,Lock,false()) -> Lock
r335: locker2_release_lock(Lock,Client) -> case2(Client,Lock,gen_modtageq(Client,record_extract(Lock,lock(),excl())))
r336: case2(Client,Lock,true()) -> record_updates(Lock,lock(),cons(tuple(excllock(),excl()),nil()))
r337: case4(Client,Lock,MCRLFree1) -> false()
r338: locker2_obtainables(nil(),Client) -> true()
r339: locker2_obtainables(cons(Lock,Locks),Client) -> case5(Client,Locks,Lock,member(Client,record_extract(Lock,lock(),pending())))
r340: case5(Client,Locks,Lock,true()) -> andt(locker2_obtainable(Lock,Client),locker2_obtainables(Locks,Client))
r341: case5(Client,Locks,Lock,false()) -> locker2_obtainables(Locks,Client)
r342: locker2_check_available(Resource,nil()) -> false()
r343: locker2_check_available(Resource,cons(Lock,Locks)) -> case6(Locks,Lock,Resource,equal(Resource,record_extract(Lock,lock(),resource())))
r344: case6(Locks,Lock,Resource,true()) -> andt(equal(record_extract(Lock,lock(),excl()),nil()),equal(record_extract(Lock,lock(),pending()),nil()))
r345: case6(Locks,Lock,Resource,false()) -> locker2_check_available(Resource,Locks)
r346: locker2_check_availables(nil(),Locks) -> true()
r347: locker2_check_availables(cons(Resource,Resources),Locks) -> andt(locker2_check_available(Resource,Locks),locker2_check_availables(Resources,Locks))
r348: locker2_adduniq(nil(),List) -> List
r349: append(cons(Head,Tail),List) -> cons(Head,append(Tail,List))
r350: subtract(List,nil()) -> List
r351: subtract(List,cons(Head,Tail)) -> subtract(delete(Head,List),Tail)
r352: delete(E,nil()) -> nil()
r353: delete(E,cons(Head,Tail)) -> case8(Tail,Head,E,equal(E,Head))
r354: case8(Tail,Head,E,true()) -> Tail
r355: case8(Tail,Head,E,false()) -> cons(Head,delete(E,Tail))
r356: gen_tag(Pid) -> tuple(Pid,tuplenil(tag()))
r357: gen_modtageq(Client1,Client2) -> equal(Client1,Client2)
r358: member(E,nil()) -> false()
r359: member(E,cons(Head,Tail)) -> case9(Tail,Head,E,equal(E,Head))
r360: case9(Tail,Head,E,true()) -> true()
r361: case9(Tail,Head,E,false()) -> member(E,Tail)
r362: eqs(empty(),empty()) -> T()
r363: eqs(empty(),stack(E2,S2)) -> F()
r364: eqs(stack(E1,S1),empty()) -> F()
r365: eqs(stack(E1,S1),stack(E2,S2)) -> and(eqt(E1,E2),eqs(S1,S2))
r366: pushs(E1,S1) -> stack(E1,S1)
r367: pops(stack(E1,S1)) -> S1
r368: tops(stack(E1,S1)) -> E1
r369: istops(E1,empty()) -> F()
r370: istops(E1,stack(E2,S1)) -> eqt(E1,E2)
r371: eqc(nocalls(),nocalls()) -> T()
r372: eqc(nocalls(),calls(E2,S2,CS2)) -> F()
r373: eqc(calls(E1,S1,CS1),nocalls()) -> F()
r374: eqc(calls(E1,S1,CS1),calls(E2,S2,CS2)) -> and(eqt(E1,E2),and(eqs(S1,S2),eqc(CS1,CS2)))
r375: push(E1,E2,nocalls()) -> calls(E1,stack(E2,empty()),nocalls())
r376: push(E1,E2,calls(E3,S1,CS1)) -> push1(E1,E2,E3,S1,CS1,eqt(E1,E3))
r377: push1(E1,E2,E3,S1,CS1,T()) -> calls(E3,pushs(E2,S1),CS1)

The set of usable rules consists of

  r352, r353

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      subtract#_A(x1,x2) = ((1,0,0),(0,1,0),(1,0,0)) x1 + ((1,0,0),(1,1,0),(0,0,0)) x2
      cons_A(x1,x2) = ((1,0,0),(1,0,0),(1,1,0)) x1 + ((1,0,0),(1,0,0),(1,1,0)) x2 + (2,1,0)
      delete_A(x1,x2) = ((1,0,0),(1,0,0),(0,0,0)) x1 + x2 + (1,4,0)
      nil_A() = (1,5,1)
      case8_A(x1,x2,x3,x4) = ((1,0,0),(1,1,0),(0,0,0)) x4 + (0,3,1)
      equal_A(x1,x2) = ((1,0,0),(0,0,0),(1,1,0)) x1 + ((1,0,0),(1,1,0),(1,1,1)) x2 + (1,1,1)

The next rules are strictly ordered:

  p1

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: locker2_check_availables#(cons(Resource,Resources),Locks) -> locker2_check_availables#(Resources,Locks)

and R consists of:

r1: or(T(),T()) -> T()
r2: or(F(),T()) -> T()
r3: or(T(),F()) -> T()
r4: or(F(),F()) -> F()
r5: and(T(),B) -> B
r6: and(B,T()) -> B
r7: and(F(),B) -> F()
r8: and(B,F()) -> F()
r9: imp(T(),B) -> B
r10: imp(F(),B) -> T()
r11: not(T()) -> F()
r12: not(F()) -> T()
r13: if(T(),B1,B2) -> B1
r14: if(F(),B1,B2) -> B2
r15: eq(T(),T()) -> T()
r16: eq(F(),F()) -> T()
r17: eq(T(),F()) -> F()
r18: eq(F(),T()) -> F()
r19: eqt(nil(),undefined()) -> F()
r20: eqt(nil(),pid(N2)) -> F()
r21: eqt(nil(),int(N2)) -> F()
r22: eqt(nil(),cons(H2,T2)) -> F()
r23: eqt(nil(),tuple(H2,T2)) -> F()
r24: eqt(nil(),tuplenil(H2)) -> F()
r25: eqt(a(),nil()) -> F()
r26: eqt(a(),a()) -> T()
r27: eqt(a(),excl()) -> F()
r28: eqt(a(),false()) -> F()
r29: eqt(a(),lock()) -> F()
r30: eqt(a(),locker()) -> F()
r31: eqt(a(),mcrlrecord()) -> F()
r32: eqt(a(),ok()) -> F()
r33: eqt(a(),pending()) -> F()
r34: eqt(a(),release()) -> F()
r35: eqt(a(),request()) -> F()
r36: eqt(a(),resource()) -> F()
r37: eqt(a(),tag()) -> F()
r38: eqt(a(),true()) -> F()
r39: eqt(a(),undefined()) -> F()
r40: eqt(a(),pid(N2)) -> F()
r41: eqt(a(),int(N2)) -> F()
r42: eqt(a(),cons(H2,T2)) -> F()
r43: eqt(a(),tuple(H2,T2)) -> F()
r44: eqt(a(),tuplenil(H2)) -> F()
r45: eqt(excl(),nil()) -> F()
r46: eqt(excl(),a()) -> F()
r47: eqt(excl(),excl()) -> T()
r48: eqt(excl(),false()) -> F()
r49: eqt(excl(),lock()) -> F()
r50: eqt(excl(),locker()) -> F()
r51: eqt(excl(),mcrlrecord()) -> F()
r52: eqt(excl(),ok()) -> F()
r53: eqt(excl(),pending()) -> F()
r54: eqt(excl(),release()) -> F()
r55: eqt(excl(),request()) -> F()
r56: eqt(excl(),resource()) -> F()
r57: eqt(excl(),tag()) -> F()
r58: eqt(excl(),true()) -> F()
r59: eqt(excl(),undefined()) -> F()
r60: eqt(excl(),pid(N2)) -> F()
r61: eqt(excl(),eqt(false(),int(N2))) -> F()
r62: eqt(false(),cons(H2,T2)) -> F()
r63: eqt(false(),tuple(H2,T2)) -> F()
r64: eqt(false(),tuplenil(H2)) -> F()
r65: eqt(lock(),nil()) -> F()
r66: eqt(lock(),a()) -> F()
r67: eqt(lock(),excl()) -> F()
r68: eqt(lock(),false()) -> F()
r69: eqt(lock(),lock()) -> T()
r70: eqt(lock(),locker()) -> F()
r71: eqt(lock(),mcrlrecord()) -> F()
r72: eqt(lock(),ok()) -> F()
r73: eqt(lock(),pending()) -> F()
r74: eqt(lock(),release()) -> F()
r75: eqt(lock(),request()) -> F()
r76: eqt(lock(),resource()) -> F()
r77: eqt(lock(),tag()) -> F()
r78: eqt(lock(),true()) -> F()
r79: eqt(lock(),undefined()) -> F()
r80: eqt(lock(),pid(N2)) -> F()
r81: eqt(lock(),int(N2)) -> F()
r82: eqt(lock(),cons(H2,T2)) -> F()
r83: eqt(lock(),tuple(H2,T2)) -> F()
r84: eqt(lock(),tuplenil(H2)) -> F()
r85: eqt(locker(),nil()) -> F()
r86: eqt(locker(),a()) -> F()
r87: eqt(locker(),excl()) -> F()
r88: eqt(locker(),false()) -> F()
r89: eqt(locker(),lock()) -> F()
r90: eqt(locker(),locker()) -> T()
r91: eqt(locker(),mcrlrecord()) -> F()
r92: eqt(locker(),ok()) -> F()
r93: eqt(locker(),pending()) -> F()
r94: eqt(locker(),release()) -> F()
r95: eqt(locker(),request()) -> F()
r96: eqt(locker(),resource()) -> F()
r97: eqt(locker(),tag()) -> F()
r98: eqt(locker(),true()) -> F()
r99: eqt(locker(),undefined()) -> F()
r100: eqt(locker(),pid(N2)) -> F()
r101: eqt(locker(),int(N2)) -> F()
r102: eqt(locker(),cons(H2,T2)) -> F()
r103: eqt(locker(),tuple(H2,T2)) -> F()
r104: eqt(locker(),tuplenil(H2)) -> F()
r105: eqt(mcrlrecord(),nil()) -> F()
r106: eqt(mcrlrecord(),a()) -> F()
r107: eqt(mcrlrecord(),excl()) -> F()
r108: eqt(mcrlrecord(),false()) -> F()
r109: eqt(mcrlrecord(),lock()) -> F()
r110: eqt(mcrlrecord(),locker()) -> F()
r111: eqt(mcrlrecord(),mcrlrecord()) -> T()
r112: eqt(mcrlrecord(),ok()) -> F()
r113: eqt(mcrlrecord(),pending()) -> F()
r114: eqt(mcrlrecord(),release()) -> F()
r115: eqt(mcrlrecord(),request()) -> F()
r116: eqt(mcrlrecord(),resource()) -> F()
r117: eqt(ok(),resource()) -> F()
r118: eqt(ok(),tag()) -> F()
r119: eqt(ok(),true()) -> F()
r120: eqt(ok(),undefined()) -> F()
r121: eqt(ok(),pid(N2)) -> F()
r122: eqt(ok(),int(N2)) -> F()
r123: eqt(ok(),cons(H2,T2)) -> F()
r124: eqt(ok(),tuple(H2,T2)) -> F()
r125: eqt(ok(),tuplenil(H2)) -> F()
r126: eqt(pending(),nil()) -> F()
r127: eqt(pending(),a()) -> F()
r128: eqt(pending(),excl()) -> F()
r129: eqt(pending(),false()) -> F()
r130: eqt(pending(),lock()) -> F()
r131: eqt(pending(),locker()) -> F()
r132: eqt(pending(),mcrlrecord()) -> F()
r133: eqt(pending(),ok()) -> F()
r134: eqt(pending(),pending()) -> T()
r135: eqt(pending(),release()) -> F()
r136: eqt(pending(),request()) -> F()
r137: eqt(pending(),resource()) -> F()
r138: eqt(pending(),tag()) -> F()
r139: eqt(pending(),true()) -> F()
r140: eqt(pending(),undefined()) -> F()
r141: eqt(pending(),pid(N2)) -> F()
r142: eqt(pending(),int(N2)) -> F()
r143: eqt(pending(),cons(H2,T2)) -> F()
r144: eqt(pending(),tuple(H2,T2)) -> F()
r145: eqt(pending(),tuplenil(H2)) -> F()
r146: eqt(release(),nil()) -> F()
r147: eqt(release(),a()) -> F()
r148: eqt(release(),excl()) -> F()
r149: eqt(release(),false()) -> F()
r150: eqt(release(),lock()) -> F()
r151: eqt(release(),locker()) -> F()
r152: eqt(release(),mcrlrecord()) -> F()
r153: eqt(release(),ok()) -> F()
r154: eqt(request(),mcrlrecord()) -> F()
r155: eqt(request(),ok()) -> F()
r156: eqt(request(),pending()) -> F()
r157: eqt(request(),release()) -> F()
r158: eqt(request(),request()) -> T()
r159: eqt(request(),resource()) -> F()
r160: eqt(request(),tag()) -> F()
r161: eqt(request(),true()) -> F()
r162: eqt(request(),undefined()) -> F()
r163: eqt(request(),pid(N2)) -> F()
r164: eqt(request(),int(N2)) -> F()
r165: eqt(request(),cons(H2,T2)) -> F()
r166: eqt(request(),tuple(H2,T2)) -> F()
r167: eqt(request(),tuplenil(H2)) -> F()
r168: eqt(resource(),nil()) -> F()
r169: eqt(resource(),a()) -> F()
r170: eqt(resource(),excl()) -> F()
r171: eqt(resource(),false()) -> F()
r172: eqt(resource(),lock()) -> F()
r173: eqt(resource(),locker()) -> F()
r174: eqt(resource(),mcrlrecord()) -> F()
r175: eqt(resource(),ok()) -> F()
r176: eqt(resource(),pending()) -> F()
r177: eqt(resource(),release()) -> F()
r178: eqt(resource(),request()) -> F()
r179: eqt(resource(),resource()) -> T()
r180: eqt(resource(),tag()) -> F()
r181: eqt(resource(),true()) -> F()
r182: eqt(resource(),undefined()) -> F()
r183: eqt(resource(),pid(N2)) -> F()
r184: eqt(resource(),int(N2)) -> F()
r185: eqt(resource(),cons(H2,T2)) -> F()
r186: eqt(resource(),tuple(H2,T2)) -> F()
r187: eqt(resource(),tuplenil(H2)) -> F()
r188: eqt(tag(),nil()) -> F()
r189: eqt(tag(),a()) -> F()
r190: eqt(tag(),excl()) -> F()
r191: eqt(tag(),false()) -> F()
r192: eqt(tag(),lock()) -> F()
r193: eqt(tag(),locker()) -> F()
r194: eqt(tag(),mcrlrecord()) -> F()
r195: eqt(tag(),ok()) -> F()
r196: eqt(tag(),pending()) -> F()
r197: eqt(tag(),release()) -> F()
r198: eqt(tag(),request()) -> F()
r199: eqt(tag(),resource()) -> F()
r200: eqt(tag(),tag()) -> T()
r201: eqt(tag(),true()) -> F()
r202: eqt(tag(),undefined()) -> F()
r203: eqt(tag(),pid(N2)) -> F()
r204: eqt(tag(),int(N2)) -> F()
r205: eqt(tag(),cons(H2,T2)) -> F()
r206: eqt(tag(),tuple(H2,T2)) -> F()
r207: eqt(tag(),tuplenil(H2)) -> F()
r208: eqt(true(),nil()) -> F()
r209: eqt(true(),a()) -> F()
r210: eqt(true(),excl()) -> F()
r211: eqt(true(),false()) -> F()
r212: eqt(true(),lock()) -> F()
r213: eqt(true(),locker()) -> F()
r214: eqt(true(),mcrlrecord()) -> F()
r215: eqt(true(),ok()) -> F()
r216: eqt(true(),pending()) -> F()
r217: eqt(true(),release()) -> F()
r218: eqt(true(),request()) -> F()
r219: eqt(true(),resource()) -> F()
r220: eqt(true(),tag()) -> F()
r221: eqt(true(),true()) -> T()
r222: eqt(true(),undefined()) -> F()
r223: eqt(true(),pid(N2)) -> F()
r224: eqt(true(),int(N2)) -> F()
r225: eqt(true(),cons(H2,T2)) -> F()
r226: eqt(true(),tuple(H2,T2)) -> F()
r227: eqt(true(),tuplenil(H2)) -> F()
r228: eqt(undefined(),nil()) -> F()
r229: eqt(undefined(),a()) -> F()
r230: eqt(undefined(),tuplenil(H2)) -> F()
r231: eqt(pid(N1),nil()) -> F()
r232: eqt(pid(N1),a()) -> F()
r233: eqt(pid(N1),excl()) -> F()
r234: eqt(pid(N1),false()) -> F()
r235: eqt(pid(N1),lock()) -> F()
r236: eqt(pid(N1),locker()) -> F()
r237: eqt(pid(N1),mcrlrecord()) -> F()
r238: eqt(pid(N1),ok()) -> F()
r239: eqt(pid(N1),pending()) -> F()
r240: eqt(pid(N1),release()) -> F()
r241: eqt(pid(N1),request()) -> F()
r242: eqt(pid(N1),resource()) -> F()
r243: eqt(pid(N1),tag()) -> F()
r244: eqt(pid(N1),true()) -> F()
r245: eqt(pid(N1),undefined()) -> F()
r246: eqt(pid(N1),pid(N2)) -> eqt(N1,N2)
r247: eqt(pid(N1),int(N2)) -> F()
r248: eqt(pid(N1),cons(H2,T2)) -> F()
r249: eqt(pid(N1),tuple(H2,T2)) -> F()
r250: eqt(pid(N1),tuplenil(H2)) -> F()
r251: eqt(int(N1),nil()) -> F()
r252: eqt(int(N1),a()) -> F()
r253: eqt(int(N1),excl()) -> F()
r254: eqt(int(N1),false()) -> F()
r255: eqt(int(N1),lock()) -> F()
r256: eqt(int(N1),locker()) -> F()
r257: eqt(int(N1),mcrlrecord()) -> F()
r258: eqt(int(N1),ok()) -> F()
r259: eqt(int(N1),pending()) -> F()
r260: eqt(int(N1),release()) -> F()
r261: eqt(int(N1),request()) -> F()
r262: eqt(int(N1),resource()) -> F()
r263: eqt(int(N1),tag()) -> F()
r264: eqt(int(N1),true()) -> F()
r265: eqt(int(N1),undefined()) -> F()
r266: eqt(cons(H1,T1),resource()) -> F()
r267: eqt(cons(H1,T1),tag()) -> F()
r268: eqt(cons(H1,T1),true()) -> F()
r269: eqt(cons(H1,T1),undefined()) -> F()
r270: eqt(cons(H1,T1),pid(N2)) -> F()
r271: eqt(cons(H1,T1),int(N2)) -> F()
r272: eqt(cons(H1,T1),cons(H2,T2)) -> and(eqt(H1,H2),eqt(T1,T2))
r273: eqt(cons(H1,T1),tuple(H2,T2)) -> F()
r274: eqt(cons(H1,T1),tuplenil(H2)) -> F()
r275: eqt(tuple(H1,T1),nil()) -> F()
r276: eqt(tuple(H1,T1),a()) -> F()
r277: eqt(tuple(H1,T1),excl()) -> F()
r278: eqt(tuple(H1,T1),false()) -> F()
r279: eqt(tuple(H1,T1),lock()) -> F()
r280: eqt(tuple(H1,T1),locker()) -> F()
r281: eqt(tuple(H1,T1),mcrlrecord()) -> F()
r282: eqt(tuple(H1,T1),ok()) -> F()
r283: eqt(tuple(H1,T1),pending()) -> F()
r284: eqt(tuple(H1,T1),release()) -> F()
r285: eqt(tuple(H1,T1),request()) -> F()
r286: eqt(tuple(H1,T1),resource()) -> F()
r287: eqt(tuple(H1,T1),tag()) -> F()
r288: eqt(tuple(H1,T1),true()) -> F()
r289: eqt(tuple(H1,T1),undefined()) -> F()
r290: eqt(tuple(H1,T1),pid(N2)) -> F()
r291: eqt(tuple(H1,T1),int(N2)) -> F()
r292: eqt(tuple(H1,T1),cons(H2,T2)) -> F()
r293: eqt(tuple(H1,T1),tuple(H2,T2)) -> and(eqt(H1,H2),eqt(T1,T2))
r294: eqt(tuple(H1,T1),tuplenil(H2)) -> F()
r295: eqt(tuplenil(H1),nil()) -> F()
r296: eqt(tuplenil(H1),a()) -> F()
r297: eqt(tuplenil(H1),excl()) -> F()
r298: eqt(tuplenil(H1),false()) -> F()
r299: eqt(tuplenil(H1),lock()) -> F()
r300: eqt(tuplenil(H1),locker()) -> F()
r301: eqt(tuplenil(H1),mcrlrecord()) -> F()
r302: eqt(tuplenil(H1),ok()) -> F()
r303: eqt(tuplenil(H1),pending()) -> F()
r304: eqt(tuplenil(H1),release()) -> F()
r305: eqt(tuplenil(H1),request()) -> F()
r306: eqt(tuplenil(H1),resource()) -> F()
r307: eqt(tuplenil(H1),tag()) -> F()
r308: eqt(tuplenil(H1),true()) -> F()
r309: eqt(tuplenil(H1),undefined()) -> F()
r310: eqt(tuplenil(H1),pid(N2)) -> F()
r311: eqt(tuplenil(H1),int(N2)) -> F()
r312: eqt(tuplenil(H1),cons(H2,T2)) -> F()
r313: eqt(tuplenil(H1),tuple(H2,T2)) -> F()
r314: eqt(tuplenil(H1),tuplenil(H2)) -> eqt(H1,H2)
r315: element(int(s(|0|())),tuplenil(T1)) -> T1
r316: element(int(s(|0|())),tuple(T1,T2)) -> T1
r317: element(int(s(s(N1))),tuple(T1,T2)) -> element(int(s(N1)),T2)
r318: record_new(lock()) -> tuple(mcrlrecord(),tuple(lock(),tuple(undefined(),tuple(nil(),tuplenil(nil())))))
r319: record_extract(tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(F2))))),lock(),resource()) -> tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(F2)))))
r320: 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)))))
r321: record_updates(Record,Name,nil()) -> Record
r322: record_updates(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields)) -> record_updates(record_update(Record,Name,Field,NewF),Name,Fields)
r323: locker2_map_promote_pending(nil(),Pending) -> nil()
r324: locker2_map_promote_pending(cons(Lock,Locks),Pending) -> cons(locker2_promote_pending(Lock,Pending),locker2_map_promote_pending(Locks,Pending))
r325: locker2_map_claim_lock(nil(),Resources,Client) -> nil()
r326: locker2_map_claim_lock(cons(Lock,Locks),Resources,Client) -> cons(locker2_claim_lock(Lock,Resources,Client),locker2_map_claim_lock(Locks,Resources,Client))
r327: locker2_map_add_pending(nil(),Resources,Client) -> nil()
r328: locker2_promote_pending(Lock,Client) -> case0(Client,Lock,record_extract(Lock,lock(),pending()))
r329: case0(Client,Lock,cons(Client,Pendings)) -> record_updates(Lock,lock(),cons(tuple(excl(),tuplenil(Client)),cons(tuple(pending(),tuplenil(Pendings)),nil())))
r330: case0(Client,Lock,MCRLFree0) -> Lock
r331: locker2_remove_pending(Lock,Client) -> record_updates(Lock,lock(),cons(tuple(pending(),tuplenil(subtract(record_extract(Lock,lock(),pending()),cons(Client,nil())))),nil()))
r332: locker2_add_pending(Lock,Resources,Client) -> case1(Client,Resources,Lock,member(record_extract(Lock,lock(),resource()),Resources))
r333: case1(Client,Resources,Lock,true()) -> record_updates(Lock,lock(),cons(tuple(pending(),tuplenil(append(record_extract(Lock,lock(),pending()),cons(Client,nil())))),nil()))
r334: case1(Client,Resources,Lock,false()) -> Lock
r335: locker2_release_lock(Lock,Client) -> case2(Client,Lock,gen_modtageq(Client,record_extract(Lock,lock(),excl())))
r336: case2(Client,Lock,true()) -> record_updates(Lock,lock(),cons(tuple(excllock(),excl()),nil()))
r337: case4(Client,Lock,MCRLFree1) -> false()
r338: locker2_obtainables(nil(),Client) -> true()
r339: locker2_obtainables(cons(Lock,Locks),Client) -> case5(Client,Locks,Lock,member(Client,record_extract(Lock,lock(),pending())))
r340: case5(Client,Locks,Lock,true()) -> andt(locker2_obtainable(Lock,Client),locker2_obtainables(Locks,Client))
r341: case5(Client,Locks,Lock,false()) -> locker2_obtainables(Locks,Client)
r342: locker2_check_available(Resource,nil()) -> false()
r343: locker2_check_available(Resource,cons(Lock,Locks)) -> case6(Locks,Lock,Resource,equal(Resource,record_extract(Lock,lock(),resource())))
r344: case6(Locks,Lock,Resource,true()) -> andt(equal(record_extract(Lock,lock(),excl()),nil()),equal(record_extract(Lock,lock(),pending()),nil()))
r345: case6(Locks,Lock,Resource,false()) -> locker2_check_available(Resource,Locks)
r346: locker2_check_availables(nil(),Locks) -> true()
r347: locker2_check_availables(cons(Resource,Resources),Locks) -> andt(locker2_check_available(Resource,Locks),locker2_check_availables(Resources,Locks))
r348: locker2_adduniq(nil(),List) -> List
r349: append(cons(Head,Tail),List) -> cons(Head,append(Tail,List))
r350: subtract(List,nil()) -> List
r351: subtract(List,cons(Head,Tail)) -> subtract(delete(Head,List),Tail)
r352: delete(E,nil()) -> nil()
r353: delete(E,cons(Head,Tail)) -> case8(Tail,Head,E,equal(E,Head))
r354: case8(Tail,Head,E,true()) -> Tail
r355: case8(Tail,Head,E,false()) -> cons(Head,delete(E,Tail))
r356: gen_tag(Pid) -> tuple(Pid,tuplenil(tag()))
r357: gen_modtageq(Client1,Client2) -> equal(Client1,Client2)
r358: member(E,nil()) -> false()
r359: member(E,cons(Head,Tail)) -> case9(Tail,Head,E,equal(E,Head))
r360: case9(Tail,Head,E,true()) -> true()
r361: case9(Tail,Head,E,false()) -> member(E,Tail)
r362: eqs(empty(),empty()) -> T()
r363: eqs(empty(),stack(E2,S2)) -> F()
r364: eqs(stack(E1,S1),empty()) -> F()
r365: eqs(stack(E1,S1),stack(E2,S2)) -> and(eqt(E1,E2),eqs(S1,S2))
r366: pushs(E1,S1) -> stack(E1,S1)
r367: pops(stack(E1,S1)) -> S1
r368: tops(stack(E1,S1)) -> E1
r369: istops(E1,empty()) -> F()
r370: istops(E1,stack(E2,S1)) -> eqt(E1,E2)
r371: eqc(nocalls(),nocalls()) -> T()
r372: eqc(nocalls(),calls(E2,S2,CS2)) -> F()
r373: eqc(calls(E1,S1,CS1),nocalls()) -> F()
r374: eqc(calls(E1,S1,CS1),calls(E2,S2,CS2)) -> and(eqt(E1,E2),and(eqs(S1,S2),eqc(CS1,CS2)))
r375: push(E1,E2,nocalls()) -> calls(E1,stack(E2,empty()),nocalls())
r376: push(E1,E2,calls(E3,S1,CS1)) -> push1(E1,E2,E3,S1,CS1,eqt(E1,E3))
r377: push1(E1,E2,E3,S1,CS1,T()) -> calls(E3,pushs(E2,S1),CS1)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      locker2_check_availables#_A(x1,x2) = ((0,0,0),(1,0,0),(1,1,0)) x1 + ((1,0,0),(0,1,0),(0,1,1)) x2
      cons_A(x1,x2) = ((1,0,0),(1,1,0),(1,1,1)) x1 + ((1,0,0),(1,1,0),(1,1,1)) x2 + (1,1,1)

The next rules are strictly ordered:

  p1

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: append#(cons(Head,Tail),List) -> append#(Tail,List)

and R consists of:

r1: or(T(),T()) -> T()
r2: or(F(),T()) -> T()
r3: or(T(),F()) -> T()
r4: or(F(),F()) -> F()
r5: and(T(),B) -> B
r6: and(B,T()) -> B
r7: and(F(),B) -> F()
r8: and(B,F()) -> F()
r9: imp(T(),B) -> B
r10: imp(F(),B) -> T()
r11: not(T()) -> F()
r12: not(F()) -> T()
r13: if(T(),B1,B2) -> B1
r14: if(F(),B1,B2) -> B2
r15: eq(T(),T()) -> T()
r16: eq(F(),F()) -> T()
r17: eq(T(),F()) -> F()
r18: eq(F(),T()) -> F()
r19: eqt(nil(),undefined()) -> F()
r20: eqt(nil(),pid(N2)) -> F()
r21: eqt(nil(),int(N2)) -> F()
r22: eqt(nil(),cons(H2,T2)) -> F()
r23: eqt(nil(),tuple(H2,T2)) -> F()
r24: eqt(nil(),tuplenil(H2)) -> F()
r25: eqt(a(),nil()) -> F()
r26: eqt(a(),a()) -> T()
r27: eqt(a(),excl()) -> F()
r28: eqt(a(),false()) -> F()
r29: eqt(a(),lock()) -> F()
r30: eqt(a(),locker()) -> F()
r31: eqt(a(),mcrlrecord()) -> F()
r32: eqt(a(),ok()) -> F()
r33: eqt(a(),pending()) -> F()
r34: eqt(a(),release()) -> F()
r35: eqt(a(),request()) -> F()
r36: eqt(a(),resource()) -> F()
r37: eqt(a(),tag()) -> F()
r38: eqt(a(),true()) -> F()
r39: eqt(a(),undefined()) -> F()
r40: eqt(a(),pid(N2)) -> F()
r41: eqt(a(),int(N2)) -> F()
r42: eqt(a(),cons(H2,T2)) -> F()
r43: eqt(a(),tuple(H2,T2)) -> F()
r44: eqt(a(),tuplenil(H2)) -> F()
r45: eqt(excl(),nil()) -> F()
r46: eqt(excl(),a()) -> F()
r47: eqt(excl(),excl()) -> T()
r48: eqt(excl(),false()) -> F()
r49: eqt(excl(),lock()) -> F()
r50: eqt(excl(),locker()) -> F()
r51: eqt(excl(),mcrlrecord()) -> F()
r52: eqt(excl(),ok()) -> F()
r53: eqt(excl(),pending()) -> F()
r54: eqt(excl(),release()) -> F()
r55: eqt(excl(),request()) -> F()
r56: eqt(excl(),resource()) -> F()
r57: eqt(excl(),tag()) -> F()
r58: eqt(excl(),true()) -> F()
r59: eqt(excl(),undefined()) -> F()
r60: eqt(excl(),pid(N2)) -> F()
r61: eqt(excl(),eqt(false(),int(N2))) -> F()
r62: eqt(false(),cons(H2,T2)) -> F()
r63: eqt(false(),tuple(H2,T2)) -> F()
r64: eqt(false(),tuplenil(H2)) -> F()
r65: eqt(lock(),nil()) -> F()
r66: eqt(lock(),a()) -> F()
r67: eqt(lock(),excl()) -> F()
r68: eqt(lock(),false()) -> F()
r69: eqt(lock(),lock()) -> T()
r70: eqt(lock(),locker()) -> F()
r71: eqt(lock(),mcrlrecord()) -> F()
r72: eqt(lock(),ok()) -> F()
r73: eqt(lock(),pending()) -> F()
r74: eqt(lock(),release()) -> F()
r75: eqt(lock(),request()) -> F()
r76: eqt(lock(),resource()) -> F()
r77: eqt(lock(),tag()) -> F()
r78: eqt(lock(),true()) -> F()
r79: eqt(lock(),undefined()) -> F()
r80: eqt(lock(),pid(N2)) -> F()
r81: eqt(lock(),int(N2)) -> F()
r82: eqt(lock(),cons(H2,T2)) -> F()
r83: eqt(lock(),tuple(H2,T2)) -> F()
r84: eqt(lock(),tuplenil(H2)) -> F()
r85: eqt(locker(),nil()) -> F()
r86: eqt(locker(),a()) -> F()
r87: eqt(locker(),excl()) -> F()
r88: eqt(locker(),false()) -> F()
r89: eqt(locker(),lock()) -> F()
r90: eqt(locker(),locker()) -> T()
r91: eqt(locker(),mcrlrecord()) -> F()
r92: eqt(locker(),ok()) -> F()
r93: eqt(locker(),pending()) -> F()
r94: eqt(locker(),release()) -> F()
r95: eqt(locker(),request()) -> F()
r96: eqt(locker(),resource()) -> F()
r97: eqt(locker(),tag()) -> F()
r98: eqt(locker(),true()) -> F()
r99: eqt(locker(),undefined()) -> F()
r100: eqt(locker(),pid(N2)) -> F()
r101: eqt(locker(),int(N2)) -> F()
r102: eqt(locker(),cons(H2,T2)) -> F()
r103: eqt(locker(),tuple(H2,T2)) -> F()
r104: eqt(locker(),tuplenil(H2)) -> F()
r105: eqt(mcrlrecord(),nil()) -> F()
r106: eqt(mcrlrecord(),a()) -> F()
r107: eqt(mcrlrecord(),excl()) -> F()
r108: eqt(mcrlrecord(),false()) -> F()
r109: eqt(mcrlrecord(),lock()) -> F()
r110: eqt(mcrlrecord(),locker()) -> F()
r111: eqt(mcrlrecord(),mcrlrecord()) -> T()
r112: eqt(mcrlrecord(),ok()) -> F()
r113: eqt(mcrlrecord(),pending()) -> F()
r114: eqt(mcrlrecord(),release()) -> F()
r115: eqt(mcrlrecord(),request()) -> F()
r116: eqt(mcrlrecord(),resource()) -> F()
r117: eqt(ok(),resource()) -> F()
r118: eqt(ok(),tag()) -> F()
r119: eqt(ok(),true()) -> F()
r120: eqt(ok(),undefined()) -> F()
r121: eqt(ok(),pid(N2)) -> F()
r122: eqt(ok(),int(N2)) -> F()
r123: eqt(ok(),cons(H2,T2)) -> F()
r124: eqt(ok(),tuple(H2,T2)) -> F()
r125: eqt(ok(),tuplenil(H2)) -> F()
r126: eqt(pending(),nil()) -> F()
r127: eqt(pending(),a()) -> F()
r128: eqt(pending(),excl()) -> F()
r129: eqt(pending(),false()) -> F()
r130: eqt(pending(),lock()) -> F()
r131: eqt(pending(),locker()) -> F()
r132: eqt(pending(),mcrlrecord()) -> F()
r133: eqt(pending(),ok()) -> F()
r134: eqt(pending(),pending()) -> T()
r135: eqt(pending(),release()) -> F()
r136: eqt(pending(),request()) -> F()
r137: eqt(pending(),resource()) -> F()
r138: eqt(pending(),tag()) -> F()
r139: eqt(pending(),true()) -> F()
r140: eqt(pending(),undefined()) -> F()
r141: eqt(pending(),pid(N2)) -> F()
r142: eqt(pending(),int(N2)) -> F()
r143: eqt(pending(),cons(H2,T2)) -> F()
r144: eqt(pending(),tuple(H2,T2)) -> F()
r145: eqt(pending(),tuplenil(H2)) -> F()
r146: eqt(release(),nil()) -> F()
r147: eqt(release(),a()) -> F()
r148: eqt(release(),excl()) -> F()
r149: eqt(release(),false()) -> F()
r150: eqt(release(),lock()) -> F()
r151: eqt(release(),locker()) -> F()
r152: eqt(release(),mcrlrecord()) -> F()
r153: eqt(release(),ok()) -> F()
r154: eqt(request(),mcrlrecord()) -> F()
r155: eqt(request(),ok()) -> F()
r156: eqt(request(),pending()) -> F()
r157: eqt(request(),release()) -> F()
r158: eqt(request(),request()) -> T()
r159: eqt(request(),resource()) -> F()
r160: eqt(request(),tag()) -> F()
r161: eqt(request(),true()) -> F()
r162: eqt(request(),undefined()) -> F()
r163: eqt(request(),pid(N2)) -> F()
r164: eqt(request(),int(N2)) -> F()
r165: eqt(request(),cons(H2,T2)) -> F()
r166: eqt(request(),tuple(H2,T2)) -> F()
r167: eqt(request(),tuplenil(H2)) -> F()
r168: eqt(resource(),nil()) -> F()
r169: eqt(resource(),a()) -> F()
r170: eqt(resource(),excl()) -> F()
r171: eqt(resource(),false()) -> F()
r172: eqt(resource(),lock()) -> F()
r173: eqt(resource(),locker()) -> F()
r174: eqt(resource(),mcrlrecord()) -> F()
r175: eqt(resource(),ok()) -> F()
r176: eqt(resource(),pending()) -> F()
r177: eqt(resource(),release()) -> F()
r178: eqt(resource(),request()) -> F()
r179: eqt(resource(),resource()) -> T()
r180: eqt(resource(),tag()) -> F()
r181: eqt(resource(),true()) -> F()
r182: eqt(resource(),undefined()) -> F()
r183: eqt(resource(),pid(N2)) -> F()
r184: eqt(resource(),int(N2)) -> F()
r185: eqt(resource(),cons(H2,T2)) -> F()
r186: eqt(resource(),tuple(H2,T2)) -> F()
r187: eqt(resource(),tuplenil(H2)) -> F()
r188: eqt(tag(),nil()) -> F()
r189: eqt(tag(),a()) -> F()
r190: eqt(tag(),excl()) -> F()
r191: eqt(tag(),false()) -> F()
r192: eqt(tag(),lock()) -> F()
r193: eqt(tag(),locker()) -> F()
r194: eqt(tag(),mcrlrecord()) -> F()
r195: eqt(tag(),ok()) -> F()
r196: eqt(tag(),pending()) -> F()
r197: eqt(tag(),release()) -> F()
r198: eqt(tag(),request()) -> F()
r199: eqt(tag(),resource()) -> F()
r200: eqt(tag(),tag()) -> T()
r201: eqt(tag(),true()) -> F()
r202: eqt(tag(),undefined()) -> F()
r203: eqt(tag(),pid(N2)) -> F()
r204: eqt(tag(),int(N2)) -> F()
r205: eqt(tag(),cons(H2,T2)) -> F()
r206: eqt(tag(),tuple(H2,T2)) -> F()
r207: eqt(tag(),tuplenil(H2)) -> F()
r208: eqt(true(),nil()) -> F()
r209: eqt(true(),a()) -> F()
r210: eqt(true(),excl()) -> F()
r211: eqt(true(),false()) -> F()
r212: eqt(true(),lock()) -> F()
r213: eqt(true(),locker()) -> F()
r214: eqt(true(),mcrlrecord()) -> F()
r215: eqt(true(),ok()) -> F()
r216: eqt(true(),pending()) -> F()
r217: eqt(true(),release()) -> F()
r218: eqt(true(),request()) -> F()
r219: eqt(true(),resource()) -> F()
r220: eqt(true(),tag()) -> F()
r221: eqt(true(),true()) -> T()
r222: eqt(true(),undefined()) -> F()
r223: eqt(true(),pid(N2)) -> F()
r224: eqt(true(),int(N2)) -> F()
r225: eqt(true(),cons(H2,T2)) -> F()
r226: eqt(true(),tuple(H2,T2)) -> F()
r227: eqt(true(),tuplenil(H2)) -> F()
r228: eqt(undefined(),nil()) -> F()
r229: eqt(undefined(),a()) -> F()
r230: eqt(undefined(),tuplenil(H2)) -> F()
r231: eqt(pid(N1),nil()) -> F()
r232: eqt(pid(N1),a()) -> F()
r233: eqt(pid(N1),excl()) -> F()
r234: eqt(pid(N1),false()) -> F()
r235: eqt(pid(N1),lock()) -> F()
r236: eqt(pid(N1),locker()) -> F()
r237: eqt(pid(N1),mcrlrecord()) -> F()
r238: eqt(pid(N1),ok()) -> F()
r239: eqt(pid(N1),pending()) -> F()
r240: eqt(pid(N1),release()) -> F()
r241: eqt(pid(N1),request()) -> F()
r242: eqt(pid(N1),resource()) -> F()
r243: eqt(pid(N1),tag()) -> F()
r244: eqt(pid(N1),true()) -> F()
r245: eqt(pid(N1),undefined()) -> F()
r246: eqt(pid(N1),pid(N2)) -> eqt(N1,N2)
r247: eqt(pid(N1),int(N2)) -> F()
r248: eqt(pid(N1),cons(H2,T2)) -> F()
r249: eqt(pid(N1),tuple(H2,T2)) -> F()
r250: eqt(pid(N1),tuplenil(H2)) -> F()
r251: eqt(int(N1),nil()) -> F()
r252: eqt(int(N1),a()) -> F()
r253: eqt(int(N1),excl()) -> F()
r254: eqt(int(N1),false()) -> F()
r255: eqt(int(N1),lock()) -> F()
r256: eqt(int(N1),locker()) -> F()
r257: eqt(int(N1),mcrlrecord()) -> F()
r258: eqt(int(N1),ok()) -> F()
r259: eqt(int(N1),pending()) -> F()
r260: eqt(int(N1),release()) -> F()
r261: eqt(int(N1),request()) -> F()
r262: eqt(int(N1),resource()) -> F()
r263: eqt(int(N1),tag()) -> F()
r264: eqt(int(N1),true()) -> F()
r265: eqt(int(N1),undefined()) -> F()
r266: eqt(cons(H1,T1),resource()) -> F()
r267: eqt(cons(H1,T1),tag()) -> F()
r268: eqt(cons(H1,T1),true()) -> F()
r269: eqt(cons(H1,T1),undefined()) -> F()
r270: eqt(cons(H1,T1),pid(N2)) -> F()
r271: eqt(cons(H1,T1),int(N2)) -> F()
r272: eqt(cons(H1,T1),cons(H2,T2)) -> and(eqt(H1,H2),eqt(T1,T2))
r273: eqt(cons(H1,T1),tuple(H2,T2)) -> F()
r274: eqt(cons(H1,T1),tuplenil(H2)) -> F()
r275: eqt(tuple(H1,T1),nil()) -> F()
r276: eqt(tuple(H1,T1),a()) -> F()
r277: eqt(tuple(H1,T1),excl()) -> F()
r278: eqt(tuple(H1,T1),false()) -> F()
r279: eqt(tuple(H1,T1),lock()) -> F()
r280: eqt(tuple(H1,T1),locker()) -> F()
r281: eqt(tuple(H1,T1),mcrlrecord()) -> F()
r282: eqt(tuple(H1,T1),ok()) -> F()
r283: eqt(tuple(H1,T1),pending()) -> F()
r284: eqt(tuple(H1,T1),release()) -> F()
r285: eqt(tuple(H1,T1),request()) -> F()
r286: eqt(tuple(H1,T1),resource()) -> F()
r287: eqt(tuple(H1,T1),tag()) -> F()
r288: eqt(tuple(H1,T1),true()) -> F()
r289: eqt(tuple(H1,T1),undefined()) -> F()
r290: eqt(tuple(H1,T1),pid(N2)) -> F()
r291: eqt(tuple(H1,T1),int(N2)) -> F()
r292: eqt(tuple(H1,T1),cons(H2,T2)) -> F()
r293: eqt(tuple(H1,T1),tuple(H2,T2)) -> and(eqt(H1,H2),eqt(T1,T2))
r294: eqt(tuple(H1,T1),tuplenil(H2)) -> F()
r295: eqt(tuplenil(H1),nil()) -> F()
r296: eqt(tuplenil(H1),a()) -> F()
r297: eqt(tuplenil(H1),excl()) -> F()
r298: eqt(tuplenil(H1),false()) -> F()
r299: eqt(tuplenil(H1),lock()) -> F()
r300: eqt(tuplenil(H1),locker()) -> F()
r301: eqt(tuplenil(H1),mcrlrecord()) -> F()
r302: eqt(tuplenil(H1),ok()) -> F()
r303: eqt(tuplenil(H1),pending()) -> F()
r304: eqt(tuplenil(H1),release()) -> F()
r305: eqt(tuplenil(H1),request()) -> F()
r306: eqt(tuplenil(H1),resource()) -> F()
r307: eqt(tuplenil(H1),tag()) -> F()
r308: eqt(tuplenil(H1),true()) -> F()
r309: eqt(tuplenil(H1),undefined()) -> F()
r310: eqt(tuplenil(H1),pid(N2)) -> F()
r311: eqt(tuplenil(H1),int(N2)) -> F()
r312: eqt(tuplenil(H1),cons(H2,T2)) -> F()
r313: eqt(tuplenil(H1),tuple(H2,T2)) -> F()
r314: eqt(tuplenil(H1),tuplenil(H2)) -> eqt(H1,H2)
r315: element(int(s(|0|())),tuplenil(T1)) -> T1
r316: element(int(s(|0|())),tuple(T1,T2)) -> T1
r317: element(int(s(s(N1))),tuple(T1,T2)) -> element(int(s(N1)),T2)
r318: record_new(lock()) -> tuple(mcrlrecord(),tuple(lock(),tuple(undefined(),tuple(nil(),tuplenil(nil())))))
r319: record_extract(tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(F2))))),lock(),resource()) -> tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(F2)))))
r320: 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)))))
r321: record_updates(Record,Name,nil()) -> Record
r322: record_updates(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields)) -> record_updates(record_update(Record,Name,Field,NewF),Name,Fields)
r323: locker2_map_promote_pending(nil(),Pending) -> nil()
r324: locker2_map_promote_pending(cons(Lock,Locks),Pending) -> cons(locker2_promote_pending(Lock,Pending),locker2_map_promote_pending(Locks,Pending))
r325: locker2_map_claim_lock(nil(),Resources,Client) -> nil()
r326: locker2_map_claim_lock(cons(Lock,Locks),Resources,Client) -> cons(locker2_claim_lock(Lock,Resources,Client),locker2_map_claim_lock(Locks,Resources,Client))
r327: locker2_map_add_pending(nil(),Resources,Client) -> nil()
r328: locker2_promote_pending(Lock,Client) -> case0(Client,Lock,record_extract(Lock,lock(),pending()))
r329: case0(Client,Lock,cons(Client,Pendings)) -> record_updates(Lock,lock(),cons(tuple(excl(),tuplenil(Client)),cons(tuple(pending(),tuplenil(Pendings)),nil())))
r330: case0(Client,Lock,MCRLFree0) -> Lock
r331: locker2_remove_pending(Lock,Client) -> record_updates(Lock,lock(),cons(tuple(pending(),tuplenil(subtract(record_extract(Lock,lock(),pending()),cons(Client,nil())))),nil()))
r332: locker2_add_pending(Lock,Resources,Client) -> case1(Client,Resources,Lock,member(record_extract(Lock,lock(),resource()),Resources))
r333: case1(Client,Resources,Lock,true()) -> record_updates(Lock,lock(),cons(tuple(pending(),tuplenil(append(record_extract(Lock,lock(),pending()),cons(Client,nil())))),nil()))
r334: case1(Client,Resources,Lock,false()) -> Lock
r335: locker2_release_lock(Lock,Client) -> case2(Client,Lock,gen_modtageq(Client,record_extract(Lock,lock(),excl())))
r336: case2(Client,Lock,true()) -> record_updates(Lock,lock(),cons(tuple(excllock(),excl()),nil()))
r337: case4(Client,Lock,MCRLFree1) -> false()
r338: locker2_obtainables(nil(),Client) -> true()
r339: locker2_obtainables(cons(Lock,Locks),Client) -> case5(Client,Locks,Lock,member(Client,record_extract(Lock,lock(),pending())))
r340: case5(Client,Locks,Lock,true()) -> andt(locker2_obtainable(Lock,Client),locker2_obtainables(Locks,Client))
r341: case5(Client,Locks,Lock,false()) -> locker2_obtainables(Locks,Client)
r342: locker2_check_available(Resource,nil()) -> false()
r343: locker2_check_available(Resource,cons(Lock,Locks)) -> case6(Locks,Lock,Resource,equal(Resource,record_extract(Lock,lock(),resource())))
r344: case6(Locks,Lock,Resource,true()) -> andt(equal(record_extract(Lock,lock(),excl()),nil()),equal(record_extract(Lock,lock(),pending()),nil()))
r345: case6(Locks,Lock,Resource,false()) -> locker2_check_available(Resource,Locks)
r346: locker2_check_availables(nil(),Locks) -> true()
r347: locker2_check_availables(cons(Resource,Resources),Locks) -> andt(locker2_check_available(Resource,Locks),locker2_check_availables(Resources,Locks))
r348: locker2_adduniq(nil(),List) -> List
r349: append(cons(Head,Tail),List) -> cons(Head,append(Tail,List))
r350: subtract(List,nil()) -> List
r351: subtract(List,cons(Head,Tail)) -> subtract(delete(Head,List),Tail)
r352: delete(E,nil()) -> nil()
r353: delete(E,cons(Head,Tail)) -> case8(Tail,Head,E,equal(E,Head))
r354: case8(Tail,Head,E,true()) -> Tail
r355: case8(Tail,Head,E,false()) -> cons(Head,delete(E,Tail))
r356: gen_tag(Pid) -> tuple(Pid,tuplenil(tag()))
r357: gen_modtageq(Client1,Client2) -> equal(Client1,Client2)
r358: member(E,nil()) -> false()
r359: member(E,cons(Head,Tail)) -> case9(Tail,Head,E,equal(E,Head))
r360: case9(Tail,Head,E,true()) -> true()
r361: case9(Tail,Head,E,false()) -> member(E,Tail)
r362: eqs(empty(),empty()) -> T()
r363: eqs(empty(),stack(E2,S2)) -> F()
r364: eqs(stack(E1,S1),empty()) -> F()
r365: eqs(stack(E1,S1),stack(E2,S2)) -> and(eqt(E1,E2),eqs(S1,S2))
r366: pushs(E1,S1) -> stack(E1,S1)
r367: pops(stack(E1,S1)) -> S1
r368: tops(stack(E1,S1)) -> E1
r369: istops(E1,empty()) -> F()
r370: istops(E1,stack(E2,S1)) -> eqt(E1,E2)
r371: eqc(nocalls(),nocalls()) -> T()
r372: eqc(nocalls(),calls(E2,S2,CS2)) -> F()
r373: eqc(calls(E1,S1,CS1),nocalls()) -> F()
r374: eqc(calls(E1,S1,CS1),calls(E2,S2,CS2)) -> and(eqt(E1,E2),and(eqs(S1,S2),eqc(CS1,CS2)))
r375: push(E1,E2,nocalls()) -> calls(E1,stack(E2,empty()),nocalls())
r376: push(E1,E2,calls(E3,S1,CS1)) -> push1(E1,E2,E3,S1,CS1,eqt(E1,E3))
r377: push1(E1,E2,E3,S1,CS1,T()) -> calls(E3,pushs(E2,S1),CS1)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      append#_A(x1,x2) = ((0,0,0),(1,0,0),(1,1,0)) x1 + ((1,0,0),(0,1,0),(0,1,1)) x2
      cons_A(x1,x2) = ((1,0,0),(1,1,0),(1,1,1)) x1 + ((1,0,0),(1,1,0),(1,1,1)) x2 + (1,1,1)

The next rules are strictly ordered:

  p1

We remove them from the problem.  Then no dependency pair remains.