YES Problem: 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) Proof: DP Processor: DPs: eqt#(pid(N1),pid(N2)) -> eqt#(N1,N2) eqt#(cons(H1,T1),cons(H2,T2)) -> eqt#(T1,T2) eqt#(cons(H1,T1),cons(H2,T2)) -> eqt#(H1,H2) eqt#(cons(H1,T1),cons(H2,T2)) -> and#(eqt(H1,H2),eqt(T1,T2)) eqt#(tuple(H1,T1),tuple(H2,T2)) -> eqt#(T1,T2) eqt#(tuple(H1,T1),tuple(H2,T2)) -> eqt#(H1,H2) eqt#(tuple(H1,T1),tuple(H2,T2)) -> and#(eqt(H1,H2),eqt(T1,T2)) eqt#(tuplenil(H1),tuplenil(H2)) -> eqt#(H1,H2) element#(int(s(s(N1))),tuple(T1,T2)) -> element#(int(s(N1)),T2) record_updates#(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields)) -> record_update#(Record,Name,Field,NewF) record_updates#(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields)) -> record_updates#(record_update(Record,Name,Field,NewF),Name,Fields) locker2_map_promote_pending#(cons(Lock,Locks),Pending) -> locker2_map_promote_pending#(Locks,Pending) locker2_map_promote_pending#(cons(Lock,Locks),Pending) -> locker2_promote_pending#(Lock,Pending) locker2_map_claim_lock#(cons(Lock,Locks),Resources,Client) -> locker2_map_claim_lock#(Locks,Resources,Client) locker2_promote_pending#(Lock,Client) -> record_extract#(Lock,lock(),pending()) 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 ()))) locker2_remove_pending#(Lock,Client) -> record_extract#(Lock,lock(),pending()) locker2_remove_pending#(Lock,Client) -> subtract#(record_extract(Lock,lock(),pending()),cons(Client,nil())) 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) -> record_extract#(Lock,lock(),resource()) locker2_add_pending#(Lock,Resources,Client) -> member#(record_extract(Lock,lock(),resource()),Resources) locker2_add_pending#(Lock,Resources,Client) -> case1#(Client,Resources,Lock,member(record_extract(Lock,lock(),resource()),Resources)) case1#(Client,Resources,Lock,true()) -> record_extract#(Lock,lock(),pending()) case1#(Client,Resources,Lock,true()) -> append#(record_extract(Lock,lock(),pending()),cons(Client,nil())) case1#(Client,Resources,Lock,true()) -> record_updates#(Lock,lock(),cons(tuple(pending(),tuplenil(append(record_extract ( Lock,lock(),pending()), cons (Client,nil())))), nil())) locker2_release_lock#(Lock,Client) -> record_extract#(Lock,lock(),excl()) locker2_release_lock#(Lock,Client) -> gen_modtageq#(Client,record_extract(Lock,lock(),excl())) 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())) locker2_obtainables#(cons(Lock,Locks),Client) -> record_extract#(Lock,lock(),pending()) locker2_obtainables#(cons(Lock,Locks),Client) -> member#(Client,record_extract(Lock,lock(),pending())) locker2_obtainables#(cons(Lock,Locks),Client) -> case5#(Client,Locks,Lock,member(Client,record_extract(Lock,lock(),pending()))) case5#(Client,Locks,Lock,true()) -> locker2_obtainables#(Locks,Client) case5#(Client,Locks,Lock,false()) -> locker2_obtainables#(Locks,Client) locker2_check_available#(Resource,cons(Lock,Locks)) -> record_extract#(Lock,lock(),resource()) locker2_check_available#(Resource,cons(Lock,Locks)) -> case6#(Locks,Lock,Resource,equal(Resource,record_extract(Lock,lock(),resource()))) case6#(Locks,Lock,Resource,true()) -> record_extract#(Lock,lock(),pending()) case6#(Locks,Lock,Resource,true()) -> record_extract#(Lock,lock(),excl()) case6#(Locks,Lock,Resource,false()) -> locker2_check_available#(Resource,Locks) locker2_check_availables#(cons(Resource,Resources),Locks) -> locker2_check_availables#(Resources,Locks) locker2_check_availables#(cons(Resource,Resources),Locks) -> locker2_check_available#(Resource,Locks) append#(cons(Head,Tail),List) -> append#(Tail,List) subtract#(List,cons(Head,Tail)) -> delete#(Head,List) subtract#(List,cons(Head,Tail)) -> subtract#(delete(Head,List),Tail) delete#(E,cons(Head,Tail)) -> case8#(Tail,Head,E,equal(E,Head)) case8#(Tail,Head,E,false()) -> delete#(E,Tail) member#(E,cons(Head,Tail)) -> case9#(Tail,Head,E,equal(E,Head)) case9#(Tail,Head,E,false()) -> member#(E,Tail) eqs#(stack(E1,S1),stack(E2,S2)) -> eqs#(S1,S2) eqs#(stack(E1,S1),stack(E2,S2)) -> eqt#(E1,E2) eqs#(stack(E1,S1),stack(E2,S2)) -> and#(eqt(E1,E2),eqs(S1,S2)) istops#(E1,stack(E2,S1)) -> eqt#(E1,E2) eqc#(calls(E1,S1,CS1),calls(E2,S2,CS2)) -> eqc#(CS1,CS2) eqc#(calls(E1,S1,CS1),calls(E2,S2,CS2)) -> eqs#(S1,S2) eqc#(calls(E1,S1,CS1),calls(E2,S2,CS2)) -> and#(eqs(S1,S2),eqc(CS1,CS2)) eqc#(calls(E1,S1,CS1),calls(E2,S2,CS2)) -> eqt#(E1,E2) eqc#(calls(E1,S1,CS1),calls(E2,S2,CS2)) -> and#(eqt(E1,E2),and(eqs(S1,S2),eqc(CS1,CS2))) push#(E1,E2,calls(E3,S1,CS1)) -> eqt#(E1,E3) push#(E1,E2,calls(E3,S1,CS1)) -> push1#(E1,E2,E3,S1,CS1,eqt(E1,E3)) push1#(E1,E2,E3,S1,CS1,T()) -> pushs#(E2,S1) TRS: 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) Usable Rule Processor: DPs: eqt#(pid(N1),pid(N2)) -> eqt#(N1,N2) eqt#(cons(H1,T1),cons(H2,T2)) -> eqt#(T1,T2) eqt#(cons(H1,T1),cons(H2,T2)) -> eqt#(H1,H2) eqt#(cons(H1,T1),cons(H2,T2)) -> and#(eqt(H1,H2),eqt(T1,T2)) eqt#(tuple(H1,T1),tuple(H2,T2)) -> eqt#(T1,T2) eqt#(tuple(H1,T1),tuple(H2,T2)) -> eqt#(H1,H2) eqt#(tuple(H1,T1),tuple(H2,T2)) -> and#(eqt(H1,H2),eqt(T1,T2)) eqt#(tuplenil(H1),tuplenil(H2)) -> eqt#(H1,H2) element#(int(s(s(N1))),tuple(T1,T2)) -> element#(int(s(N1)),T2) record_updates#(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields)) -> record_update#(Record,Name,Field,NewF) record_updates#(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields)) -> record_updates#(record_update(Record,Name,Field,NewF),Name,Fields) locker2_map_promote_pending#(cons(Lock,Locks),Pending) -> locker2_map_promote_pending#(Locks,Pending) locker2_map_promote_pending#(cons(Lock,Locks),Pending) -> locker2_promote_pending#(Lock,Pending) locker2_map_claim_lock#(cons(Lock,Locks),Resources,Client) -> locker2_map_claim_lock#(Locks,Resources,Client) locker2_promote_pending#(Lock,Client) -> record_extract#(Lock,lock(),pending()) 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 ()))) locker2_remove_pending#(Lock,Client) -> record_extract#(Lock,lock(),pending()) locker2_remove_pending#(Lock,Client) -> subtract#(record_extract(Lock,lock(),pending()),cons(Client,nil())) 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) -> record_extract#(Lock,lock(),resource()) locker2_add_pending#(Lock,Resources,Client) -> member#(record_extract(Lock,lock(),resource()),Resources) locker2_add_pending#(Lock,Resources,Client) -> case1#(Client,Resources,Lock,member(record_extract(Lock,lock(),resource()),Resources)) case1#(Client,Resources,Lock,true()) -> record_extract#(Lock,lock(),pending()) case1#(Client,Resources,Lock,true()) -> append#(record_extract(Lock,lock(),pending()),cons(Client,nil())) case1#(Client,Resources,Lock,true()) -> record_updates#(Lock,lock(),cons(tuple(pending(),tuplenil(append( record_extract ( Lock,lock(),pending()), cons (Client,nil())))), nil())) locker2_release_lock#(Lock,Client) -> record_extract#(Lock,lock(),excl()) locker2_release_lock#(Lock,Client) -> gen_modtageq#(Client,record_extract(Lock,lock(),excl())) 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())) locker2_obtainables#(cons(Lock,Locks),Client) -> record_extract#(Lock,lock(),pending()) locker2_obtainables#(cons(Lock,Locks),Client) -> member#(Client,record_extract(Lock,lock(),pending())) locker2_obtainables#(cons(Lock,Locks),Client) -> case5#(Client,Locks,Lock,member(Client,record_extract(Lock,lock(),pending()))) case5#(Client,Locks,Lock,true()) -> locker2_obtainables#(Locks,Client) case5#(Client,Locks,Lock,false()) -> locker2_obtainables#(Locks,Client) locker2_check_available#(Resource,cons(Lock,Locks)) -> record_extract#(Lock,lock(),resource()) locker2_check_available#(Resource,cons(Lock,Locks)) -> case6#(Locks,Lock,Resource,equal(Resource,record_extract(Lock,lock(),resource()))) case6#(Locks,Lock,Resource,true()) -> record_extract#(Lock,lock(),pending()) case6#(Locks,Lock,Resource,true()) -> record_extract#(Lock,lock(),excl()) case6#(Locks,Lock,Resource,false()) -> locker2_check_available#(Resource,Locks) locker2_check_availables#(cons(Resource,Resources),Locks) -> locker2_check_availables#(Resources,Locks) locker2_check_availables#(cons(Resource,Resources),Locks) -> locker2_check_available#(Resource,Locks) append#(cons(Head,Tail),List) -> append#(Tail,List) subtract#(List,cons(Head,Tail)) -> delete#(Head,List) subtract#(List,cons(Head,Tail)) -> subtract#(delete(Head,List),Tail) delete#(E,cons(Head,Tail)) -> case8#(Tail,Head,E,equal(E,Head)) case8#(Tail,Head,E,false()) -> delete#(E,Tail) member#(E,cons(Head,Tail)) -> case9#(Tail,Head,E,equal(E,Head)) case9#(Tail,Head,E,false()) -> member#(E,Tail) eqs#(stack(E1,S1),stack(E2,S2)) -> eqs#(S1,S2) eqs#(stack(E1,S1),stack(E2,S2)) -> eqt#(E1,E2) eqs#(stack(E1,S1),stack(E2,S2)) -> and#(eqt(E1,E2),eqs(S1,S2)) istops#(E1,stack(E2,S1)) -> eqt#(E1,E2) eqc#(calls(E1,S1,CS1),calls(E2,S2,CS2)) -> eqc#(CS1,CS2) eqc#(calls(E1,S1,CS1),calls(E2,S2,CS2)) -> eqs#(S1,S2) eqc#(calls(E1,S1,CS1),calls(E2,S2,CS2)) -> and#(eqs(S1,S2),eqc(CS1,CS2)) eqc#(calls(E1,S1,CS1),calls(E2,S2,CS2)) -> eqt#(E1,E2) eqc#(calls(E1,S1,CS1),calls(E2,S2,CS2)) -> and#(eqt(E1,E2),and(eqs(S1,S2),eqc(CS1,CS2))) push#(E1,E2,calls(E3,S1,CS1)) -> eqt#(E1,E3) push#(E1,E2,calls(E3,S1,CS1)) -> push1#(E1,E2,E3,S1,CS1,eqt(E1,E3)) push1#(E1,E2,E3,S1,CS1,T()) -> pushs#(E2,S1) TRS: 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) and(T(),B) -> B and(B,T()) -> B and(F(),B) -> F() and(B,F()) -> F() 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))))) subtract(List,cons(Head,Tail)) -> subtract(delete(Head,List),Tail) subtract(List,nil()) -> List delete(E,nil()) -> nil() delete(E,cons(Head,Tail)) -> case8(Tail,Head,E,equal(E,Head)) record_extract(tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(F2))))), lock(),resource()) -> tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(F2))))) member(E,nil()) -> false() member(E,cons(Head,Tail)) -> case9(Tail,Head,E,equal(E,Head)) gen_modtageq(Client1,Client2) -> equal(Client1,Client2) 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)) 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))) Matrix Interpretation Processor: dim=1 usable rules: 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) and(T(),B) -> B and(B,T()) -> B and(F(),B) -> F() and(B,F()) -> F() subtract(List,cons(Head,Tail)) -> subtract(delete(Head,List),Tail) subtract(List,nil()) -> List delete(E,nil()) -> nil() delete(E,cons(Head,Tail)) -> case8(Tail,Head,E,equal(E,Head)) record_extract(tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(F2))))), lock(),resource()) -> tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(F2))))) member(E,nil()) -> false() member(E,cons(Head,Tail)) -> case9(Tail,Head,E,equal(E,Head)) 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)) interpretation: [push1#](x0, x1, x2, x3, x4, x5) = x0 + 4x1 + 6, [push#](x0, x1, x2) = 6x0 + 6x1 + x2 + 3, [eqc#](x0, x1) = 4x0 + 1, [istops#](x0, x1) = 4x0 + 4, [pushs#](x0, x1) = 0, [eqs#](x0, x1) = x0 + 3, [case9#](x0, x1, x2, x3) = 2x0 + 4, [case8#](x0, x1, x2, x3) = 2x0 + 2x1 + x2 + 2x3 + 3, [delete#](x0, x1) = x0 + 2x1 + 4, [locker2_check_availables#](x0, x1) = 4x0, [case6#](x0, x1, x2, x3) = x3, [locker2_check_available#](x0, x1) = 3, [case5#](x0, x1, x2, x3) = 6x1 + 5x2 + 2x3, [locker2_obtainables#](x0, x1) = 5x0 + 3, [case2#](x0, x1, x2) = x0 + 4x1 + 4, [gen_modtageq#](x0, x1) = 0, [locker2_release_lock#](x0, x1) = 4x0 + x1 + 5, [append#](x0, x1) = 4x0 + 4, [case1#](x0, x1, x2, x3) = 5x1 + 4x2 + 6, [member#](x0, x1) = 2x1 + 1, [locker2_add_pending#](x0, x1, x2) = 4x0 + 5x1 + 4x2 + 7, [subtract#](x0, x1) = 4x0 + x1 + 4, [locker2_remove_pending#](x0, x1) = 4x0 + 2x1 + 7, [case0#](x0, x1, x2) = 2x0 + 5x2 + 6, [locker2_map_claim_lock#](x0, x1, x2) = 6x0 + 4, [locker2_promote_pending#](x0, x1) = 5x0 + 3x1 + 7, [locker2_map_promote_pending#](x0, x1) = 5x0 + 4x1 + 5, [record_updates#](x0, x1, x2) = 4x1 + x2, [record_update#](x0, x1, x2, x3) = 0, [record_extract#](x0, x1, x2) = 0, [element#](x0, x1) = x1, [eqt#](x0, x1) = 4x0 + 3, [and#](x0, x1) = 4x0 + 4, [calls](x0, x1, x2) = x0 + x1 + 2x2 + 4, [eqc](x0, x1) = 0, [nocalls] = 0, [stack](x0, x1) = 4x0 + 2x1 + 5, [eqs](x0, x1) = x0, [empty] = 0, [case9](x0, x1, x2, x3) = x3 + 4, [case8](x0, x1, x2, x3) = 2, [delete](x0, x1) = x1, [equal](x0, x1) = 2, [excllock] = 0, [gen_modtageq](x0, x1) = 0, [append](x0, x1) = 2x0, [member](x0, x1) = 6, [subtract](x0, x1) = 2x0, [record_update](x0, x1, x2, x3) = 0, [record_extract](x0, x1, x2) = x0, [s](x0) = 3, [true] = 4, [tag] = 0, [resource] = 0, [request] = 0, [release] = 7, [pending] = 0, [ok] = 5, [mcrlrecord] = 0, [locker] = 0, [lock] = 0, [false] = 5, [excl] = 0, [a] = 7, [tuplenil](x0) = x0 + 1, [tuple](x0, x1) = 2x0 + 2x1 + 1, [cons](x0, x1) = x0 + 2x1 + 2, [int](x0) = 4x0 + 7, [pid](x0) = x0 + 6, [eqt](x0, x1) = x0, [undefined] = 1, [nil] = 0, [and](x0, x1) = x0 + x1, [F] = 0, [T] = 0 orientation: eqt#(pid(N1),pid(N2)) = 4N1 + 27 >= 4N1 + 3 = eqt#(N1,N2) eqt#(cons(H1,T1),cons(H2,T2)) = 4H1 + 8T1 + 11 >= 4T1 + 3 = eqt#(T1,T2) eqt#(cons(H1,T1),cons(H2,T2)) = 4H1 + 8T1 + 11 >= 4H1 + 3 = eqt#(H1,H2) eqt#(cons(H1,T1),cons(H2,T2)) = 4H1 + 8T1 + 11 >= 4H1 + 4 = and#(eqt(H1,H2),eqt(T1,T2)) eqt#(tuple(H1,T1),tuple(H2,T2)) = 8H1 + 8T1 + 7 >= 4T1 + 3 = eqt#(T1,T2) eqt#(tuple(H1,T1),tuple(H2,T2)) = 8H1 + 8T1 + 7 >= 4H1 + 3 = eqt#(H1,H2) eqt#(tuple(H1,T1),tuple(H2,T2)) = 8H1 + 8T1 + 7 >= 4H1 + 4 = and#(eqt(H1,H2),eqt(T1,T2)) eqt#(tuplenil(H1),tuplenil(H2)) = 4H1 + 7 >= 4H1 + 3 = eqt#(H1,H2) element#(int(s(s(N1))),tuple(T1,T2)) = 2T1 + 2T2 + 1 >= T2 = element#(int(s(N1)),T2) record_updates#(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields)) = 2Field + 2Fields + 4Name + 2NewF + 5 >= 0 = record_update#(Record,Name,Field,NewF) record_updates#(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields)) = 2Field + 2Fields + 4Name + 2NewF + 5 >= Fields + 4Name = record_updates#(record_update(Record,Name,Field,NewF),Name,Fields) locker2_map_promote_pending#(cons(Lock,Locks),Pending) = 5Lock + 10Locks + 4Pending + 15 >= 5Locks + 4Pending + 5 = locker2_map_promote_pending#(Locks,Pending) locker2_map_promote_pending#(cons(Lock,Locks),Pending) = 5Lock + 10Locks + 4Pending + 15 >= 5Lock + 3Pending + 7 = locker2_promote_pending#(Lock,Pending) locker2_map_claim_lock#(cons(Lock,Locks),Resources,Client) = 6Lock + 12Locks + 16 >= 6Locks + 4 = locker2_map_claim_lock#(Locks,Resources,Client) locker2_promote_pending#(Lock,Client) = 3Client + 5Lock + 7 >= 0 = record_extract#(Lock,lock(),pending()) locker2_promote_pending#(Lock,Client) = 3Client + 5Lock + 7 >= 2Client + 5Lock + 6 = case0#(Client,Lock,record_extract(Lock,lock(),pending())) case0#(Client,Lock,cons(Client,Pendings)) = 7Client + 10Pendings + 16 >= 2Client + 4Pendings + 15 = record_updates#(Lock,lock(),cons(tuple(excl(),tuplenil(Client)),cons( tuple ( pending(), tuplenil ( Pendings)), nil ()))) locker2_remove_pending#(Lock,Client) = 2Client + 4Lock + 7 >= 0 = record_extract#(Lock,lock(),pending()) locker2_remove_pending#(Lock,Client) = 2Client + 4Lock + 7 >= Client + 4Lock + 6 = subtract#(record_extract(Lock,lock(),pending()),cons(Client,nil())) locker2_remove_pending#(Lock,Client) = 2Client + 4Lock + 7 >= 4Lock + 5 = record_updates#(Lock,lock(),cons(tuple(pending(),tuplenil(subtract(record_extract (Lock, lock (), pending ()), cons (Client, nil ())))), nil())) locker2_add_pending#(Lock,Resources,Client) = 4Client + 4Lock + 5Resources + 7 >= 0 = record_extract#(Lock,lock(),resource()) locker2_add_pending#(Lock,Resources,Client) = 4Client + 4Lock + 5Resources + 7 >= 2Resources + 1 = member#(record_extract(Lock,lock(),resource()),Resources) locker2_add_pending#(Lock,Resources,Client) = 4Client + 4Lock + 5Resources + 7 >= 4Lock + 5Resources + 6 = case1#(Client,Resources,Lock,member(record_extract(Lock,lock(),resource()), Resources)) case1#(Client,Resources,Lock,true()) = 4Lock + 5Resources + 6 >= 0 = record_extract#(Lock,lock(),pending()) case1#(Client,Resources,Lock,true()) = 4Lock + 5Resources + 6 >= 4Lock + 4 = append#(record_extract(Lock,lock(),pending()),cons(Client,nil())) case1#(Client,Resources,Lock,true()) = 4Lock + 5Resources + 6 >= 4Lock + 5 = record_updates#(Lock,lock(),cons(tuple(pending(),tuplenil(append(record_extract (Lock, lock(), pending ()), cons (Client, nil ())))), nil())) locker2_release_lock#(Lock,Client) = Client + 4Lock + 5 >= 0 = record_extract#(Lock,lock(),excl()) locker2_release_lock#(Lock,Client) = Client + 4Lock + 5 >= 0 = gen_modtageq#(Client,record_extract(Lock,lock(),excl())) locker2_release_lock#(Lock,Client) = Client + 4Lock + 5 >= Client + 4Lock + 4 = case2#(Client,Lock,gen_modtageq(Client,record_extract(Lock,lock(),excl()))) case2#(Client,Lock,true()) = Client + 4Lock + 4 >= 3 = record_updates#(Lock,lock(),cons(tuple(excllock(),excl()),nil())) locker2_obtainables#(cons(Lock,Locks),Client) = 5Lock + 10Locks + 13 >= 0 = record_extract#(Lock,lock(),pending()) locker2_obtainables#(cons(Lock,Locks),Client) = 5Lock + 10Locks + 13 >= 2Lock + 1 = member#(Client,record_extract(Lock,lock(),pending())) locker2_obtainables#(cons(Lock,Locks),Client) = 5Lock + 10Locks + 13 >= 5Lock + 6Locks + 12 = case5#(Client,Locks,Lock,member(Client,record_extract(Lock,lock(),pending()))) case5#(Client,Locks,Lock,true()) = 5Lock + 6Locks + 8 >= 5Locks + 3 = locker2_obtainables#(Locks,Client) case5#(Client,Locks,Lock,false()) = 5Lock + 6Locks + 10 >= 5Locks + 3 = locker2_obtainables#(Locks,Client) locker2_check_available#(Resource,cons(Lock,Locks)) = 3 >= 0 = record_extract#(Lock,lock(),resource()) locker2_check_available#(Resource,cons(Lock,Locks)) = 3 >= 2 = case6#(Locks,Lock,Resource,equal(Resource,record_extract(Lock,lock(), resource()))) case6#(Locks,Lock,Resource,true()) = 4 >= 0 = record_extract#(Lock,lock(),pending()) case6#(Locks,Lock,Resource,true()) = 4 >= 0 = record_extract#(Lock,lock(),excl()) case6#(Locks,Lock,Resource,false()) = 5 >= 3 = locker2_check_available#(Resource,Locks) locker2_check_availables#(cons(Resource,Resources),Locks) = 4Resource + 8Resources + 8 >= 4Resources = locker2_check_availables#(Resources,Locks) locker2_check_availables#(cons(Resource,Resources),Locks) = 4Resource + 8Resources + 8 >= 3 = locker2_check_available#(Resource,Locks) append#(cons(Head,Tail),List) = 4Head + 8Tail + 12 >= 4Tail + 4 = append#(Tail,List) subtract#(List,cons(Head,Tail)) = Head + 4List + 2Tail + 6 >= Head + 2List + 4 = delete#(Head,List) subtract#(List,cons(Head,Tail)) = Head + 4List + 2Tail + 6 >= 4List + Tail + 4 = subtract#(delete(Head,List),Tail) delete#(E,cons(Head,Tail)) = E + 2Head + 4Tail + 8 >= E + 2Head + 2Tail + 7 = case8#(Tail,Head,E,equal(E,Head)) case8#(Tail,Head,E,false()) = E + 2Head + 2Tail + 13 >= E + 2Tail + 4 = delete#(E,Tail) member#(E,cons(Head,Tail)) = 2Head + 4Tail + 5 >= 2Tail + 4 = case9#(Tail,Head,E,equal(E,Head)) case9#(Tail,Head,E,false()) = 2Tail + 4 >= 2Tail + 1 = member#(E,Tail) eqs#(stack(E1,S1),stack(E2,S2)) = 4E1 + 2S1 + 8 >= S1 + 3 = eqs#(S1,S2) eqs#(stack(E1,S1),stack(E2,S2)) = 4E1 + 2S1 + 8 >= 4E1 + 3 = eqt#(E1,E2) eqs#(stack(E1,S1),stack(E2,S2)) = 4E1 + 2S1 + 8 >= 4E1 + 4 = and#(eqt(E1,E2),eqs(S1,S2)) istops#(E1,stack(E2,S1)) = 4E1 + 4 >= 4E1 + 3 = eqt#(E1,E2) eqc#(calls(E1,S1,CS1),calls(E2,S2,CS2)) = 8CS1 + 4E1 + 4S1 + 17 >= 4CS1 + 1 = eqc#(CS1,CS2) eqc#(calls(E1,S1,CS1),calls(E2,S2,CS2)) = 8CS1 + 4E1 + 4S1 + 17 >= S1 + 3 = eqs#(S1,S2) eqc#(calls(E1,S1,CS1),calls(E2,S2,CS2)) = 8CS1 + 4E1 + 4S1 + 17 >= 4S1 + 4 = and#(eqs(S1,S2),eqc(CS1,CS2)) eqc#(calls(E1,S1,CS1),calls(E2,S2,CS2)) = 8CS1 + 4E1 + 4S1 + 17 >= 4E1 + 3 = eqt#(E1,E2) eqc#(calls(E1,S1,CS1),calls(E2,S2,CS2)) = 8CS1 + 4E1 + 4S1 + 17 >= 4E1 + 4 = and#(eqt(E1,E2),and(eqs(S1,S2),eqc(CS1,CS2))) push#(E1,E2,calls(E3,S1,CS1)) = 2CS1 + 6E1 + 6E2 + E3 + S1 + 7 >= 4E1 + 3 = eqt#(E1,E3) push#(E1,E2,calls(E3,S1,CS1)) = 2CS1 + 6E1 + 6E2 + E3 + S1 + 7 >= E1 + 4E2 + 6 = push1#(E1,E2,E3,S1,CS1,eqt(E1,E3)) push1#(E1,E2,E3,S1,CS1,T()) = E1 + 4E2 + 6 >= 0 = pushs#(E2,S1) eqt(nil(),undefined()) = 0 >= 0 = F() eqt(nil(),pid(N2)) = 0 >= 0 = F() eqt(nil(),int(N2)) = 0 >= 0 = F() eqt(nil(),cons(H2,T2)) = 0 >= 0 = F() eqt(nil(),tuple(H2,T2)) = 0 >= 0 = F() eqt(nil(),tuplenil(H2)) = 0 >= 0 = F() eqt(a(),nil()) = 7 >= 0 = F() eqt(a(),a()) = 7 >= 0 = T() eqt(a(),excl()) = 7 >= 0 = F() eqt(a(),false()) = 7 >= 0 = F() eqt(a(),lock()) = 7 >= 0 = F() eqt(a(),locker()) = 7 >= 0 = F() eqt(a(),mcrlrecord()) = 7 >= 0 = F() eqt(a(),ok()) = 7 >= 0 = F() eqt(a(),pending()) = 7 >= 0 = F() eqt(a(),release()) = 7 >= 0 = F() eqt(a(),request()) = 7 >= 0 = F() eqt(a(),resource()) = 7 >= 0 = F() eqt(a(),tag()) = 7 >= 0 = F() eqt(a(),true()) = 7 >= 0 = F() eqt(a(),undefined()) = 7 >= 0 = F() eqt(a(),pid(N2)) = 7 >= 0 = F() eqt(a(),int(N2)) = 7 >= 0 = F() eqt(a(),cons(H2,T2)) = 7 >= 0 = F() eqt(a(),tuple(H2,T2)) = 7 >= 0 = F() eqt(a(),tuplenil(H2)) = 7 >= 0 = F() eqt(excl(),nil()) = 0 >= 0 = F() eqt(excl(),a()) = 0 >= 0 = F() eqt(excl(),excl()) = 0 >= 0 = T() eqt(excl(),false()) = 0 >= 0 = F() eqt(excl(),lock()) = 0 >= 0 = F() eqt(excl(),locker()) = 0 >= 0 = F() eqt(excl(),mcrlrecord()) = 0 >= 0 = F() eqt(excl(),ok()) = 0 >= 0 = F() eqt(excl(),pending()) = 0 >= 0 = F() eqt(excl(),release()) = 0 >= 0 = F() eqt(excl(),request()) = 0 >= 0 = F() eqt(excl(),resource()) = 0 >= 0 = F() eqt(excl(),tag()) = 0 >= 0 = F() eqt(excl(),true()) = 0 >= 0 = F() eqt(excl(),undefined()) = 0 >= 0 = F() eqt(excl(),pid(N2)) = 0 >= 0 = F() eqt(excl(),eqt(false(),int(N2))) = 0 >= 0 = F() eqt(false(),cons(H2,T2)) = 5 >= 0 = F() eqt(false(),tuple(H2,T2)) = 5 >= 0 = F() eqt(false(),tuplenil(H2)) = 5 >= 0 = F() eqt(lock(),nil()) = 0 >= 0 = F() eqt(lock(),a()) = 0 >= 0 = F() eqt(lock(),excl()) = 0 >= 0 = F() eqt(lock(),false()) = 0 >= 0 = F() eqt(lock(),lock()) = 0 >= 0 = T() eqt(lock(),locker()) = 0 >= 0 = F() eqt(lock(),mcrlrecord()) = 0 >= 0 = F() eqt(lock(),ok()) = 0 >= 0 = F() eqt(lock(),pending()) = 0 >= 0 = F() eqt(lock(),release()) = 0 >= 0 = F() eqt(lock(),request()) = 0 >= 0 = F() eqt(lock(),resource()) = 0 >= 0 = F() eqt(lock(),tag()) = 0 >= 0 = F() eqt(lock(),true()) = 0 >= 0 = F() eqt(lock(),undefined()) = 0 >= 0 = F() eqt(lock(),pid(N2)) = 0 >= 0 = F() eqt(lock(),int(N2)) = 0 >= 0 = F() eqt(lock(),cons(H2,T2)) = 0 >= 0 = F() eqt(lock(),tuple(H2,T2)) = 0 >= 0 = F() eqt(lock(),tuplenil(H2)) = 0 >= 0 = F() eqt(locker(),nil()) = 0 >= 0 = F() eqt(locker(),a()) = 0 >= 0 = F() eqt(locker(),excl()) = 0 >= 0 = F() eqt(locker(),false()) = 0 >= 0 = F() eqt(locker(),lock()) = 0 >= 0 = F() eqt(locker(),locker()) = 0 >= 0 = T() eqt(locker(),mcrlrecord()) = 0 >= 0 = F() eqt(locker(),ok()) = 0 >= 0 = F() eqt(locker(),pending()) = 0 >= 0 = F() eqt(locker(),release()) = 0 >= 0 = F() eqt(locker(),request()) = 0 >= 0 = F() eqt(locker(),resource()) = 0 >= 0 = F() eqt(locker(),tag()) = 0 >= 0 = F() eqt(locker(),true()) = 0 >= 0 = F() eqt(locker(),undefined()) = 0 >= 0 = F() eqt(locker(),pid(N2)) = 0 >= 0 = F() eqt(locker(),int(N2)) = 0 >= 0 = F() eqt(locker(),cons(H2,T2)) = 0 >= 0 = F() eqt(locker(),tuple(H2,T2)) = 0 >= 0 = F() eqt(locker(),tuplenil(H2)) = 0 >= 0 = F() eqt(mcrlrecord(),nil()) = 0 >= 0 = F() eqt(mcrlrecord(),a()) = 0 >= 0 = F() eqt(mcrlrecord(),excl()) = 0 >= 0 = F() eqt(mcrlrecord(),false()) = 0 >= 0 = F() eqt(mcrlrecord(),lock()) = 0 >= 0 = F() eqt(mcrlrecord(),locker()) = 0 >= 0 = F() eqt(mcrlrecord(),mcrlrecord()) = 0 >= 0 = T() eqt(mcrlrecord(),ok()) = 0 >= 0 = F() eqt(mcrlrecord(),pending()) = 0 >= 0 = F() eqt(mcrlrecord(),release()) = 0 >= 0 = F() eqt(mcrlrecord(),request()) = 0 >= 0 = F() eqt(mcrlrecord(),resource()) = 0 >= 0 = F() eqt(ok(),resource()) = 5 >= 0 = F() eqt(ok(),tag()) = 5 >= 0 = F() eqt(ok(),true()) = 5 >= 0 = F() eqt(ok(),undefined()) = 5 >= 0 = F() eqt(ok(),pid(N2)) = 5 >= 0 = F() eqt(ok(),int(N2)) = 5 >= 0 = F() eqt(ok(),cons(H2,T2)) = 5 >= 0 = F() eqt(ok(),tuple(H2,T2)) = 5 >= 0 = F() eqt(ok(),tuplenil(H2)) = 5 >= 0 = F() eqt(pending(),nil()) = 0 >= 0 = F() eqt(pending(),a()) = 0 >= 0 = F() eqt(pending(),excl()) = 0 >= 0 = F() eqt(pending(),false()) = 0 >= 0 = F() eqt(pending(),lock()) = 0 >= 0 = F() eqt(pending(),locker()) = 0 >= 0 = F() eqt(pending(),mcrlrecord()) = 0 >= 0 = F() eqt(pending(),ok()) = 0 >= 0 = F() eqt(pending(),pending()) = 0 >= 0 = T() eqt(pending(),release()) = 0 >= 0 = F() eqt(pending(),request()) = 0 >= 0 = F() eqt(pending(),resource()) = 0 >= 0 = F() eqt(pending(),tag()) = 0 >= 0 = F() eqt(pending(),true()) = 0 >= 0 = F() eqt(pending(),undefined()) = 0 >= 0 = F() eqt(pending(),pid(N2)) = 0 >= 0 = F() eqt(pending(),int(N2)) = 0 >= 0 = F() eqt(pending(),cons(H2,T2)) = 0 >= 0 = F() eqt(pending(),tuple(H2,T2)) = 0 >= 0 = F() eqt(pending(),tuplenil(H2)) = 0 >= 0 = F() eqt(release(),nil()) = 7 >= 0 = F() eqt(release(),a()) = 7 >= 0 = F() eqt(release(),excl()) = 7 >= 0 = F() eqt(release(),false()) = 7 >= 0 = F() eqt(release(),lock()) = 7 >= 0 = F() eqt(release(),locker()) = 7 >= 0 = F() eqt(release(),mcrlrecord()) = 7 >= 0 = F() eqt(release(),ok()) = 7 >= 0 = F() eqt(request(),mcrlrecord()) = 0 >= 0 = F() eqt(request(),ok()) = 0 >= 0 = F() eqt(request(),pending()) = 0 >= 0 = F() eqt(request(),release()) = 0 >= 0 = F() eqt(request(),request()) = 0 >= 0 = T() eqt(request(),resource()) = 0 >= 0 = F() eqt(request(),tag()) = 0 >= 0 = F() eqt(request(),true()) = 0 >= 0 = F() eqt(request(),undefined()) = 0 >= 0 = F() eqt(request(),pid(N2)) = 0 >= 0 = F() eqt(request(),int(N2)) = 0 >= 0 = F() eqt(request(),cons(H2,T2)) = 0 >= 0 = F() eqt(request(),tuple(H2,T2)) = 0 >= 0 = F() eqt(request(),tuplenil(H2)) = 0 >= 0 = F() eqt(resource(),nil()) = 0 >= 0 = F() eqt(resource(),a()) = 0 >= 0 = F() eqt(resource(),excl()) = 0 >= 0 = F() eqt(resource(),false()) = 0 >= 0 = F() eqt(resource(),lock()) = 0 >= 0 = F() eqt(resource(),locker()) = 0 >= 0 = F() eqt(resource(),mcrlrecord()) = 0 >= 0 = F() eqt(resource(),ok()) = 0 >= 0 = F() eqt(resource(),pending()) = 0 >= 0 = F() eqt(resource(),release()) = 0 >= 0 = F() eqt(resource(),request()) = 0 >= 0 = F() eqt(resource(),resource()) = 0 >= 0 = T() eqt(resource(),tag()) = 0 >= 0 = F() eqt(resource(),true()) = 0 >= 0 = F() eqt(resource(),undefined()) = 0 >= 0 = F() eqt(resource(),pid(N2)) = 0 >= 0 = F() eqt(resource(),int(N2)) = 0 >= 0 = F() eqt(resource(),cons(H2,T2)) = 0 >= 0 = F() eqt(resource(),tuple(H2,T2)) = 0 >= 0 = F() eqt(resource(),tuplenil(H2)) = 0 >= 0 = F() eqt(tag(),nil()) = 0 >= 0 = F() eqt(tag(),a()) = 0 >= 0 = F() eqt(tag(),excl()) = 0 >= 0 = F() eqt(tag(),false()) = 0 >= 0 = F() eqt(tag(),lock()) = 0 >= 0 = F() eqt(tag(),locker()) = 0 >= 0 = F() eqt(tag(),mcrlrecord()) = 0 >= 0 = F() eqt(tag(),ok()) = 0 >= 0 = F() eqt(tag(),pending()) = 0 >= 0 = F() eqt(tag(),release()) = 0 >= 0 = F() eqt(tag(),request()) = 0 >= 0 = F() eqt(tag(),resource()) = 0 >= 0 = F() eqt(tag(),tag()) = 0 >= 0 = T() eqt(tag(),true()) = 0 >= 0 = F() eqt(tag(),undefined()) = 0 >= 0 = F() eqt(tag(),pid(N2)) = 0 >= 0 = F() eqt(tag(),int(N2)) = 0 >= 0 = F() eqt(tag(),cons(H2,T2)) = 0 >= 0 = F() eqt(tag(),tuple(H2,T2)) = 0 >= 0 = F() eqt(tag(),tuplenil(H2)) = 0 >= 0 = F() eqt(true(),nil()) = 4 >= 0 = F() eqt(true(),a()) = 4 >= 0 = F() eqt(true(),excl()) = 4 >= 0 = F() eqt(true(),false()) = 4 >= 0 = F() eqt(true(),lock()) = 4 >= 0 = F() eqt(true(),locker()) = 4 >= 0 = F() eqt(true(),mcrlrecord()) = 4 >= 0 = F() eqt(true(),ok()) = 4 >= 0 = F() eqt(true(),pending()) = 4 >= 0 = F() eqt(true(),release()) = 4 >= 0 = F() eqt(true(),request()) = 4 >= 0 = F() eqt(true(),resource()) = 4 >= 0 = F() eqt(true(),tag()) = 4 >= 0 = F() eqt(true(),true()) = 4 >= 0 = T() eqt(true(),undefined()) = 4 >= 0 = F() eqt(true(),pid(N2)) = 4 >= 0 = F() eqt(true(),int(N2)) = 4 >= 0 = F() eqt(true(),cons(H2,T2)) = 4 >= 0 = F() eqt(true(),tuple(H2,T2)) = 4 >= 0 = F() eqt(true(),tuplenil(H2)) = 4 >= 0 = F() eqt(undefined(),nil()) = 1 >= 0 = F() eqt(undefined(),a()) = 1 >= 0 = F() eqt(undefined(),tuplenil(H2)) = 1 >= 0 = F() eqt(pid(N1),nil()) = N1 + 6 >= 0 = F() eqt(pid(N1),a()) = N1 + 6 >= 0 = F() eqt(pid(N1),excl()) = N1 + 6 >= 0 = F() eqt(pid(N1),false()) = N1 + 6 >= 0 = F() eqt(pid(N1),lock()) = N1 + 6 >= 0 = F() eqt(pid(N1),locker()) = N1 + 6 >= 0 = F() eqt(pid(N1),mcrlrecord()) = N1 + 6 >= 0 = F() eqt(pid(N1),ok()) = N1 + 6 >= 0 = F() eqt(pid(N1),pending()) = N1 + 6 >= 0 = F() eqt(pid(N1),release()) = N1 + 6 >= 0 = F() eqt(pid(N1),request()) = N1 + 6 >= 0 = F() eqt(pid(N1),resource()) = N1 + 6 >= 0 = F() eqt(pid(N1),tag()) = N1 + 6 >= 0 = F() eqt(pid(N1),true()) = N1 + 6 >= 0 = F() eqt(pid(N1),undefined()) = N1 + 6 >= 0 = F() eqt(pid(N1),pid(N2)) = N1 + 6 >= N1 = eqt(N1,N2) eqt(pid(N1),int(N2)) = N1 + 6 >= 0 = F() eqt(pid(N1),cons(H2,T2)) = N1 + 6 >= 0 = F() eqt(pid(N1),tuple(H2,T2)) = N1 + 6 >= 0 = F() eqt(pid(N1),tuplenil(H2)) = N1 + 6 >= 0 = F() eqt(int(N1),nil()) = 4N1 + 7 >= 0 = F() eqt(int(N1),a()) = 4N1 + 7 >= 0 = F() eqt(int(N1),excl()) = 4N1 + 7 >= 0 = F() eqt(int(N1),false()) = 4N1 + 7 >= 0 = F() eqt(int(N1),lock()) = 4N1 + 7 >= 0 = F() eqt(int(N1),locker()) = 4N1 + 7 >= 0 = F() eqt(int(N1),mcrlrecord()) = 4N1 + 7 >= 0 = F() eqt(int(N1),ok()) = 4N1 + 7 >= 0 = F() eqt(int(N1),pending()) = 4N1 + 7 >= 0 = F() eqt(int(N1),release()) = 4N1 + 7 >= 0 = F() eqt(int(N1),request()) = 4N1 + 7 >= 0 = F() eqt(int(N1),resource()) = 4N1 + 7 >= 0 = F() eqt(int(N1),tag()) = 4N1 + 7 >= 0 = F() eqt(int(N1),true()) = 4N1 + 7 >= 0 = F() eqt(int(N1),undefined()) = 4N1 + 7 >= 0 = F() eqt(cons(H1,T1),resource()) = H1 + 2T1 + 2 >= 0 = F() eqt(cons(H1,T1),tag()) = H1 + 2T1 + 2 >= 0 = F() eqt(cons(H1,T1),true()) = H1 + 2T1 + 2 >= 0 = F() eqt(cons(H1,T1),undefined()) = H1 + 2T1 + 2 >= 0 = F() eqt(cons(H1,T1),pid(N2)) = H1 + 2T1 + 2 >= 0 = F() eqt(cons(H1,T1),int(N2)) = H1 + 2T1 + 2 >= 0 = F() eqt(cons(H1,T1),cons(H2,T2)) = H1 + 2T1 + 2 >= H1 + T1 = and(eqt(H1,H2),eqt(T1,T2)) eqt(cons(H1,T1),tuple(H2,T2)) = H1 + 2T1 + 2 >= 0 = F() eqt(cons(H1,T1),tuplenil(H2)) = H1 + 2T1 + 2 >= 0 = F() eqt(tuple(H1,T1),nil()) = 2H1 + 2T1 + 1 >= 0 = F() eqt(tuple(H1,T1),a()) = 2H1 + 2T1 + 1 >= 0 = F() eqt(tuple(H1,T1),excl()) = 2H1 + 2T1 + 1 >= 0 = F() eqt(tuple(H1,T1),false()) = 2H1 + 2T1 + 1 >= 0 = F() eqt(tuple(H1,T1),lock()) = 2H1 + 2T1 + 1 >= 0 = F() eqt(tuple(H1,T1),locker()) = 2H1 + 2T1 + 1 >= 0 = F() eqt(tuple(H1,T1),mcrlrecord()) = 2H1 + 2T1 + 1 >= 0 = F() eqt(tuple(H1,T1),ok()) = 2H1 + 2T1 + 1 >= 0 = F() eqt(tuple(H1,T1),pending()) = 2H1 + 2T1 + 1 >= 0 = F() eqt(tuple(H1,T1),release()) = 2H1 + 2T1 + 1 >= 0 = F() eqt(tuple(H1,T1),request()) = 2H1 + 2T1 + 1 >= 0 = F() eqt(tuple(H1,T1),resource()) = 2H1 + 2T1 + 1 >= 0 = F() eqt(tuple(H1,T1),tag()) = 2H1 + 2T1 + 1 >= 0 = F() eqt(tuple(H1,T1),true()) = 2H1 + 2T1 + 1 >= 0 = F() eqt(tuple(H1,T1),undefined()) = 2H1 + 2T1 + 1 >= 0 = F() eqt(tuple(H1,T1),pid(N2)) = 2H1 + 2T1 + 1 >= 0 = F() eqt(tuple(H1,T1),int(N2)) = 2H1 + 2T1 + 1 >= 0 = F() eqt(tuple(H1,T1),cons(H2,T2)) = 2H1 + 2T1 + 1 >= 0 = F() eqt(tuple(H1,T1),tuple(H2,T2)) = 2H1 + 2T1 + 1 >= H1 + T1 = and(eqt(H1,H2),eqt(T1,T2)) eqt(tuple(H1,T1),tuplenil(H2)) = 2H1 + 2T1 + 1 >= 0 = F() eqt(tuplenil(H1),nil()) = H1 + 1 >= 0 = F() eqt(tuplenil(H1),a()) = H1 + 1 >= 0 = F() eqt(tuplenil(H1),excl()) = H1 + 1 >= 0 = F() eqt(tuplenil(H1),false()) = H1 + 1 >= 0 = F() eqt(tuplenil(H1),lock()) = H1 + 1 >= 0 = F() eqt(tuplenil(H1),locker()) = H1 + 1 >= 0 = F() eqt(tuplenil(H1),mcrlrecord()) = H1 + 1 >= 0 = F() eqt(tuplenil(H1),ok()) = H1 + 1 >= 0 = F() eqt(tuplenil(H1),pending()) = H1 + 1 >= 0 = F() eqt(tuplenil(H1),release()) = H1 + 1 >= 0 = F() eqt(tuplenil(H1),request()) = H1 + 1 >= 0 = F() eqt(tuplenil(H1),resource()) = H1 + 1 >= 0 = F() eqt(tuplenil(H1),tag()) = H1 + 1 >= 0 = F() eqt(tuplenil(H1),true()) = H1 + 1 >= 0 = F() eqt(tuplenil(H1),undefined()) = H1 + 1 >= 0 = F() eqt(tuplenil(H1),pid(N2)) = H1 + 1 >= 0 = F() eqt(tuplenil(H1),int(N2)) = H1 + 1 >= 0 = F() eqt(tuplenil(H1),cons(H2,T2)) = H1 + 1 >= 0 = F() eqt(tuplenil(H1),tuple(H2,T2)) = H1 + 1 >= 0 = F() eqt(tuplenil(H1),tuplenil(H2)) = H1 + 1 >= H1 = eqt(H1,H2) and(T(),B) = B >= B = B and(B,T()) = B >= B = B and(F(),B) = B >= 0 = F() and(B,F()) = B >= 0 = F() record_update(tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(F2))))), lock(),pending(),NewF) = 0 >= 8F0 + 16F1 + 16NewF + 31 = tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(NewF))))) subtract(List,cons(Head,Tail)) = 2List >= 2List = subtract(delete(Head,List),Tail) subtract(List,nil()) = 2List >= List = List delete(E,nil()) = 0 >= 0 = nil() delete(E,cons(Head,Tail)) = Head + 2Tail + 2 >= 2 = case8(Tail,Head,E,equal(E,Head)) record_extract(tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(F2))))), lock(),resource()) = 8F0 + 16F1 + 16F2 + 31 >= 8F0 + 16F1 + 16F2 + 31 = tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(F2))))) member(E,nil()) = 6 >= 5 = false() member(E,cons(Head,Tail)) = 6 >= 6 = case9(Tail,Head,E,equal(E,Head)) gen_modtageq(Client1,Client2) = 0 >= 2 = equal(Client1,Client2) eqs(empty(),empty()) = 0 >= 0 = T() eqs(empty(),stack(E2,S2)) = 0 >= 0 = F() eqs(stack(E1,S1),empty()) = 4E1 + 2S1 + 5 >= 0 = F() eqs(stack(E1,S1),stack(E2,S2)) = 4E1 + 2S1 + 5 >= E1 + S1 = and(eqt(E1,E2),eqs(S1,S2)) eqc(nocalls(),nocalls()) = 0 >= 0 = T() eqc(nocalls(),calls(E2,S2,CS2)) = 0 >= 0 = F() eqc(calls(E1,S1,CS1),nocalls()) = 0 >= 0 = F() eqc(calls(E1,S1,CS1),calls(E2,S2,CS2)) = 0 >= E1 + S1 = and(eqt(E1,E2),and(eqs(S1,S2),eqc(CS1,CS2))) problem: DPs: TRS: 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) and(T(),B) -> B and(B,T()) -> B and(F(),B) -> F() and(B,F()) -> F() 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))))) subtract(List,cons(Head,Tail)) -> subtract(delete(Head,List),Tail) subtract(List,nil()) -> List delete(E,nil()) -> nil() delete(E,cons(Head,Tail)) -> case8(Tail,Head,E,equal(E,Head)) record_extract(tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(F2))))), lock(),resource()) -> tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(F2))))) member(E,nil()) -> false() member(E,cons(Head,Tail)) -> case9(Tail,Head,E,equal(E,Head)) gen_modtageq(Client1,Client2) -> equal(Client1,Client2) 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)) 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))) Qed