YES

The TRS could be proven terminating. The proof took 4056 ms.

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (3907ms).
 | – Problem 2 was processed with processor SubtermCriterion (3ms).
 | – Problem 3 was processed with processor SubtermCriterion (2ms).
 | – Problem 4 was processed with processor SubtermCriterion (2ms).
 | – Problem 5 was processed with processor SubtermCriterion (2ms).
 | – Problem 6 was processed with processor SubtermCriterion (2ms).
 |    | – Problem 13 was processed with processor DependencyGraph (9ms).
 | – Problem 7 was processed with processor SubtermCriterion (44ms).
 | – Problem 8 was processed with processor SubtermCriterion (2ms).
 | – Problem 9 was processed with processor SubtermCriterion (2ms).
 | – Problem 10 was processed with processor SubtermCriterion (2ms).
 | – Problem 11 was processed with processor SubtermCriterion (2ms).
 | – Problem 12 was processed with processor SubtermCriterion (2ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

eqt#(pid(N1), pid(N2))eqt#(N1, N2)eqs#(stack(E1, S1), stack(E2, S2))and#(eqt(E1, E2), eqs(S1, S2))
eqc#(calls(E1, S1, CS1), calls(E2, S2, CS2))and#(eqt(E1, E2), and(eqs(S1, S2), eqc(CS1, CS2)))locker2_check_available#(Resource, cons(Lock, Locks))record_extract#(Lock, lock, resource)
eqt#(tuple(H1, T1), tuple(H2, T2))and#(eqt(H1, H2), eqt(T1, T2))subtract#(List, cons(Head, Tail))delete#(Head, List)
locker2_map_promote_pending#(cons(Lock, Locks), Pending)locker2_map_promote_pending#(Locks, Pending)eqs#(stack(E1, S1), stack(E2, S2))eqs#(S1, S2)
case6#(Locks, Lock, Resource, true)record_extract#(Lock, lock, excl)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)))locker2_check_availables#(cons(Resource, Resources), Locks)locker2_check_available#(Resource, Locks)
locker2_remove_pending#(Lock, Client)record_extract#(Lock, lock, pending)istops#(E1, stack(E2, S1))eqt#(E1, E2)
locker2_check_availables#(cons(Resource, Resources), Locks)locker2_check_availables#(Resources, Locks)locker2_obtainables#(cons(Lock, Locks), Client)record_extract#(Lock, lock, pending)
case5#(Client, Locks, Lock, false)locker2_obtainables#(Locks, Client)element#(int(s(s(N1))), tuple(T1, T2))element#(int(s(N1)), T2)
case9#(Tail, Head, E, false)member#(E, Tail)locker2_add_pending#(Lock, Resources, Client)member#(record_extract(Lock, lock, resource), Resources)
case6#(Locks, Lock, Resource, true)record_extract#(Lock, lock, pending)locker2_promote_pending#(Lock, Client)case0#(Client, Lock, record_extract(Lock, lock, pending))
case8#(Tail, Head, E, false)delete#(E, Tail)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))eqc#(calls(E1, S1, CS1), calls(E2, S2, CS2))eqc#(CS1, CS2)
eqt#(cons(H1, T1), cons(H2, T2))and#(eqt(H1, H2), eqt(T1, T2))case0#(Client, Lock, cons(Client, Pendings))record_updates#(Lock, lock, cons(tuple(excl, tuplenil(Client)), cons(tuple(pending, tuplenil(Pendings)), nil)))
delete#(E, cons(Head, Tail))case8#(Tail, Head, E, equal(E, Head))push#(E1, E2, calls(E3, S1, CS1))push1#(E1, E2, E3, S1, CS1, eqt(E1, E3))
eqc#(calls(E1, S1, CS1), calls(E2, S2, CS2))eqs#(S1, S2)case1#(Client, Resources, Lock, true)record_extract#(Lock, lock, pending)
append#(cons(Head, Tail), List)append#(Tail, List)eqt#(tuplenil(H1), tuplenil(H2))eqt#(H1, H2)
locker2_check_available#(Resource, cons(Lock, Locks))case6#(Locks, Lock, Resource, equal(Resource, record_extract(Lock, lock, resource)))record_updates#(Record, Name, cons(tuple(Field, tuplenil(NewF)), Fields))record_updates#(record_update(Record, Name, Field, NewF), Name, Fields)
locker2_remove_pending#(Lock, Client)subtract#(record_extract(Lock, lock, pending), cons(Client, nil))case6#(Locks, Lock, Resource, false)locker2_check_available#(Resource, Locks)
locker2_release_lock#(Lock, Client)gen_modtageq#(Client, record_extract(Lock, lock, excl))locker2_add_pending#(Lock, Resources, Client)record_extract#(Lock, lock, resource)
eqt#(tuple(H1, T1), tuple(H2, T2))eqt#(T1, T2)locker2_remove_pending#(Lock, Client)record_updates#(Lock, lock, cons(tuple(pending, tuplenil(subtract(record_extract(Lock, lock, pending), cons(Client, nil)))), nil))
eqt#(cons(H1, T1), cons(H2, T2))eqt#(H1, H2)eqc#(calls(E1, S1, CS1), calls(E2, S2, CS2))eqt#(E1, E2)
eqs#(stack(E1, S1), stack(E2, S2))eqt#(E1, E2)locker2_map_claim_lock#(cons(Lock, Locks), Resources, Client)locker2_map_claim_lock#(Locks, Resources, Client)
eqt#(tuple(H1, T1), tuple(H2, T2))eqt#(H1, H2)locker2_map_promote_pending#(cons(Lock, Locks), Pending)locker2_promote_pending#(Lock, Pending)
case5#(Client, Locks, Lock, true)locker2_obtainables#(Locks, Client)locker2_add_pending#(Lock, Resources, Client)case1#(Client, Resources, Lock, member(record_extract(Lock, lock, resource), Resources))
locker2_release_lock#(Lock, Client)record_extract#(Lock, lock, excl)locker2_promote_pending#(Lock, Client)record_extract#(Lock, lock, pending)
eqt#(cons(H1, T1), cons(H2, T2))eqt#(T1, T2)push1#(E1, E2, E3, S1, CS1, T)pushs#(E2, S1)
record_updates#(Record, Name, cons(tuple(Field, tuplenil(NewF)), Fields))record_update#(Record, Name, Field, NewF)push#(E1, E2, calls(E3, S1, CS1))eqt#(E1, E3)
eqc#(calls(E1, S1, CS1), calls(E2, S2, CS2))and#(eqs(S1, S2), eqc(CS1, CS2))subtract#(List, cons(Head, Tail))subtract#(delete(Head, List), Tail)
case1#(Client, Resources, Lock, true)append#(record_extract(Lock, lock, pending), cons(Client, nil))member#(E, cons(Head, Tail))case9#(Tail, Head, E, equal(E, Head))
case1#(Client, Resources, Lock, true)record_updates#(Lock, lock, cons(tuple(pending, tuplenil(append(record_extract(Lock, lock, pending), cons(Client, nil)))), nil))

Rewrite Rules

or(T, T)Tor(F, T)T
or(T, F)Tor(F, F)F
and(T, B)Band(B, T)B
and(F, B)Fand(B, F)F
imp(T, B)Bimp(F, B)T
not(T)Fnot(F)T
if(T, B1, B2)B1if(F, B1, B2)B2
eq(T, T)Teq(F, F)T
eq(T, F)Feq(F, T)F
eqt(nil, undefined)Feqt(nil, pid(N2))F
eqt(nil, int(N2))Feqt(nil, cons(H2, T2))F
eqt(nil, tuple(H2, T2))Feqt(nil, tuplenil(H2))F
eqt(a, nil)Feqt(a, a)T
eqt(a, excl)Feqt(a, false)F
eqt(a, lock)Feqt(a, locker)F
eqt(a, mcrlrecord)Feqt(a, ok)F
eqt(a, pending)Feqt(a, release)F
eqt(a, request)Feqt(a, resource)F
eqt(a, tag)Feqt(a, true)F
eqt(a, undefined)Feqt(a, pid(N2))F
eqt(a, int(N2))Feqt(a, cons(H2, T2))F
eqt(a, tuple(H2, T2))Feqt(a, tuplenil(H2))F
eqt(excl, nil)Feqt(excl, a)F
eqt(excl, excl)Teqt(excl, false)F
eqt(excl, lock)Feqt(excl, locker)F
eqt(excl, mcrlrecord)Feqt(excl, ok)F
eqt(excl, pending)Feqt(excl, release)F
eqt(excl, request)Feqt(excl, resource)F
eqt(excl, tag)Feqt(excl, true)F
eqt(excl, undefined)Feqt(excl, pid(N2))F
eqt(excl, eqt(false, int(N2)))Feqt(false, cons(H2, T2))F
eqt(false, tuple(H2, T2))Feqt(false, tuplenil(H2))F
eqt(lock, nil)Feqt(lock, a)F
eqt(lock, excl)Feqt(lock, false)F
eqt(lock, lock)Teqt(lock, locker)F
eqt(lock, mcrlrecord)Feqt(lock, ok)F
eqt(lock, pending)Feqt(lock, release)F
eqt(lock, request)Feqt(lock, resource)F
eqt(lock, tag)Feqt(lock, true)F
eqt(lock, undefined)Feqt(lock, pid(N2))F
eqt(lock, int(N2))Feqt(lock, cons(H2, T2))F
eqt(lock, tuple(H2, T2))Feqt(lock, tuplenil(H2))F
eqt(locker, nil)Feqt(locker, a)F
eqt(locker, excl)Feqt(locker, false)F
eqt(locker, lock)Feqt(locker, locker)T
eqt(locker, mcrlrecord)Feqt(locker, ok)F
eqt(locker, pending)Feqt(locker, release)F
eqt(locker, request)Feqt(locker, resource)F
eqt(locker, tag)Feqt(locker, true)F
eqt(locker, undefined)Feqt(locker, pid(N2))F
eqt(locker, int(N2))Feqt(locker, cons(H2, T2))F
eqt(locker, tuple(H2, T2))Feqt(locker, tuplenil(H2))F
eqt(mcrlrecord, nil)Feqt(mcrlrecord, a)F
eqt(mcrlrecord, excl)Feqt(mcrlrecord, false)F
eqt(mcrlrecord, lock)Feqt(mcrlrecord, locker)F
eqt(mcrlrecord, mcrlrecord)Teqt(mcrlrecord, ok)F
eqt(mcrlrecord, pending)Feqt(mcrlrecord, release)F
eqt(mcrlrecord, request)Feqt(mcrlrecord, resource)F
eqt(ok, resource)Feqt(ok, tag)F
eqt(ok, true)Feqt(ok, undefined)F
eqt(ok, pid(N2))Feqt(ok, int(N2))F
eqt(ok, cons(H2, T2))Feqt(ok, tuple(H2, T2))F
eqt(ok, tuplenil(H2))Feqt(pending, nil)F
eqt(pending, a)Feqt(pending, excl)F
eqt(pending, false)Feqt(pending, lock)F
eqt(pending, locker)Feqt(pending, mcrlrecord)F
eqt(pending, ok)Feqt(pending, pending)T
eqt(pending, release)Feqt(pending, request)F
eqt(pending, resource)Feqt(pending, tag)F
eqt(pending, true)Feqt(pending, undefined)F
eqt(pending, pid(N2))Feqt(pending, int(N2))F
eqt(pending, cons(H2, T2))Feqt(pending, tuple(H2, T2))F
eqt(pending, tuplenil(H2))Feqt(release, nil)F
eqt(release, a)Feqt(release, excl)F
eqt(release, false)Feqt(release, lock)F
eqt(release, locker)Feqt(release, mcrlrecord)F
eqt(release, ok)Feqt(request, mcrlrecord)F
eqt(request, ok)Feqt(request, pending)F
eqt(request, release)Feqt(request, request)T
eqt(request, resource)Feqt(request, tag)F
eqt(request, true)Feqt(request, undefined)F
eqt(request, pid(N2))Feqt(request, int(N2))F
eqt(request, cons(H2, T2))Feqt(request, tuple(H2, T2))F
eqt(request, tuplenil(H2))Feqt(resource, nil)F
eqt(resource, a)Feqt(resource, excl)F
eqt(resource, false)Feqt(resource, lock)F
eqt(resource, locker)Feqt(resource, mcrlrecord)F
eqt(resource, ok)Feqt(resource, pending)F
eqt(resource, release)Feqt(resource, request)F
eqt(resource, resource)Teqt(resource, tag)F
eqt(resource, true)Feqt(resource, undefined)F
eqt(resource, pid(N2))Feqt(resource, int(N2))F
eqt(resource, cons(H2, T2))Feqt(resource, tuple(H2, T2))F
eqt(resource, tuplenil(H2))Feqt(tag, nil)F
eqt(tag, a)Feqt(tag, excl)F
eqt(tag, false)Feqt(tag, lock)F
eqt(tag, locker)Feqt(tag, mcrlrecord)F
eqt(tag, ok)Feqt(tag, pending)F
eqt(tag, release)Feqt(tag, request)F
eqt(tag, resource)Feqt(tag, tag)T
eqt(tag, true)Feqt(tag, undefined)F
eqt(tag, pid(N2))Feqt(tag, int(N2))F
eqt(tag, cons(H2, T2))Feqt(tag, tuple(H2, T2))F
eqt(tag, tuplenil(H2))Feqt(true, nil)F
eqt(true, a)Feqt(true, excl)F
eqt(true, false)Feqt(true, lock)F
eqt(true, locker)Feqt(true, mcrlrecord)F
eqt(true, ok)Feqt(true, pending)F
eqt(true, release)Feqt(true, request)F
eqt(true, resource)Feqt(true, tag)F
eqt(true, true)Teqt(true, undefined)F
eqt(true, pid(N2))Feqt(true, int(N2))F
eqt(true, cons(H2, T2))Feqt(true, tuple(H2, T2))F
eqt(true, tuplenil(H2))Feqt(undefined, nil)F
eqt(undefined, a)Feqt(undefined, tuplenil(H2))F
eqt(pid(N1), nil)Feqt(pid(N1), a)F
eqt(pid(N1), excl)Feqt(pid(N1), false)F
eqt(pid(N1), lock)Feqt(pid(N1), locker)F
eqt(pid(N1), mcrlrecord)Feqt(pid(N1), ok)F
eqt(pid(N1), pending)Feqt(pid(N1), release)F
eqt(pid(N1), request)Feqt(pid(N1), resource)F
eqt(pid(N1), tag)Feqt(pid(N1), true)F
eqt(pid(N1), undefined)Feqt(pid(N1), pid(N2))eqt(N1, N2)
eqt(pid(N1), int(N2))Feqt(pid(N1), cons(H2, T2))F
eqt(pid(N1), tuple(H2, T2))Feqt(pid(N1), tuplenil(H2))F
eqt(int(N1), nil)Feqt(int(N1), a)F
eqt(int(N1), excl)Feqt(int(N1), false)F
eqt(int(N1), lock)Feqt(int(N1), locker)F
eqt(int(N1), mcrlrecord)Feqt(int(N1), ok)F
eqt(int(N1), pending)Feqt(int(N1), release)F
eqt(int(N1), request)Feqt(int(N1), resource)F
eqt(int(N1), tag)Feqt(int(N1), true)F
eqt(int(N1), undefined)Feqt(cons(H1, T1), resource)F
eqt(cons(H1, T1), tag)Feqt(cons(H1, T1), true)F
eqt(cons(H1, T1), undefined)Feqt(cons(H1, T1), pid(N2))F
eqt(cons(H1, T1), int(N2))Feqt(cons(H1, T1), cons(H2, T2))and(eqt(H1, H2), eqt(T1, T2))
eqt(cons(H1, T1), tuple(H2, T2))Feqt(cons(H1, T1), tuplenil(H2))F
eqt(tuple(H1, T1), nil)Feqt(tuple(H1, T1), a)F
eqt(tuple(H1, T1), excl)Feqt(tuple(H1, T1), false)F
eqt(tuple(H1, T1), lock)Feqt(tuple(H1, T1), locker)F
eqt(tuple(H1, T1), mcrlrecord)Feqt(tuple(H1, T1), ok)F
eqt(tuple(H1, T1), pending)Feqt(tuple(H1, T1), release)F
eqt(tuple(H1, T1), request)Feqt(tuple(H1, T1), resource)F
eqt(tuple(H1, T1), tag)Feqt(tuple(H1, T1), true)F
eqt(tuple(H1, T1), undefined)Feqt(tuple(H1, T1), pid(N2))F
eqt(tuple(H1, T1), int(N2))Feqt(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)Feqt(tuplenil(H1), a)F
eqt(tuplenil(H1), excl)Feqt(tuplenil(H1), false)F
eqt(tuplenil(H1), lock)Feqt(tuplenil(H1), locker)F
eqt(tuplenil(H1), mcrlrecord)Feqt(tuplenil(H1), ok)F
eqt(tuplenil(H1), pending)Feqt(tuplenil(H1), release)F
eqt(tuplenil(H1), request)Feqt(tuplenil(H1), resource)F
eqt(tuplenil(H1), tag)Feqt(tuplenil(H1), true)F
eqt(tuplenil(H1), undefined)Feqt(tuplenil(H1), pid(N2))F
eqt(tuplenil(H1), int(N2))Feqt(tuplenil(H1), cons(H2, T2))F
eqt(tuplenil(H1), tuple(H2, T2))Feqt(tuplenil(H1), tuplenil(H2))eqt(H1, H2)
element(int(s(0)), tuplenil(T1))T1element(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)Recordrecord_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)nillocker2_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)nillocker2_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)nillocker2_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)falselocker2_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))Feqs(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))S1tops(stack(E1, S1))E1
istops(E1, empty)Fistops(E1, stack(E2, S1))eqt(E1, E2)
eqc(nocalls, nocalls)Teqc(nocalls, calls(E2, S2, CS2))F
eqc(calls(E1, S1, CS1), nocalls)Feqc(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)

Original Signature

Termination of terms over the following signature is verified: tuplenil, record_new, tuple, tag, gen_tag, imp, locker2_map_promote_pending, pops, locker2_check_availables, mcrlrecord, pending, request, empty, false, ok, istops, locker2_add_pending, andt, case2, append, element, case1, case0, tops, push1, case6, case5, or, int, case4, record_extract, locker, case9, case8, locker2_map_add_pending, calls, eqc, and, not, 0, locker2_promote_pending, locker2_claim_lock, locker2_adduniq, stack, release, locker2_obtainables, F, locker2_remove_pending, push, T, gen_modtageq, record_update, undefined, if, record_updates, eqt, excllock, delete, eqs, cons, member, locker2_map_claim_lock, locker2_obtainable, a, pushs, resource, lock, true, locker2_release_lock, pid, equal, subtract, locker2_check_available, s, excl, nil, eq, nocalls

Strategy


The following SCCs where found

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

eqt#(pid(N1), pid(N2)) → eqt#(N1, N2)eqt#(tuple(H1, T1), tuple(H2, T2)) → eqt#(T1, T2)
eqt#(tuple(H1, T1), tuple(H2, T2)) → eqt#(H1, H2)eqt#(cons(H1, T1), cons(H2, T2)) → eqt#(H1, H2)
eqt#(tuplenil(H1), tuplenil(H2)) → eqt#(H1, H2)eqt#(cons(H1, T1), cons(H2, T2)) → eqt#(T1, T2)

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

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

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)

subtract#(List, cons(Head, Tail)) → subtract#(delete(Head, List), Tail)

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

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

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

case5#(Client, Locks, Lock, true) → locker2_obtainables#(Locks, Client)case5#(Client, Locks, Lock, false) → locker2_obtainables#(Locks, Client)
locker2_obtainables#(cons(Lock, Locks), Client) → case5#(Client, Locks, Lock, member(Client, record_extract(Lock, lock, pending)))

Problem 2: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

or(T, T)Tor(F, T)T
or(T, F)Tor(F, F)F
and(T, B)Band(B, T)B
and(F, B)Fand(B, F)F
imp(T, B)Bimp(F, B)T
not(T)Fnot(F)T
if(T, B1, B2)B1if(F, B1, B2)B2
eq(T, T)Teq(F, F)T
eq(T, F)Feq(F, T)F
eqt(nil, undefined)Feqt(nil, pid(N2))F
eqt(nil, int(N2))Feqt(nil, cons(H2, T2))F
eqt(nil, tuple(H2, T2))Feqt(nil, tuplenil(H2))F
eqt(a, nil)Feqt(a, a)T
eqt(a, excl)Feqt(a, false)F
eqt(a, lock)Feqt(a, locker)F
eqt(a, mcrlrecord)Feqt(a, ok)F
eqt(a, pending)Feqt(a, release)F
eqt(a, request)Feqt(a, resource)F
eqt(a, tag)Feqt(a, true)F
eqt(a, undefined)Feqt(a, pid(N2))F
eqt(a, int(N2))Feqt(a, cons(H2, T2))F
eqt(a, tuple(H2, T2))Feqt(a, tuplenil(H2))F
eqt(excl, nil)Feqt(excl, a)F
eqt(excl, excl)Teqt(excl, false)F
eqt(excl, lock)Feqt(excl, locker)F
eqt(excl, mcrlrecord)Feqt(excl, ok)F
eqt(excl, pending)Feqt(excl, release)F
eqt(excl, request)Feqt(excl, resource)F
eqt(excl, tag)Feqt(excl, true)F
eqt(excl, undefined)Feqt(excl, pid(N2))F
eqt(excl, eqt(false, int(N2)))Feqt(false, cons(H2, T2))F
eqt(false, tuple(H2, T2))Feqt(false, tuplenil(H2))F
eqt(lock, nil)Feqt(lock, a)F
eqt(lock, excl)Feqt(lock, false)F
eqt(lock, lock)Teqt(lock, locker)F
eqt(lock, mcrlrecord)Feqt(lock, ok)F
eqt(lock, pending)Feqt(lock, release)F
eqt(lock, request)Feqt(lock, resource)F
eqt(lock, tag)Feqt(lock, true)F
eqt(lock, undefined)Feqt(lock, pid(N2))F
eqt(lock, int(N2))Feqt(lock, cons(H2, T2))F
eqt(lock, tuple(H2, T2))Feqt(lock, tuplenil(H2))F
eqt(locker, nil)Feqt(locker, a)F
eqt(locker, excl)Feqt(locker, false)F
eqt(locker, lock)Feqt(locker, locker)T
eqt(locker, mcrlrecord)Feqt(locker, ok)F
eqt(locker, pending)Feqt(locker, release)F
eqt(locker, request)Feqt(locker, resource)F
eqt(locker, tag)Feqt(locker, true)F
eqt(locker, undefined)Feqt(locker, pid(N2))F
eqt(locker, int(N2))Feqt(locker, cons(H2, T2))F
eqt(locker, tuple(H2, T2))Feqt(locker, tuplenil(H2))F
eqt(mcrlrecord, nil)Feqt(mcrlrecord, a)F
eqt(mcrlrecord, excl)Feqt(mcrlrecord, false)F
eqt(mcrlrecord, lock)Feqt(mcrlrecord, locker)F
eqt(mcrlrecord, mcrlrecord)Teqt(mcrlrecord, ok)F
eqt(mcrlrecord, pending)Feqt(mcrlrecord, release)F
eqt(mcrlrecord, request)Feqt(mcrlrecord, resource)F
eqt(ok, resource)Feqt(ok, tag)F
eqt(ok, true)Feqt(ok, undefined)F
eqt(ok, pid(N2))Feqt(ok, int(N2))F
eqt(ok, cons(H2, T2))Feqt(ok, tuple(H2, T2))F
eqt(ok, tuplenil(H2))Feqt(pending, nil)F
eqt(pending, a)Feqt(pending, excl)F
eqt(pending, false)Feqt(pending, lock)F
eqt(pending, locker)Feqt(pending, mcrlrecord)F
eqt(pending, ok)Feqt(pending, pending)T
eqt(pending, release)Feqt(pending, request)F
eqt(pending, resource)Feqt(pending, tag)F
eqt(pending, true)Feqt(pending, undefined)F
eqt(pending, pid(N2))Feqt(pending, int(N2))F
eqt(pending, cons(H2, T2))Feqt(pending, tuple(H2, T2))F
eqt(pending, tuplenil(H2))Feqt(release, nil)F
eqt(release, a)Feqt(release, excl)F
eqt(release, false)Feqt(release, lock)F
eqt(release, locker)Feqt(release, mcrlrecord)F
eqt(release, ok)Feqt(request, mcrlrecord)F
eqt(request, ok)Feqt(request, pending)F
eqt(request, release)Feqt(request, request)T
eqt(request, resource)Feqt(request, tag)F
eqt(request, true)Feqt(request, undefined)F
eqt(request, pid(N2))Feqt(request, int(N2))F
eqt(request, cons(H2, T2))Feqt(request, tuple(H2, T2))F
eqt(request, tuplenil(H2))Feqt(resource, nil)F
eqt(resource, a)Feqt(resource, excl)F
eqt(resource, false)Feqt(resource, lock)F
eqt(resource, locker)Feqt(resource, mcrlrecord)F
eqt(resource, ok)Feqt(resource, pending)F
eqt(resource, release)Feqt(resource, request)F
eqt(resource, resource)Teqt(resource, tag)F
eqt(resource, true)Feqt(resource, undefined)F
eqt(resource, pid(N2))Feqt(resource, int(N2))F
eqt(resource, cons(H2, T2))Feqt(resource, tuple(H2, T2))F
eqt(resource, tuplenil(H2))Feqt(tag, nil)F
eqt(tag, a)Feqt(tag, excl)F
eqt(tag, false)Feqt(tag, lock)F
eqt(tag, locker)Feqt(tag, mcrlrecord)F
eqt(tag, ok)Feqt(tag, pending)F
eqt(tag, release)Feqt(tag, request)F
eqt(tag, resource)Feqt(tag, tag)T
eqt(tag, true)Feqt(tag, undefined)F
eqt(tag, pid(N2))Feqt(tag, int(N2))F
eqt(tag, cons(H2, T2))Feqt(tag, tuple(H2, T2))F
eqt(tag, tuplenil(H2))Feqt(true, nil)F
eqt(true, a)Feqt(true, excl)F
eqt(true, false)Feqt(true, lock)F
eqt(true, locker)Feqt(true, mcrlrecord)F
eqt(true, ok)Feqt(true, pending)F
eqt(true, release)Feqt(true, request)F
eqt(true, resource)Feqt(true, tag)F
eqt(true, true)Teqt(true, undefined)F
eqt(true, pid(N2))Feqt(true, int(N2))F
eqt(true, cons(H2, T2))Feqt(true, tuple(H2, T2))F
eqt(true, tuplenil(H2))Feqt(undefined, nil)F
eqt(undefined, a)Feqt(undefined, tuplenil(H2))F
eqt(pid(N1), nil)Feqt(pid(N1), a)F
eqt(pid(N1), excl)Feqt(pid(N1), false)F
eqt(pid(N1), lock)Feqt(pid(N1), locker)F
eqt(pid(N1), mcrlrecord)Feqt(pid(N1), ok)F
eqt(pid(N1), pending)Feqt(pid(N1), release)F
eqt(pid(N1), request)Feqt(pid(N1), resource)F
eqt(pid(N1), tag)Feqt(pid(N1), true)F
eqt(pid(N1), undefined)Feqt(pid(N1), pid(N2))eqt(N1, N2)
eqt(pid(N1), int(N2))Feqt(pid(N1), cons(H2, T2))F
eqt(pid(N1), tuple(H2, T2))Feqt(pid(N1), tuplenil(H2))F
eqt(int(N1), nil)Feqt(int(N1), a)F
eqt(int(N1), excl)Feqt(int(N1), false)F
eqt(int(N1), lock)Feqt(int(N1), locker)F
eqt(int(N1), mcrlrecord)Feqt(int(N1), ok)F
eqt(int(N1), pending)Feqt(int(N1), release)F
eqt(int(N1), request)Feqt(int(N1), resource)F
eqt(int(N1), tag)Feqt(int(N1), true)F
eqt(int(N1), undefined)Feqt(cons(H1, T1), resource)F
eqt(cons(H1, T1), tag)Feqt(cons(H1, T1), true)F
eqt(cons(H1, T1), undefined)Feqt(cons(H1, T1), pid(N2))F
eqt(cons(H1, T1), int(N2))Feqt(cons(H1, T1), cons(H2, T2))and(eqt(H1, H2), eqt(T1, T2))
eqt(cons(H1, T1), tuple(H2, T2))Feqt(cons(H1, T1), tuplenil(H2))F
eqt(tuple(H1, T1), nil)Feqt(tuple(H1, T1), a)F
eqt(tuple(H1, T1), excl)Feqt(tuple(H1, T1), false)F
eqt(tuple(H1, T1), lock)Feqt(tuple(H1, T1), locker)F
eqt(tuple(H1, T1), mcrlrecord)Feqt(tuple(H1, T1), ok)F
eqt(tuple(H1, T1), pending)Feqt(tuple(H1, T1), release)F
eqt(tuple(H1, T1), request)Feqt(tuple(H1, T1), resource)F
eqt(tuple(H1, T1), tag)Feqt(tuple(H1, T1), true)F
eqt(tuple(H1, T1), undefined)Feqt(tuple(H1, T1), pid(N2))F
eqt(tuple(H1, T1), int(N2))Feqt(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)Feqt(tuplenil(H1), a)F
eqt(tuplenil(H1), excl)Feqt(tuplenil(H1), false)F
eqt(tuplenil(H1), lock)Feqt(tuplenil(H1), locker)F
eqt(tuplenil(H1), mcrlrecord)Feqt(tuplenil(H1), ok)F
eqt(tuplenil(H1), pending)Feqt(tuplenil(H1), release)F
eqt(tuplenil(H1), request)Feqt(tuplenil(H1), resource)F
eqt(tuplenil(H1), tag)Feqt(tuplenil(H1), true)F
eqt(tuplenil(H1), undefined)Feqt(tuplenil(H1), pid(N2))F
eqt(tuplenil(H1), int(N2))Feqt(tuplenil(H1), cons(H2, T2))F
eqt(tuplenil(H1), tuple(H2, T2))Feqt(tuplenil(H1), tuplenil(H2))eqt(H1, H2)
element(int(s(0)), tuplenil(T1))T1element(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)Recordrecord_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)nillocker2_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)nillocker2_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)nillocker2_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)falselocker2_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))Feqs(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))S1tops(stack(E1, S1))E1
istops(E1, empty)Fistops(E1, stack(E2, S1))eqt(E1, E2)
eqc(nocalls, nocalls)Teqc(nocalls, calls(E2, S2, CS2))F
eqc(calls(E1, S1, CS1), nocalls)Feqc(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)

Original Signature

Termination of terms over the following signature is verified: tuplenil, record_new, tuple, tag, gen_tag, imp, locker2_map_promote_pending, pops, locker2_check_availables, mcrlrecord, pending, request, empty, false, ok, istops, locker2_add_pending, andt, case2, append, element, case1, case0, tops, push1, case6, case5, or, int, case4, record_extract, locker, case9, case8, locker2_map_add_pending, calls, eqc, and, not, 0, locker2_promote_pending, locker2_claim_lock, locker2_adduniq, stack, release, locker2_obtainables, F, locker2_remove_pending, push, T, gen_modtageq, record_update, undefined, if, record_updates, eqt, excllock, delete, eqs, cons, member, locker2_map_claim_lock, locker2_obtainable, a, pushs, resource, lock, true, locker2_release_lock, pid, equal, subtract, locker2_check_available, s, excl, nil, eq, nocalls

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 3: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

or(T, T)Tor(F, T)T
or(T, F)Tor(F, F)F
and(T, B)Band(B, T)B
and(F, B)Fand(B, F)F
imp(T, B)Bimp(F, B)T
not(T)Fnot(F)T
if(T, B1, B2)B1if(F, B1, B2)B2
eq(T, T)Teq(F, F)T
eq(T, F)Feq(F, T)F
eqt(nil, undefined)Feqt(nil, pid(N2))F
eqt(nil, int(N2))Feqt(nil, cons(H2, T2))F
eqt(nil, tuple(H2, T2))Feqt(nil, tuplenil(H2))F
eqt(a, nil)Feqt(a, a)T
eqt(a, excl)Feqt(a, false)F
eqt(a, lock)Feqt(a, locker)F
eqt(a, mcrlrecord)Feqt(a, ok)F
eqt(a, pending)Feqt(a, release)F
eqt(a, request)Feqt(a, resource)F
eqt(a, tag)Feqt(a, true)F
eqt(a, undefined)Feqt(a, pid(N2))F
eqt(a, int(N2))Feqt(a, cons(H2, T2))F
eqt(a, tuple(H2, T2))Feqt(a, tuplenil(H2))F
eqt(excl, nil)Feqt(excl, a)F
eqt(excl, excl)Teqt(excl, false)F
eqt(excl, lock)Feqt(excl, locker)F
eqt(excl, mcrlrecord)Feqt(excl, ok)F
eqt(excl, pending)Feqt(excl, release)F
eqt(excl, request)Feqt(excl, resource)F
eqt(excl, tag)Feqt(excl, true)F
eqt(excl, undefined)Feqt(excl, pid(N2))F
eqt(excl, eqt(false, int(N2)))Feqt(false, cons(H2, T2))F
eqt(false, tuple(H2, T2))Feqt(false, tuplenil(H2))F
eqt(lock, nil)Feqt(lock, a)F
eqt(lock, excl)Feqt(lock, false)F
eqt(lock, lock)Teqt(lock, locker)F
eqt(lock, mcrlrecord)Feqt(lock, ok)F
eqt(lock, pending)Feqt(lock, release)F
eqt(lock, request)Feqt(lock, resource)F
eqt(lock, tag)Feqt(lock, true)F
eqt(lock, undefined)Feqt(lock, pid(N2))F
eqt(lock, int(N2))Feqt(lock, cons(H2, T2))F
eqt(lock, tuple(H2, T2))Feqt(lock, tuplenil(H2))F
eqt(locker, nil)Feqt(locker, a)F
eqt(locker, excl)Feqt(locker, false)F
eqt(locker, lock)Feqt(locker, locker)T
eqt(locker, mcrlrecord)Feqt(locker, ok)F
eqt(locker, pending)Feqt(locker, release)F
eqt(locker, request)Feqt(locker, resource)F
eqt(locker, tag)Feqt(locker, true)F
eqt(locker, undefined)Feqt(locker, pid(N2))F
eqt(locker, int(N2))Feqt(locker, cons(H2, T2))F
eqt(locker, tuple(H2, T2))Feqt(locker, tuplenil(H2))F
eqt(mcrlrecord, nil)Feqt(mcrlrecord, a)F
eqt(mcrlrecord, excl)Feqt(mcrlrecord, false)F
eqt(mcrlrecord, lock)Feqt(mcrlrecord, locker)F
eqt(mcrlrecord, mcrlrecord)Teqt(mcrlrecord, ok)F
eqt(mcrlrecord, pending)Feqt(mcrlrecord, release)F
eqt(mcrlrecord, request)Feqt(mcrlrecord, resource)F
eqt(ok, resource)Feqt(ok, tag)F
eqt(ok, true)Feqt(ok, undefined)F
eqt(ok, pid(N2))Feqt(ok, int(N2))F
eqt(ok, cons(H2, T2))Feqt(ok, tuple(H2, T2))F
eqt(ok, tuplenil(H2))Feqt(pending, nil)F
eqt(pending, a)Feqt(pending, excl)F
eqt(pending, false)Feqt(pending, lock)F
eqt(pending, locker)Feqt(pending, mcrlrecord)F
eqt(pending, ok)Feqt(pending, pending)T
eqt(pending, release)Feqt(pending, request)F
eqt(pending, resource)Feqt(pending, tag)F
eqt(pending, true)Feqt(pending, undefined)F
eqt(pending, pid(N2))Feqt(pending, int(N2))F
eqt(pending, cons(H2, T2))Feqt(pending, tuple(H2, T2))F
eqt(pending, tuplenil(H2))Feqt(release, nil)F
eqt(release, a)Feqt(release, excl)F
eqt(release, false)Feqt(release, lock)F
eqt(release, locker)Feqt(release, mcrlrecord)F
eqt(release, ok)Feqt(request, mcrlrecord)F
eqt(request, ok)Feqt(request, pending)F
eqt(request, release)Feqt(request, request)T
eqt(request, resource)Feqt(request, tag)F
eqt(request, true)Feqt(request, undefined)F
eqt(request, pid(N2))Feqt(request, int(N2))F
eqt(request, cons(H2, T2))Feqt(request, tuple(H2, T2))F
eqt(request, tuplenil(H2))Feqt(resource, nil)F
eqt(resource, a)Feqt(resource, excl)F
eqt(resource, false)Feqt(resource, lock)F
eqt(resource, locker)Feqt(resource, mcrlrecord)F
eqt(resource, ok)Feqt(resource, pending)F
eqt(resource, release)Feqt(resource, request)F
eqt(resource, resource)Teqt(resource, tag)F
eqt(resource, true)Feqt(resource, undefined)F
eqt(resource, pid(N2))Feqt(resource, int(N2))F
eqt(resource, cons(H2, T2))Feqt(resource, tuple(H2, T2))F
eqt(resource, tuplenil(H2))Feqt(tag, nil)F
eqt(tag, a)Feqt(tag, excl)F
eqt(tag, false)Feqt(tag, lock)F
eqt(tag, locker)Feqt(tag, mcrlrecord)F
eqt(tag, ok)Feqt(tag, pending)F
eqt(tag, release)Feqt(tag, request)F
eqt(tag, resource)Feqt(tag, tag)T
eqt(tag, true)Feqt(tag, undefined)F
eqt(tag, pid(N2))Feqt(tag, int(N2))F
eqt(tag, cons(H2, T2))Feqt(tag, tuple(H2, T2))F
eqt(tag, tuplenil(H2))Feqt(true, nil)F
eqt(true, a)Feqt(true, excl)F
eqt(true, false)Feqt(true, lock)F
eqt(true, locker)Feqt(true, mcrlrecord)F
eqt(true, ok)Feqt(true, pending)F
eqt(true, release)Feqt(true, request)F
eqt(true, resource)Feqt(true, tag)F
eqt(true, true)Teqt(true, undefined)F
eqt(true, pid(N2))Feqt(true, int(N2))F
eqt(true, cons(H2, T2))Feqt(true, tuple(H2, T2))F
eqt(true, tuplenil(H2))Feqt(undefined, nil)F
eqt(undefined, a)Feqt(undefined, tuplenil(H2))F
eqt(pid(N1), nil)Feqt(pid(N1), a)F
eqt(pid(N1), excl)Feqt(pid(N1), false)F
eqt(pid(N1), lock)Feqt(pid(N1), locker)F
eqt(pid(N1), mcrlrecord)Feqt(pid(N1), ok)F
eqt(pid(N1), pending)Feqt(pid(N1), release)F
eqt(pid(N1), request)Feqt(pid(N1), resource)F
eqt(pid(N1), tag)Feqt(pid(N1), true)F
eqt(pid(N1), undefined)Feqt(pid(N1), pid(N2))eqt(N1, N2)
eqt(pid(N1), int(N2))Feqt(pid(N1), cons(H2, T2))F
eqt(pid(N1), tuple(H2, T2))Feqt(pid(N1), tuplenil(H2))F
eqt(int(N1), nil)Feqt(int(N1), a)F
eqt(int(N1), excl)Feqt(int(N1), false)F
eqt(int(N1), lock)Feqt(int(N1), locker)F
eqt(int(N1), mcrlrecord)Feqt(int(N1), ok)F
eqt(int(N1), pending)Feqt(int(N1), release)F
eqt(int(N1), request)Feqt(int(N1), resource)F
eqt(int(N1), tag)Feqt(int(N1), true)F
eqt(int(N1), undefined)Feqt(cons(H1, T1), resource)F
eqt(cons(H1, T1), tag)Feqt(cons(H1, T1), true)F
eqt(cons(H1, T1), undefined)Feqt(cons(H1, T1), pid(N2))F
eqt(cons(H1, T1), int(N2))Feqt(cons(H1, T1), cons(H2, T2))and(eqt(H1, H2), eqt(T1, T2))
eqt(cons(H1, T1), tuple(H2, T2))Feqt(cons(H1, T1), tuplenil(H2))F
eqt(tuple(H1, T1), nil)Feqt(tuple(H1, T1), a)F
eqt(tuple(H1, T1), excl)Feqt(tuple(H1, T1), false)F
eqt(tuple(H1, T1), lock)Feqt(tuple(H1, T1), locker)F
eqt(tuple(H1, T1), mcrlrecord)Feqt(tuple(H1, T1), ok)F
eqt(tuple(H1, T1), pending)Feqt(tuple(H1, T1), release)F
eqt(tuple(H1, T1), request)Feqt(tuple(H1, T1), resource)F
eqt(tuple(H1, T1), tag)Feqt(tuple(H1, T1), true)F
eqt(tuple(H1, T1), undefined)Feqt(tuple(H1, T1), pid(N2))F
eqt(tuple(H1, T1), int(N2))Feqt(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)Feqt(tuplenil(H1), a)F
eqt(tuplenil(H1), excl)Feqt(tuplenil(H1), false)F
eqt(tuplenil(H1), lock)Feqt(tuplenil(H1), locker)F
eqt(tuplenil(H1), mcrlrecord)Feqt(tuplenil(H1), ok)F
eqt(tuplenil(H1), pending)Feqt(tuplenil(H1), release)F
eqt(tuplenil(H1), request)Feqt(tuplenil(H1), resource)F
eqt(tuplenil(H1), tag)Feqt(tuplenil(H1), true)F
eqt(tuplenil(H1), undefined)Feqt(tuplenil(H1), pid(N2))F
eqt(tuplenil(H1), int(N2))Feqt(tuplenil(H1), cons(H2, T2))F
eqt(tuplenil(H1), tuple(H2, T2))Feqt(tuplenil(H1), tuplenil(H2))eqt(H1, H2)
element(int(s(0)), tuplenil(T1))T1element(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)Recordrecord_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)nillocker2_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)nillocker2_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)nillocker2_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)falselocker2_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))Feqs(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))S1tops(stack(E1, S1))E1
istops(E1, empty)Fistops(E1, stack(E2, S1))eqt(E1, E2)
eqc(nocalls, nocalls)Teqc(nocalls, calls(E2, S2, CS2))F
eqc(calls(E1, S1, CS1), nocalls)Feqc(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)

Original Signature

Termination of terms over the following signature is verified: tuplenil, record_new, tuple, tag, gen_tag, imp, locker2_map_promote_pending, pops, locker2_check_availables, mcrlrecord, pending, request, empty, false, ok, istops, locker2_add_pending, andt, case2, append, element, case1, case0, tops, push1, case6, case5, or, int, case4, record_extract, locker, case9, case8, locker2_map_add_pending, calls, eqc, and, not, 0, locker2_promote_pending, locker2_claim_lock, locker2_adduniq, stack, release, locker2_obtainables, F, locker2_remove_pending, push, T, gen_modtageq, record_update, undefined, if, record_updates, eqt, excllock, delete, eqs, cons, member, locker2_map_claim_lock, locker2_obtainable, a, pushs, resource, lock, true, locker2_release_lock, pid, equal, subtract, locker2_check_available, s, excl, nil, eq, nocalls

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 4: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

or(T, T)Tor(F, T)T
or(T, F)Tor(F, F)F
and(T, B)Band(B, T)B
and(F, B)Fand(B, F)F
imp(T, B)Bimp(F, B)T
not(T)Fnot(F)T
if(T, B1, B2)B1if(F, B1, B2)B2
eq(T, T)Teq(F, F)T
eq(T, F)Feq(F, T)F
eqt(nil, undefined)Feqt(nil, pid(N2))F
eqt(nil, int(N2))Feqt(nil, cons(H2, T2))F
eqt(nil, tuple(H2, T2))Feqt(nil, tuplenil(H2))F
eqt(a, nil)Feqt(a, a)T
eqt(a, excl)Feqt(a, false)F
eqt(a, lock)Feqt(a, locker)F
eqt(a, mcrlrecord)Feqt(a, ok)F
eqt(a, pending)Feqt(a, release)F
eqt(a, request)Feqt(a, resource)F
eqt(a, tag)Feqt(a, true)F
eqt(a, undefined)Feqt(a, pid(N2))F
eqt(a, int(N2))Feqt(a, cons(H2, T2))F
eqt(a, tuple(H2, T2))Feqt(a, tuplenil(H2))F
eqt(excl, nil)Feqt(excl, a)F
eqt(excl, excl)Teqt(excl, false)F
eqt(excl, lock)Feqt(excl, locker)F
eqt(excl, mcrlrecord)Feqt(excl, ok)F
eqt(excl, pending)Feqt(excl, release)F
eqt(excl, request)Feqt(excl, resource)F
eqt(excl, tag)Feqt(excl, true)F
eqt(excl, undefined)Feqt(excl, pid(N2))F
eqt(excl, eqt(false, int(N2)))Feqt(false, cons(H2, T2))F
eqt(false, tuple(H2, T2))Feqt(false, tuplenil(H2))F
eqt(lock, nil)Feqt(lock, a)F
eqt(lock, excl)Feqt(lock, false)F
eqt(lock, lock)Teqt(lock, locker)F
eqt(lock, mcrlrecord)Feqt(lock, ok)F
eqt(lock, pending)Feqt(lock, release)F
eqt(lock, request)Feqt(lock, resource)F
eqt(lock, tag)Feqt(lock, true)F
eqt(lock, undefined)Feqt(lock, pid(N2))F
eqt(lock, int(N2))Feqt(lock, cons(H2, T2))F
eqt(lock, tuple(H2, T2))Feqt(lock, tuplenil(H2))F
eqt(locker, nil)Feqt(locker, a)F
eqt(locker, excl)Feqt(locker, false)F
eqt(locker, lock)Feqt(locker, locker)T
eqt(locker, mcrlrecord)Feqt(locker, ok)F
eqt(locker, pending)Feqt(locker, release)F
eqt(locker, request)Feqt(locker, resource)F
eqt(locker, tag)Feqt(locker, true)F
eqt(locker, undefined)Feqt(locker, pid(N2))F
eqt(locker, int(N2))Feqt(locker, cons(H2, T2))F
eqt(locker, tuple(H2, T2))Feqt(locker, tuplenil(H2))F
eqt(mcrlrecord, nil)Feqt(mcrlrecord, a)F
eqt(mcrlrecord, excl)Feqt(mcrlrecord, false)F
eqt(mcrlrecord, lock)Feqt(mcrlrecord, locker)F
eqt(mcrlrecord, mcrlrecord)Teqt(mcrlrecord, ok)F
eqt(mcrlrecord, pending)Feqt(mcrlrecord, release)F
eqt(mcrlrecord, request)Feqt(mcrlrecord, resource)F
eqt(ok, resource)Feqt(ok, tag)F
eqt(ok, true)Feqt(ok, undefined)F
eqt(ok, pid(N2))Feqt(ok, int(N2))F
eqt(ok, cons(H2, T2))Feqt(ok, tuple(H2, T2))F
eqt(ok, tuplenil(H2))Feqt(pending, nil)F
eqt(pending, a)Feqt(pending, excl)F
eqt(pending, false)Feqt(pending, lock)F
eqt(pending, locker)Feqt(pending, mcrlrecord)F
eqt(pending, ok)Feqt(pending, pending)T
eqt(pending, release)Feqt(pending, request)F
eqt(pending, resource)Feqt(pending, tag)F
eqt(pending, true)Feqt(pending, undefined)F
eqt(pending, pid(N2))Feqt(pending, int(N2))F
eqt(pending, cons(H2, T2))Feqt(pending, tuple(H2, T2))F
eqt(pending, tuplenil(H2))Feqt(release, nil)F
eqt(release, a)Feqt(release, excl)F
eqt(release, false)Feqt(release, lock)F
eqt(release, locker)Feqt(release, mcrlrecord)F
eqt(release, ok)Feqt(request, mcrlrecord)F
eqt(request, ok)Feqt(request, pending)F
eqt(request, release)Feqt(request, request)T
eqt(request, resource)Feqt(request, tag)F
eqt(request, true)Feqt(request, undefined)F
eqt(request, pid(N2))Feqt(request, int(N2))F
eqt(request, cons(H2, T2))Feqt(request, tuple(H2, T2))F
eqt(request, tuplenil(H2))Feqt(resource, nil)F
eqt(resource, a)Feqt(resource, excl)F
eqt(resource, false)Feqt(resource, lock)F
eqt(resource, locker)Feqt(resource, mcrlrecord)F
eqt(resource, ok)Feqt(resource, pending)F
eqt(resource, release)Feqt(resource, request)F
eqt(resource, resource)Teqt(resource, tag)F
eqt(resource, true)Feqt(resource, undefined)F
eqt(resource, pid(N2))Feqt(resource, int(N2))F
eqt(resource, cons(H2, T2))Feqt(resource, tuple(H2, T2))F
eqt(resource, tuplenil(H2))Feqt(tag, nil)F
eqt(tag, a)Feqt(tag, excl)F
eqt(tag, false)Feqt(tag, lock)F
eqt(tag, locker)Feqt(tag, mcrlrecord)F
eqt(tag, ok)Feqt(tag, pending)F
eqt(tag, release)Feqt(tag, request)F
eqt(tag, resource)Feqt(tag, tag)T
eqt(tag, true)Feqt(tag, undefined)F
eqt(tag, pid(N2))Feqt(tag, int(N2))F
eqt(tag, cons(H2, T2))Feqt(tag, tuple(H2, T2))F
eqt(tag, tuplenil(H2))Feqt(true, nil)F
eqt(true, a)Feqt(true, excl)F
eqt(true, false)Feqt(true, lock)F
eqt(true, locker)Feqt(true, mcrlrecord)F
eqt(true, ok)Feqt(true, pending)F
eqt(true, release)Feqt(true, request)F
eqt(true, resource)Feqt(true, tag)F
eqt(true, true)Teqt(true, undefined)F
eqt(true, pid(N2))Feqt(true, int(N2))F
eqt(true, cons(H2, T2))Feqt(true, tuple(H2, T2))F
eqt(true, tuplenil(H2))Feqt(undefined, nil)F
eqt(undefined, a)Feqt(undefined, tuplenil(H2))F
eqt(pid(N1), nil)Feqt(pid(N1), a)F
eqt(pid(N1), excl)Feqt(pid(N1), false)F
eqt(pid(N1), lock)Feqt(pid(N1), locker)F
eqt(pid(N1), mcrlrecord)Feqt(pid(N1), ok)F
eqt(pid(N1), pending)Feqt(pid(N1), release)F
eqt(pid(N1), request)Feqt(pid(N1), resource)F
eqt(pid(N1), tag)Feqt(pid(N1), true)F
eqt(pid(N1), undefined)Feqt(pid(N1), pid(N2))eqt(N1, N2)
eqt(pid(N1), int(N2))Feqt(pid(N1), cons(H2, T2))F
eqt(pid(N1), tuple(H2, T2))Feqt(pid(N1), tuplenil(H2))F
eqt(int(N1), nil)Feqt(int(N1), a)F
eqt(int(N1), excl)Feqt(int(N1), false)F
eqt(int(N1), lock)Feqt(int(N1), locker)F
eqt(int(N1), mcrlrecord)Feqt(int(N1), ok)F
eqt(int(N1), pending)Feqt(int(N1), release)F
eqt(int(N1), request)Feqt(int(N1), resource)F
eqt(int(N1), tag)Feqt(int(N1), true)F
eqt(int(N1), undefined)Feqt(cons(H1, T1), resource)F
eqt(cons(H1, T1), tag)Feqt(cons(H1, T1), true)F
eqt(cons(H1, T1), undefined)Feqt(cons(H1, T1), pid(N2))F
eqt(cons(H1, T1), int(N2))Feqt(cons(H1, T1), cons(H2, T2))and(eqt(H1, H2), eqt(T1, T2))
eqt(cons(H1, T1), tuple(H2, T2))Feqt(cons(H1, T1), tuplenil(H2))F
eqt(tuple(H1, T1), nil)Feqt(tuple(H1, T1), a)F
eqt(tuple(H1, T1), excl)Feqt(tuple(H1, T1), false)F
eqt(tuple(H1, T1), lock)Feqt(tuple(H1, T1), locker)F
eqt(tuple(H1, T1), mcrlrecord)Feqt(tuple(H1, T1), ok)F
eqt(tuple(H1, T1), pending)Feqt(tuple(H1, T1), release)F
eqt(tuple(H1, T1), request)Feqt(tuple(H1, T1), resource)F
eqt(tuple(H1, T1), tag)Feqt(tuple(H1, T1), true)F
eqt(tuple(H1, T1), undefined)Feqt(tuple(H1, T1), pid(N2))F
eqt(tuple(H1, T1), int(N2))Feqt(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)Feqt(tuplenil(H1), a)F
eqt(tuplenil(H1), excl)Feqt(tuplenil(H1), false)F
eqt(tuplenil(H1), lock)Feqt(tuplenil(H1), locker)F
eqt(tuplenil(H1), mcrlrecord)Feqt(tuplenil(H1), ok)F
eqt(tuplenil(H1), pending)Feqt(tuplenil(H1), release)F
eqt(tuplenil(H1), request)Feqt(tuplenil(H1), resource)F
eqt(tuplenil(H1), tag)Feqt(tuplenil(H1), true)F
eqt(tuplenil(H1), undefined)Feqt(tuplenil(H1), pid(N2))F
eqt(tuplenil(H1), int(N2))Feqt(tuplenil(H1), cons(H2, T2))F
eqt(tuplenil(H1), tuple(H2, T2))Feqt(tuplenil(H1), tuplenil(H2))eqt(H1, H2)
element(int(s(0)), tuplenil(T1))T1element(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)Recordrecord_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)nillocker2_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)nillocker2_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)nillocker2_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)falselocker2_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))Feqs(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))S1tops(stack(E1, S1))E1
istops(E1, empty)Fistops(E1, stack(E2, S1))eqt(E1, E2)
eqc(nocalls, nocalls)Teqc(nocalls, calls(E2, S2, CS2))F
eqc(calls(E1, S1, CS1), nocalls)Feqc(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)

Original Signature

Termination of terms over the following signature is verified: tuplenil, record_new, tuple, tag, gen_tag, imp, locker2_map_promote_pending, pops, locker2_check_availables, mcrlrecord, pending, request, empty, false, ok, istops, locker2_add_pending, andt, case2, append, element, case1, case0, tops, push1, case6, case5, or, int, case4, record_extract, locker, case9, case8, locker2_map_add_pending, calls, eqc, and, not, 0, locker2_promote_pending, locker2_claim_lock, locker2_adduniq, stack, release, locker2_obtainables, F, locker2_remove_pending, push, T, gen_modtageq, record_update, undefined, if, record_updates, eqt, excllock, delete, eqs, cons, member, locker2_map_claim_lock, locker2_obtainable, a, pushs, resource, lock, true, locker2_release_lock, pid, equal, subtract, locker2_check_available, s, excl, nil, eq, nocalls

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 5: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

or(T, T)Tor(F, T)T
or(T, F)Tor(F, F)F
and(T, B)Band(B, T)B
and(F, B)Fand(B, F)F
imp(T, B)Bimp(F, B)T
not(T)Fnot(F)T
if(T, B1, B2)B1if(F, B1, B2)B2
eq(T, T)Teq(F, F)T
eq(T, F)Feq(F, T)F
eqt(nil, undefined)Feqt(nil, pid(N2))F
eqt(nil, int(N2))Feqt(nil, cons(H2, T2))F
eqt(nil, tuple(H2, T2))Feqt(nil, tuplenil(H2))F
eqt(a, nil)Feqt(a, a)T
eqt(a, excl)Feqt(a, false)F
eqt(a, lock)Feqt(a, locker)F
eqt(a, mcrlrecord)Feqt(a, ok)F
eqt(a, pending)Feqt(a, release)F
eqt(a, request)Feqt(a, resource)F
eqt(a, tag)Feqt(a, true)F
eqt(a, undefined)Feqt(a, pid(N2))F
eqt(a, int(N2))Feqt(a, cons(H2, T2))F
eqt(a, tuple(H2, T2))Feqt(a, tuplenil(H2))F
eqt(excl, nil)Feqt(excl, a)F
eqt(excl, excl)Teqt(excl, false)F
eqt(excl, lock)Feqt(excl, locker)F
eqt(excl, mcrlrecord)Feqt(excl, ok)F
eqt(excl, pending)Feqt(excl, release)F
eqt(excl, request)Feqt(excl, resource)F
eqt(excl, tag)Feqt(excl, true)F
eqt(excl, undefined)Feqt(excl, pid(N2))F
eqt(excl, eqt(false, int(N2)))Feqt(false, cons(H2, T2))F
eqt(false, tuple(H2, T2))Feqt(false, tuplenil(H2))F
eqt(lock, nil)Feqt(lock, a)F
eqt(lock, excl)Feqt(lock, false)F
eqt(lock, lock)Teqt(lock, locker)F
eqt(lock, mcrlrecord)Feqt(lock, ok)F
eqt(lock, pending)Feqt(lock, release)F
eqt(lock, request)Feqt(lock, resource)F
eqt(lock, tag)Feqt(lock, true)F
eqt(lock, undefined)Feqt(lock, pid(N2))F
eqt(lock, int(N2))Feqt(lock, cons(H2, T2))F
eqt(lock, tuple(H2, T2))Feqt(lock, tuplenil(H2))F
eqt(locker, nil)Feqt(locker, a)F
eqt(locker, excl)Feqt(locker, false)F
eqt(locker, lock)Feqt(locker, locker)T
eqt(locker, mcrlrecord)Feqt(locker, ok)F
eqt(locker, pending)Feqt(locker, release)F
eqt(locker, request)Feqt(locker, resource)F
eqt(locker, tag)Feqt(locker, true)F
eqt(locker, undefined)Feqt(locker, pid(N2))F
eqt(locker, int(N2))Feqt(locker, cons(H2, T2))F
eqt(locker, tuple(H2, T2))Feqt(locker, tuplenil(H2))F
eqt(mcrlrecord, nil)Feqt(mcrlrecord, a)F
eqt(mcrlrecord, excl)Feqt(mcrlrecord, false)F
eqt(mcrlrecord, lock)Feqt(mcrlrecord, locker)F
eqt(mcrlrecord, mcrlrecord)Teqt(mcrlrecord, ok)F
eqt(mcrlrecord, pending)Feqt(mcrlrecord, release)F
eqt(mcrlrecord, request)Feqt(mcrlrecord, resource)F
eqt(ok, resource)Feqt(ok, tag)F
eqt(ok, true)Feqt(ok, undefined)F
eqt(ok, pid(N2))Feqt(ok, int(N2))F
eqt(ok, cons(H2, T2))Feqt(ok, tuple(H2, T2))F
eqt(ok, tuplenil(H2))Feqt(pending, nil)F
eqt(pending, a)Feqt(pending, excl)F
eqt(pending, false)Feqt(pending, lock)F
eqt(pending, locker)Feqt(pending, mcrlrecord)F
eqt(pending, ok)Feqt(pending, pending)T
eqt(pending, release)Feqt(pending, request)F
eqt(pending, resource)Feqt(pending, tag)F
eqt(pending, true)Feqt(pending, undefined)F
eqt(pending, pid(N2))Feqt(pending, int(N2))F
eqt(pending, cons(H2, T2))Feqt(pending, tuple(H2, T2))F
eqt(pending, tuplenil(H2))Feqt(release, nil)F
eqt(release, a)Feqt(release, excl)F
eqt(release, false)Feqt(release, lock)F
eqt(release, locker)Feqt(release, mcrlrecord)F
eqt(release, ok)Feqt(request, mcrlrecord)F
eqt(request, ok)Feqt(request, pending)F
eqt(request, release)Feqt(request, request)T
eqt(request, resource)Feqt(request, tag)F
eqt(request, true)Feqt(request, undefined)F
eqt(request, pid(N2))Feqt(request, int(N2))F
eqt(request, cons(H2, T2))Feqt(request, tuple(H2, T2))F
eqt(request, tuplenil(H2))Feqt(resource, nil)F
eqt(resource, a)Feqt(resource, excl)F
eqt(resource, false)Feqt(resource, lock)F
eqt(resource, locker)Feqt(resource, mcrlrecord)F
eqt(resource, ok)Feqt(resource, pending)F
eqt(resource, release)Feqt(resource, request)F
eqt(resource, resource)Teqt(resource, tag)F
eqt(resource, true)Feqt(resource, undefined)F
eqt(resource, pid(N2))Feqt(resource, int(N2))F
eqt(resource, cons(H2, T2))Feqt(resource, tuple(H2, T2))F
eqt(resource, tuplenil(H2))Feqt(tag, nil)F
eqt(tag, a)Feqt(tag, excl)F
eqt(tag, false)Feqt(tag, lock)F
eqt(tag, locker)Feqt(tag, mcrlrecord)F
eqt(tag, ok)Feqt(tag, pending)F
eqt(tag, release)Feqt(tag, request)F
eqt(tag, resource)Feqt(tag, tag)T
eqt(tag, true)Feqt(tag, undefined)F
eqt(tag, pid(N2))Feqt(tag, int(N2))F
eqt(tag, cons(H2, T2))Feqt(tag, tuple(H2, T2))F
eqt(tag, tuplenil(H2))Feqt(true, nil)F
eqt(true, a)Feqt(true, excl)F
eqt(true, false)Feqt(true, lock)F
eqt(true, locker)Feqt(true, mcrlrecord)F
eqt(true, ok)Feqt(true, pending)F
eqt(true, release)Feqt(true, request)F
eqt(true, resource)Feqt(true, tag)F
eqt(true, true)Teqt(true, undefined)F
eqt(true, pid(N2))Feqt(true, int(N2))F
eqt(true, cons(H2, T2))Feqt(true, tuple(H2, T2))F
eqt(true, tuplenil(H2))Feqt(undefined, nil)F
eqt(undefined, a)Feqt(undefined, tuplenil(H2))F
eqt(pid(N1), nil)Feqt(pid(N1), a)F
eqt(pid(N1), excl)Feqt(pid(N1), false)F
eqt(pid(N1), lock)Feqt(pid(N1), locker)F
eqt(pid(N1), mcrlrecord)Feqt(pid(N1), ok)F
eqt(pid(N1), pending)Feqt(pid(N1), release)F
eqt(pid(N1), request)Feqt(pid(N1), resource)F
eqt(pid(N1), tag)Feqt(pid(N1), true)F
eqt(pid(N1), undefined)Feqt(pid(N1), pid(N2))eqt(N1, N2)
eqt(pid(N1), int(N2))Feqt(pid(N1), cons(H2, T2))F
eqt(pid(N1), tuple(H2, T2))Feqt(pid(N1), tuplenil(H2))F
eqt(int(N1), nil)Feqt(int(N1), a)F
eqt(int(N1), excl)Feqt(int(N1), false)F
eqt(int(N1), lock)Feqt(int(N1), locker)F
eqt(int(N1), mcrlrecord)Feqt(int(N1), ok)F
eqt(int(N1), pending)Feqt(int(N1), release)F
eqt(int(N1), request)Feqt(int(N1), resource)F
eqt(int(N1), tag)Feqt(int(N1), true)F
eqt(int(N1), undefined)Feqt(cons(H1, T1), resource)F
eqt(cons(H1, T1), tag)Feqt(cons(H1, T1), true)F
eqt(cons(H1, T1), undefined)Feqt(cons(H1, T1), pid(N2))F
eqt(cons(H1, T1), int(N2))Feqt(cons(H1, T1), cons(H2, T2))and(eqt(H1, H2), eqt(T1, T2))
eqt(cons(H1, T1), tuple(H2, T2))Feqt(cons(H1, T1), tuplenil(H2))F
eqt(tuple(H1, T1), nil)Feqt(tuple(H1, T1), a)F
eqt(tuple(H1, T1), excl)Feqt(tuple(H1, T1), false)F
eqt(tuple(H1, T1), lock)Feqt(tuple(H1, T1), locker)F
eqt(tuple(H1, T1), mcrlrecord)Feqt(tuple(H1, T1), ok)F
eqt(tuple(H1, T1), pending)Feqt(tuple(H1, T1), release)F
eqt(tuple(H1, T1), request)Feqt(tuple(H1, T1), resource)F
eqt(tuple(H1, T1), tag)Feqt(tuple(H1, T1), true)F
eqt(tuple(H1, T1), undefined)Feqt(tuple(H1, T1), pid(N2))F
eqt(tuple(H1, T1), int(N2))Feqt(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)Feqt(tuplenil(H1), a)F
eqt(tuplenil(H1), excl)Feqt(tuplenil(H1), false)F
eqt(tuplenil(H1), lock)Feqt(tuplenil(H1), locker)F
eqt(tuplenil(H1), mcrlrecord)Feqt(tuplenil(H1), ok)F
eqt(tuplenil(H1), pending)Feqt(tuplenil(H1), release)F
eqt(tuplenil(H1), request)Feqt(tuplenil(H1), resource)F
eqt(tuplenil(H1), tag)Feqt(tuplenil(H1), true)F
eqt(tuplenil(H1), undefined)Feqt(tuplenil(H1), pid(N2))F
eqt(tuplenil(H1), int(N2))Feqt(tuplenil(H1), cons(H2, T2))F
eqt(tuplenil(H1), tuple(H2, T2))Feqt(tuplenil(H1), tuplenil(H2))eqt(H1, H2)
element(int(s(0)), tuplenil(T1))T1element(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)Recordrecord_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)nillocker2_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)nillocker2_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)nillocker2_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)falselocker2_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))Feqs(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))S1tops(stack(E1, S1))E1
istops(E1, empty)Fistops(E1, stack(E2, S1))eqt(E1, E2)
eqc(nocalls, nocalls)Teqc(nocalls, calls(E2, S2, CS2))F
eqc(calls(E1, S1, CS1), nocalls)Feqc(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)

Original Signature

Termination of terms over the following signature is verified: tuplenil, record_new, tuple, tag, gen_tag, imp, locker2_map_promote_pending, pops, locker2_check_availables, mcrlrecord, pending, request, empty, false, ok, istops, locker2_add_pending, andt, case2, append, element, case1, case0, tops, push1, case6, case5, or, int, case4, record_extract, locker, case9, case8, locker2_map_add_pending, calls, eqc, and, not, 0, locker2_promote_pending, locker2_claim_lock, locker2_adduniq, stack, release, locker2_obtainables, F, locker2_remove_pending, push, T, gen_modtageq, record_update, undefined, if, record_updates, eqt, excllock, delete, eqs, cons, member, locker2_map_claim_lock, locker2_obtainable, a, pushs, resource, lock, true, locker2_release_lock, pid, equal, subtract, locker2_check_available, s, excl, nil, eq, nocalls

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 6: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

case5#(Client, Locks, Lock, true)locker2_obtainables#(Locks, Client)case5#(Client, Locks, Lock, false)locker2_obtainables#(Locks, Client)
locker2_obtainables#(cons(Lock, Locks), Client)case5#(Client, Locks, Lock, member(Client, record_extract(Lock, lock, pending)))

Rewrite Rules

or(T, T)Tor(F, T)T
or(T, F)Tor(F, F)F
and(T, B)Band(B, T)B
and(F, B)Fand(B, F)F
imp(T, B)Bimp(F, B)T
not(T)Fnot(F)T
if(T, B1, B2)B1if(F, B1, B2)B2
eq(T, T)Teq(F, F)T
eq(T, F)Feq(F, T)F
eqt(nil, undefined)Feqt(nil, pid(N2))F
eqt(nil, int(N2))Feqt(nil, cons(H2, T2))F
eqt(nil, tuple(H2, T2))Feqt(nil, tuplenil(H2))F
eqt(a, nil)Feqt(a, a)T
eqt(a, excl)Feqt(a, false)F
eqt(a, lock)Feqt(a, locker)F
eqt(a, mcrlrecord)Feqt(a, ok)F
eqt(a, pending)Feqt(a, release)F
eqt(a, request)Feqt(a, resource)F
eqt(a, tag)Feqt(a, true)F
eqt(a, undefined)Feqt(a, pid(N2))F
eqt(a, int(N2))Feqt(a, cons(H2, T2))F
eqt(a, tuple(H2, T2))Feqt(a, tuplenil(H2))F
eqt(excl, nil)Feqt(excl, a)F
eqt(excl, excl)Teqt(excl, false)F
eqt(excl, lock)Feqt(excl, locker)F
eqt(excl, mcrlrecord)Feqt(excl, ok)F
eqt(excl, pending)Feqt(excl, release)F
eqt(excl, request)Feqt(excl, resource)F
eqt(excl, tag)Feqt(excl, true)F
eqt(excl, undefined)Feqt(excl, pid(N2))F
eqt(excl, eqt(false, int(N2)))Feqt(false, cons(H2, T2))F
eqt(false, tuple(H2, T2))Feqt(false, tuplenil(H2))F
eqt(lock, nil)Feqt(lock, a)F
eqt(lock, excl)Feqt(lock, false)F
eqt(lock, lock)Teqt(lock, locker)F
eqt(lock, mcrlrecord)Feqt(lock, ok)F
eqt(lock, pending)Feqt(lock, release)F
eqt(lock, request)Feqt(lock, resource)F
eqt(lock, tag)Feqt(lock, true)F
eqt(lock, undefined)Feqt(lock, pid(N2))F
eqt(lock, int(N2))Feqt(lock, cons(H2, T2))F
eqt(lock, tuple(H2, T2))Feqt(lock, tuplenil(H2))F
eqt(locker, nil)Feqt(locker, a)F
eqt(locker, excl)Feqt(locker, false)F
eqt(locker, lock)Feqt(locker, locker)T
eqt(locker, mcrlrecord)Feqt(locker, ok)F
eqt(locker, pending)Feqt(locker, release)F
eqt(locker, request)Feqt(locker, resource)F
eqt(locker, tag)Feqt(locker, true)F
eqt(locker, undefined)Feqt(locker, pid(N2))F
eqt(locker, int(N2))Feqt(locker, cons(H2, T2))F
eqt(locker, tuple(H2, T2))Feqt(locker, tuplenil(H2))F
eqt(mcrlrecord, nil)Feqt(mcrlrecord, a)F
eqt(mcrlrecord, excl)Feqt(mcrlrecord, false)F
eqt(mcrlrecord, lock)Feqt(mcrlrecord, locker)F
eqt(mcrlrecord, mcrlrecord)Teqt(mcrlrecord, ok)F
eqt(mcrlrecord, pending)Feqt(mcrlrecord, release)F
eqt(mcrlrecord, request)Feqt(mcrlrecord, resource)F
eqt(ok, resource)Feqt(ok, tag)F
eqt(ok, true)Feqt(ok, undefined)F
eqt(ok, pid(N2))Feqt(ok, int(N2))F
eqt(ok, cons(H2, T2))Feqt(ok, tuple(H2, T2))F
eqt(ok, tuplenil(H2))Feqt(pending, nil)F
eqt(pending, a)Feqt(pending, excl)F
eqt(pending, false)Feqt(pending, lock)F
eqt(pending, locker)Feqt(pending, mcrlrecord)F
eqt(pending, ok)Feqt(pending, pending)T
eqt(pending, release)Feqt(pending, request)F
eqt(pending, resource)Feqt(pending, tag)F
eqt(pending, true)Feqt(pending, undefined)F
eqt(pending, pid(N2))Feqt(pending, int(N2))F
eqt(pending, cons(H2, T2))Feqt(pending, tuple(H2, T2))F
eqt(pending, tuplenil(H2))Feqt(release, nil)F
eqt(release, a)Feqt(release, excl)F
eqt(release, false)Feqt(release, lock)F
eqt(release, locker)Feqt(release, mcrlrecord)F
eqt(release, ok)Feqt(request, mcrlrecord)F
eqt(request, ok)Feqt(request, pending)F
eqt(request, release)Feqt(request, request)T
eqt(request, resource)Feqt(request, tag)F
eqt(request, true)Feqt(request, undefined)F
eqt(request, pid(N2))Feqt(request, int(N2))F
eqt(request, cons(H2, T2))Feqt(request, tuple(H2, T2))F
eqt(request, tuplenil(H2))Feqt(resource, nil)F
eqt(resource, a)Feqt(resource, excl)F
eqt(resource, false)Feqt(resource, lock)F
eqt(resource, locker)Feqt(resource, mcrlrecord)F
eqt(resource, ok)Feqt(resource, pending)F
eqt(resource, release)Feqt(resource, request)F
eqt(resource, resource)Teqt(resource, tag)F
eqt(resource, true)Feqt(resource, undefined)F
eqt(resource, pid(N2))Feqt(resource, int(N2))F
eqt(resource, cons(H2, T2))Feqt(resource, tuple(H2, T2))F
eqt(resource, tuplenil(H2))Feqt(tag, nil)F
eqt(tag, a)Feqt(tag, excl)F
eqt(tag, false)Feqt(tag, lock)F
eqt(tag, locker)Feqt(tag, mcrlrecord)F
eqt(tag, ok)Feqt(tag, pending)F
eqt(tag, release)Feqt(tag, request)F
eqt(tag, resource)Feqt(tag, tag)T
eqt(tag, true)Feqt(tag, undefined)F
eqt(tag, pid(N2))Feqt(tag, int(N2))F
eqt(tag, cons(H2, T2))Feqt(tag, tuple(H2, T2))F
eqt(tag, tuplenil(H2))Feqt(true, nil)F
eqt(true, a)Feqt(true, excl)F
eqt(true, false)Feqt(true, lock)F
eqt(true, locker)Feqt(true, mcrlrecord)F
eqt(true, ok)Feqt(true, pending)F
eqt(true, release)Feqt(true, request)F
eqt(true, resource)Feqt(true, tag)F
eqt(true, true)Teqt(true, undefined)F
eqt(true, pid(N2))Feqt(true, int(N2))F
eqt(true, cons(H2, T2))Feqt(true, tuple(H2, T2))F
eqt(true, tuplenil(H2))Feqt(undefined, nil)F
eqt(undefined, a)Feqt(undefined, tuplenil(H2))F
eqt(pid(N1), nil)Feqt(pid(N1), a)F
eqt(pid(N1), excl)Feqt(pid(N1), false)F
eqt(pid(N1), lock)Feqt(pid(N1), locker)F
eqt(pid(N1), mcrlrecord)Feqt(pid(N1), ok)F
eqt(pid(N1), pending)Feqt(pid(N1), release)F
eqt(pid(N1), request)Feqt(pid(N1), resource)F
eqt(pid(N1), tag)Feqt(pid(N1), true)F
eqt(pid(N1), undefined)Feqt(pid(N1), pid(N2))eqt(N1, N2)
eqt(pid(N1), int(N2))Feqt(pid(N1), cons(H2, T2))F
eqt(pid(N1), tuple(H2, T2))Feqt(pid(N1), tuplenil(H2))F
eqt(int(N1), nil)Feqt(int(N1), a)F
eqt(int(N1), excl)Feqt(int(N1), false)F
eqt(int(N1), lock)Feqt(int(N1), locker)F
eqt(int(N1), mcrlrecord)Feqt(int(N1), ok)F
eqt(int(N1), pending)Feqt(int(N1), release)F
eqt(int(N1), request)Feqt(int(N1), resource)F
eqt(int(N1), tag)Feqt(int(N1), true)F
eqt(int(N1), undefined)Feqt(cons(H1, T1), resource)F
eqt(cons(H1, T1), tag)Feqt(cons(H1, T1), true)F
eqt(cons(H1, T1), undefined)Feqt(cons(H1, T1), pid(N2))F
eqt(cons(H1, T1), int(N2))Feqt(cons(H1, T1), cons(H2, T2))and(eqt(H1, H2), eqt(T1, T2))
eqt(cons(H1, T1), tuple(H2, T2))Feqt(cons(H1, T1), tuplenil(H2))F
eqt(tuple(H1, T1), nil)Feqt(tuple(H1, T1), a)F
eqt(tuple(H1, T1), excl)Feqt(tuple(H1, T1), false)F
eqt(tuple(H1, T1), lock)Feqt(tuple(H1, T1), locker)F
eqt(tuple(H1, T1), mcrlrecord)Feqt(tuple(H1, T1), ok)F
eqt(tuple(H1, T1), pending)Feqt(tuple(H1, T1), release)F
eqt(tuple(H1, T1), request)Feqt(tuple(H1, T1), resource)F
eqt(tuple(H1, T1), tag)Feqt(tuple(H1, T1), true)F
eqt(tuple(H1, T1), undefined)Feqt(tuple(H1, T1), pid(N2))F
eqt(tuple(H1, T1), int(N2))Feqt(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)Feqt(tuplenil(H1), a)F
eqt(tuplenil(H1), excl)Feqt(tuplenil(H1), false)F
eqt(tuplenil(H1), lock)Feqt(tuplenil(H1), locker)F
eqt(tuplenil(H1), mcrlrecord)Feqt(tuplenil(H1), ok)F
eqt(tuplenil(H1), pending)Feqt(tuplenil(H1), release)F
eqt(tuplenil(H1), request)Feqt(tuplenil(H1), resource)F
eqt(tuplenil(H1), tag)Feqt(tuplenil(H1), true)F
eqt(tuplenil(H1), undefined)Feqt(tuplenil(H1), pid(N2))F
eqt(tuplenil(H1), int(N2))Feqt(tuplenil(H1), cons(H2, T2))F
eqt(tuplenil(H1), tuple(H2, T2))Feqt(tuplenil(H1), tuplenil(H2))eqt(H1, H2)
element(int(s(0)), tuplenil(T1))T1element(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)Recordrecord_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)nillocker2_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)nillocker2_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)nillocker2_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)falselocker2_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))Feqs(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))S1tops(stack(E1, S1))E1
istops(E1, empty)Fistops(E1, stack(E2, S1))eqt(E1, E2)
eqc(nocalls, nocalls)Teqc(nocalls, calls(E2, S2, CS2))F
eqc(calls(E1, S1, CS1), nocalls)Feqc(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)

Original Signature

Termination of terms over the following signature is verified: tuplenil, record_new, tuple, tag, gen_tag, imp, locker2_map_promote_pending, pops, locker2_check_availables, mcrlrecord, pending, request, empty, false, ok, istops, locker2_add_pending, andt, case2, append, element, case1, case0, tops, push1, case6, case5, or, int, case4, record_extract, locker, case9, case8, locker2_map_add_pending, calls, eqc, and, not, 0, locker2_promote_pending, locker2_claim_lock, locker2_adduniq, stack, release, locker2_obtainables, F, locker2_remove_pending, push, T, gen_modtageq, record_update, undefined, if, record_updates, eqt, excllock, delete, eqs, cons, member, locker2_map_claim_lock, locker2_obtainable, a, pushs, resource, lock, true, locker2_release_lock, pid, equal, subtract, locker2_check_available, s, excl, nil, eq, nocalls

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

locker2_obtainables#(cons(Lock, Locks), Client)case5#(Client, Locks, Lock, member(Client, record_extract(Lock, lock, pending)))

Problem 13: DependencyGraph



Dependency Pair Problem

Dependency Pairs

case5#(Client, Locks, Lock, true)locker2_obtainables#(Locks, Client)case5#(Client, Locks, Lock, false)locker2_obtainables#(Locks, Client)

Rewrite Rules

or(T, T)Tor(F, T)T
or(T, F)Tor(F, F)F
and(T, B)Band(B, T)B
and(F, B)Fand(B, F)F
imp(T, B)Bimp(F, B)T
not(T)Fnot(F)T
if(T, B1, B2)B1if(F, B1, B2)B2
eq(T, T)Teq(F, F)T
eq(T, F)Feq(F, T)F
eqt(nil, undefined)Feqt(nil, pid(N2))F
eqt(nil, int(N2))Feqt(nil, cons(H2, T2))F
eqt(nil, tuple(H2, T2))Feqt(nil, tuplenil(H2))F
eqt(a, nil)Feqt(a, a)T
eqt(a, excl)Feqt(a, false)F
eqt(a, lock)Feqt(a, locker)F
eqt(a, mcrlrecord)Feqt(a, ok)F
eqt(a, pending)Feqt(a, release)F
eqt(a, request)Feqt(a, resource)F
eqt(a, tag)Feqt(a, true)F
eqt(a, undefined)Feqt(a, pid(N2))F
eqt(a, int(N2))Feqt(a, cons(H2, T2))F
eqt(a, tuple(H2, T2))Feqt(a, tuplenil(H2))F
eqt(excl, nil)Feqt(excl, a)F
eqt(excl, excl)Teqt(excl, false)F
eqt(excl, lock)Feqt(excl, locker)F
eqt(excl, mcrlrecord)Feqt(excl, ok)F
eqt(excl, pending)Feqt(excl, release)F
eqt(excl, request)Feqt(excl, resource)F
eqt(excl, tag)Feqt(excl, true)F
eqt(excl, undefined)Feqt(excl, pid(N2))F
eqt(excl, eqt(false, int(N2)))Feqt(false, cons(H2, T2))F
eqt(false, tuple(H2, T2))Feqt(false, tuplenil(H2))F
eqt(lock, nil)Feqt(lock, a)F
eqt(lock, excl)Feqt(lock, false)F
eqt(lock, lock)Teqt(lock, locker)F
eqt(lock, mcrlrecord)Feqt(lock, ok)F
eqt(lock, pending)Feqt(lock, release)F
eqt(lock, request)Feqt(lock, resource)F
eqt(lock, tag)Feqt(lock, true)F
eqt(lock, undefined)Feqt(lock, pid(N2))F
eqt(lock, int(N2))Feqt(lock, cons(H2, T2))F
eqt(lock, tuple(H2, T2))Feqt(lock, tuplenil(H2))F
eqt(locker, nil)Feqt(locker, a)F
eqt(locker, excl)Feqt(locker, false)F
eqt(locker, lock)Feqt(locker, locker)T
eqt(locker, mcrlrecord)Feqt(locker, ok)F
eqt(locker, pending)Feqt(locker, release)F
eqt(locker, request)Feqt(locker, resource)F
eqt(locker, tag)Feqt(locker, true)F
eqt(locker, undefined)Feqt(locker, pid(N2))F
eqt(locker, int(N2))Feqt(locker, cons(H2, T2))F
eqt(locker, tuple(H2, T2))Feqt(locker, tuplenil(H2))F
eqt(mcrlrecord, nil)Feqt(mcrlrecord, a)F
eqt(mcrlrecord, excl)Feqt(mcrlrecord, false)F
eqt(mcrlrecord, lock)Feqt(mcrlrecord, locker)F
eqt(mcrlrecord, mcrlrecord)Teqt(mcrlrecord, ok)F
eqt(mcrlrecord, pending)Feqt(mcrlrecord, release)F
eqt(mcrlrecord, request)Feqt(mcrlrecord, resource)F
eqt(ok, resource)Feqt(ok, tag)F
eqt(ok, true)Feqt(ok, undefined)F
eqt(ok, pid(N2))Feqt(ok, int(N2))F
eqt(ok, cons(H2, T2))Feqt(ok, tuple(H2, T2))F
eqt(ok, tuplenil(H2))Feqt(pending, nil)F
eqt(pending, a)Feqt(pending, excl)F
eqt(pending, false)Feqt(pending, lock)F
eqt(pending, locker)Feqt(pending, mcrlrecord)F
eqt(pending, ok)Feqt(pending, pending)T
eqt(pending, release)Feqt(pending, request)F
eqt(pending, resource)Feqt(pending, tag)F
eqt(pending, true)Feqt(pending, undefined)F
eqt(pending, pid(N2))Feqt(pending, int(N2))F
eqt(pending, cons(H2, T2))Feqt(pending, tuple(H2, T2))F
eqt(pending, tuplenil(H2))Feqt(release, nil)F
eqt(release, a)Feqt(release, excl)F
eqt(release, false)Feqt(release, lock)F
eqt(release, locker)Feqt(release, mcrlrecord)F
eqt(release, ok)Feqt(request, mcrlrecord)F
eqt(request, ok)Feqt(request, pending)F
eqt(request, release)Feqt(request, request)T
eqt(request, resource)Feqt(request, tag)F
eqt(request, true)Feqt(request, undefined)F
eqt(request, pid(N2))Feqt(request, int(N2))F
eqt(request, cons(H2, T2))Feqt(request, tuple(H2, T2))F
eqt(request, tuplenil(H2))Feqt(resource, nil)F
eqt(resource, a)Feqt(resource, excl)F
eqt(resource, false)Feqt(resource, lock)F
eqt(resource, locker)Feqt(resource, mcrlrecord)F
eqt(resource, ok)Feqt(resource, pending)F
eqt(resource, release)Feqt(resource, request)F
eqt(resource, resource)Teqt(resource, tag)F
eqt(resource, true)Feqt(resource, undefined)F
eqt(resource, pid(N2))Feqt(resource, int(N2))F
eqt(resource, cons(H2, T2))Feqt(resource, tuple(H2, T2))F
eqt(resource, tuplenil(H2))Feqt(tag, nil)F
eqt(tag, a)Feqt(tag, excl)F
eqt(tag, false)Feqt(tag, lock)F
eqt(tag, locker)Feqt(tag, mcrlrecord)F
eqt(tag, ok)Feqt(tag, pending)F
eqt(tag, release)Feqt(tag, request)F
eqt(tag, resource)Feqt(tag, tag)T
eqt(tag, true)Feqt(tag, undefined)F
eqt(tag, pid(N2))Feqt(tag, int(N2))F
eqt(tag, cons(H2, T2))Feqt(tag, tuple(H2, T2))F
eqt(tag, tuplenil(H2))Feqt(true, nil)F
eqt(true, a)Feqt(true, excl)F
eqt(true, false)Feqt(true, lock)F
eqt(true, locker)Feqt(true, mcrlrecord)F
eqt(true, ok)Feqt(true, pending)F
eqt(true, release)Feqt(true, request)F
eqt(true, resource)Feqt(true, tag)F
eqt(true, true)Teqt(true, undefined)F
eqt(true, pid(N2))Feqt(true, int(N2))F
eqt(true, cons(H2, T2))Feqt(true, tuple(H2, T2))F
eqt(true, tuplenil(H2))Feqt(undefined, nil)F
eqt(undefined, a)Feqt(undefined, tuplenil(H2))F
eqt(pid(N1), nil)Feqt(pid(N1), a)F
eqt(pid(N1), excl)Feqt(pid(N1), false)F
eqt(pid(N1), lock)Feqt(pid(N1), locker)F
eqt(pid(N1), mcrlrecord)Feqt(pid(N1), ok)F
eqt(pid(N1), pending)Feqt(pid(N1), release)F
eqt(pid(N1), request)Feqt(pid(N1), resource)F
eqt(pid(N1), tag)Feqt(pid(N1), true)F
eqt(pid(N1), undefined)Feqt(pid(N1), pid(N2))eqt(N1, N2)
eqt(pid(N1), int(N2))Feqt(pid(N1), cons(H2, T2))F
eqt(pid(N1), tuple(H2, T2))Feqt(pid(N1), tuplenil(H2))F
eqt(int(N1), nil)Feqt(int(N1), a)F
eqt(int(N1), excl)Feqt(int(N1), false)F
eqt(int(N1), lock)Feqt(int(N1), locker)F
eqt(int(N1), mcrlrecord)Feqt(int(N1), ok)F
eqt(int(N1), pending)Feqt(int(N1), release)F
eqt(int(N1), request)Feqt(int(N1), resource)F
eqt(int(N1), tag)Feqt(int(N1), true)F
eqt(int(N1), undefined)Feqt(cons(H1, T1), resource)F
eqt(cons(H1, T1), tag)Feqt(cons(H1, T1), true)F
eqt(cons(H1, T1), undefined)Feqt(cons(H1, T1), pid(N2))F
eqt(cons(H1, T1), int(N2))Feqt(cons(H1, T1), cons(H2, T2))and(eqt(H1, H2), eqt(T1, T2))
eqt(cons(H1, T1), tuple(H2, T2))Feqt(cons(H1, T1), tuplenil(H2))F
eqt(tuple(H1, T1), nil)Feqt(tuple(H1, T1), a)F
eqt(tuple(H1, T1), excl)Feqt(tuple(H1, T1), false)F
eqt(tuple(H1, T1), lock)Feqt(tuple(H1, T1), locker)F
eqt(tuple(H1, T1), mcrlrecord)Feqt(tuple(H1, T1), ok)F
eqt(tuple(H1, T1), pending)Feqt(tuple(H1, T1), release)F
eqt(tuple(H1, T1), request)Feqt(tuple(H1, T1), resource)F
eqt(tuple(H1, T1), tag)Feqt(tuple(H1, T1), true)F
eqt(tuple(H1, T1), undefined)Feqt(tuple(H1, T1), pid(N2))F
eqt(tuple(H1, T1), int(N2))Feqt(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)Feqt(tuplenil(H1), a)F
eqt(tuplenil(H1), excl)Feqt(tuplenil(H1), false)F
eqt(tuplenil(H1), lock)Feqt(tuplenil(H1), locker)F
eqt(tuplenil(H1), mcrlrecord)Feqt(tuplenil(H1), ok)F
eqt(tuplenil(H1), pending)Feqt(tuplenil(H1), release)F
eqt(tuplenil(H1), request)Feqt(tuplenil(H1), resource)F
eqt(tuplenil(H1), tag)Feqt(tuplenil(H1), true)F
eqt(tuplenil(H1), undefined)Feqt(tuplenil(H1), pid(N2))F
eqt(tuplenil(H1), int(N2))Feqt(tuplenil(H1), cons(H2, T2))F
eqt(tuplenil(H1), tuple(H2, T2))Feqt(tuplenil(H1), tuplenil(H2))eqt(H1, H2)
element(int(s(0)), tuplenil(T1))T1element(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)Recordrecord_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)nillocker2_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)nillocker2_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)nillocker2_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)falselocker2_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))Feqs(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))S1tops(stack(E1, S1))E1
istops(E1, empty)Fistops(E1, stack(E2, S1))eqt(E1, E2)
eqc(nocalls, nocalls)Teqc(nocalls, calls(E2, S2, CS2))F
eqc(calls(E1, S1, CS1), nocalls)Feqc(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)

Original Signature

Termination of terms over the following signature is verified: tuplenil, record_new, tuple, tag, gen_tag, imp, locker2_map_promote_pending, pops, locker2_check_availables, mcrlrecord, pending, request, empty, false, ok, istops, locker2_add_pending, andt, element, append, case2, case1, tops, case0, push1, case6, case5, or, int, case4, record_extract, locker, case9, case8, locker2_map_add_pending, calls, eqc, and, not, 0, locker2_promote_pending, locker2_claim_lock, locker2_adduniq, stack, release, locker2_obtainables, F, locker2_remove_pending, push, T, gen_modtageq, record_update, if, undefined, excllock, eqt, record_updates, eqs, delete, cons, member, locker2_map_claim_lock, locker2_obtainable, pushs, a, lock, resource, locker2_release_lock, true, equal, pid, subtract, locker2_check_available, s, excl, nocalls, eq, nil

Strategy


There are no SCCs!

Problem 7: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

or(T, T)Tor(F, T)T
or(T, F)Tor(F, F)F
and(T, B)Band(B, T)B
and(F, B)Fand(B, F)F
imp(T, B)Bimp(F, B)T
not(T)Fnot(F)T
if(T, B1, B2)B1if(F, B1, B2)B2
eq(T, T)Teq(F, F)T
eq(T, F)Feq(F, T)F
eqt(nil, undefined)Feqt(nil, pid(N2))F
eqt(nil, int(N2))Feqt(nil, cons(H2, T2))F
eqt(nil, tuple(H2, T2))Feqt(nil, tuplenil(H2))F
eqt(a, nil)Feqt(a, a)T
eqt(a, excl)Feqt(a, false)F
eqt(a, lock)Feqt(a, locker)F
eqt(a, mcrlrecord)Feqt(a, ok)F
eqt(a, pending)Feqt(a, release)F
eqt(a, request)Feqt(a, resource)F
eqt(a, tag)Feqt(a, true)F
eqt(a, undefined)Feqt(a, pid(N2))F
eqt(a, int(N2))Feqt(a, cons(H2, T2))F
eqt(a, tuple(H2, T2))Feqt(a, tuplenil(H2))F
eqt(excl, nil)Feqt(excl, a)F
eqt(excl, excl)Teqt(excl, false)F
eqt(excl, lock)Feqt(excl, locker)F
eqt(excl, mcrlrecord)Feqt(excl, ok)F
eqt(excl, pending)Feqt(excl, release)F
eqt(excl, request)Feqt(excl, resource)F
eqt(excl, tag)Feqt(excl, true)F
eqt(excl, undefined)Feqt(excl, pid(N2))F
eqt(excl, eqt(false, int(N2)))Feqt(false, cons(H2, T2))F
eqt(false, tuple(H2, T2))Feqt(false, tuplenil(H2))F
eqt(lock, nil)Feqt(lock, a)F
eqt(lock, excl)Feqt(lock, false)F
eqt(lock, lock)Teqt(lock, locker)F
eqt(lock, mcrlrecord)Feqt(lock, ok)F
eqt(lock, pending)Feqt(lock, release)F
eqt(lock, request)Feqt(lock, resource)F
eqt(lock, tag)Feqt(lock, true)F
eqt(lock, undefined)Feqt(lock, pid(N2))F
eqt(lock, int(N2))Feqt(lock, cons(H2, T2))F
eqt(lock, tuple(H2, T2))Feqt(lock, tuplenil(H2))F
eqt(locker, nil)Feqt(locker, a)F
eqt(locker, excl)Feqt(locker, false)F
eqt(locker, lock)Feqt(locker, locker)T
eqt(locker, mcrlrecord)Feqt(locker, ok)F
eqt(locker, pending)Feqt(locker, release)F
eqt(locker, request)Feqt(locker, resource)F
eqt(locker, tag)Feqt(locker, true)F
eqt(locker, undefined)Feqt(locker, pid(N2))F
eqt(locker, int(N2))Feqt(locker, cons(H2, T2))F
eqt(locker, tuple(H2, T2))Feqt(locker, tuplenil(H2))F
eqt(mcrlrecord, nil)Feqt(mcrlrecord, a)F
eqt(mcrlrecord, excl)Feqt(mcrlrecord, false)F
eqt(mcrlrecord, lock)Feqt(mcrlrecord, locker)F
eqt(mcrlrecord, mcrlrecord)Teqt(mcrlrecord, ok)F
eqt(mcrlrecord, pending)Feqt(mcrlrecord, release)F
eqt(mcrlrecord, request)Feqt(mcrlrecord, resource)F
eqt(ok, resource)Feqt(ok, tag)F
eqt(ok, true)Feqt(ok, undefined)F
eqt(ok, pid(N2))Feqt(ok, int(N2))F
eqt(ok, cons(H2, T2))Feqt(ok, tuple(H2, T2))F
eqt(ok, tuplenil(H2))Feqt(pending, nil)F
eqt(pending, a)Feqt(pending, excl)F
eqt(pending, false)Feqt(pending, lock)F
eqt(pending, locker)Feqt(pending, mcrlrecord)F
eqt(pending, ok)Feqt(pending, pending)T
eqt(pending, release)Feqt(pending, request)F
eqt(pending, resource)Feqt(pending, tag)F
eqt(pending, true)Feqt(pending, undefined)F
eqt(pending, pid(N2))Feqt(pending, int(N2))F
eqt(pending, cons(H2, T2))Feqt(pending, tuple(H2, T2))F
eqt(pending, tuplenil(H2))Feqt(release, nil)F
eqt(release, a)Feqt(release, excl)F
eqt(release, false)Feqt(release, lock)F
eqt(release, locker)Feqt(release, mcrlrecord)F
eqt(release, ok)Feqt(request, mcrlrecord)F
eqt(request, ok)Feqt(request, pending)F
eqt(request, release)Feqt(request, request)T
eqt(request, resource)Feqt(request, tag)F
eqt(request, true)Feqt(request, undefined)F
eqt(request, pid(N2))Feqt(request, int(N2))F
eqt(request, cons(H2, T2))Feqt(request, tuple(H2, T2))F
eqt(request, tuplenil(H2))Feqt(resource, nil)F
eqt(resource, a)Feqt(resource, excl)F
eqt(resource, false)Feqt(resource, lock)F
eqt(resource, locker)Feqt(resource, mcrlrecord)F
eqt(resource, ok)Feqt(resource, pending)F
eqt(resource, release)Feqt(resource, request)F
eqt(resource, resource)Teqt(resource, tag)F
eqt(resource, true)Feqt(resource, undefined)F
eqt(resource, pid(N2))Feqt(resource, int(N2))F
eqt(resource, cons(H2, T2))Feqt(resource, tuple(H2, T2))F
eqt(resource, tuplenil(H2))Feqt(tag, nil)F
eqt(tag, a)Feqt(tag, excl)F
eqt(tag, false)Feqt(tag, lock)F
eqt(tag, locker)Feqt(tag, mcrlrecord)F
eqt(tag, ok)Feqt(tag, pending)F
eqt(tag, release)Feqt(tag, request)F
eqt(tag, resource)Feqt(tag, tag)T
eqt(tag, true)Feqt(tag, undefined)F
eqt(tag, pid(N2))Feqt(tag, int(N2))F
eqt(tag, cons(H2, T2))Feqt(tag, tuple(H2, T2))F
eqt(tag, tuplenil(H2))Feqt(true, nil)F
eqt(true, a)Feqt(true, excl)F
eqt(true, false)Feqt(true, lock)F
eqt(true, locker)Feqt(true, mcrlrecord)F
eqt(true, ok)Feqt(true, pending)F
eqt(true, release)Feqt(true, request)F
eqt(true, resource)Feqt(true, tag)F
eqt(true, true)Teqt(true, undefined)F
eqt(true, pid(N2))Feqt(true, int(N2))F
eqt(true, cons(H2, T2))Feqt(true, tuple(H2, T2))F
eqt(true, tuplenil(H2))Feqt(undefined, nil)F
eqt(undefined, a)Feqt(undefined, tuplenil(H2))F
eqt(pid(N1), nil)Feqt(pid(N1), a)F
eqt(pid(N1), excl)Feqt(pid(N1), false)F
eqt(pid(N1), lock)Feqt(pid(N1), locker)F
eqt(pid(N1), mcrlrecord)Feqt(pid(N1), ok)F
eqt(pid(N1), pending)Feqt(pid(N1), release)F
eqt(pid(N1), request)Feqt(pid(N1), resource)F
eqt(pid(N1), tag)Feqt(pid(N1), true)F
eqt(pid(N1), undefined)Feqt(pid(N1), pid(N2))eqt(N1, N2)
eqt(pid(N1), int(N2))Feqt(pid(N1), cons(H2, T2))F
eqt(pid(N1), tuple(H2, T2))Feqt(pid(N1), tuplenil(H2))F
eqt(int(N1), nil)Feqt(int(N1), a)F
eqt(int(N1), excl)Feqt(int(N1), false)F
eqt(int(N1), lock)Feqt(int(N1), locker)F
eqt(int(N1), mcrlrecord)Feqt(int(N1), ok)F
eqt(int(N1), pending)Feqt(int(N1), release)F
eqt(int(N1), request)Feqt(int(N1), resource)F
eqt(int(N1), tag)Feqt(int(N1), true)F
eqt(int(N1), undefined)Feqt(cons(H1, T1), resource)F
eqt(cons(H1, T1), tag)Feqt(cons(H1, T1), true)F
eqt(cons(H1, T1), undefined)Feqt(cons(H1, T1), pid(N2))F
eqt(cons(H1, T1), int(N2))Feqt(cons(H1, T1), cons(H2, T2))and(eqt(H1, H2), eqt(T1, T2))
eqt(cons(H1, T1), tuple(H2, T2))Feqt(cons(H1, T1), tuplenil(H2))F
eqt(tuple(H1, T1), nil)Feqt(tuple(H1, T1), a)F
eqt(tuple(H1, T1), excl)Feqt(tuple(H1, T1), false)F
eqt(tuple(H1, T1), lock)Feqt(tuple(H1, T1), locker)F
eqt(tuple(H1, T1), mcrlrecord)Feqt(tuple(H1, T1), ok)F
eqt(tuple(H1, T1), pending)Feqt(tuple(H1, T1), release)F
eqt(tuple(H1, T1), request)Feqt(tuple(H1, T1), resource)F
eqt(tuple(H1, T1), tag)Feqt(tuple(H1, T1), true)F
eqt(tuple(H1, T1), undefined)Feqt(tuple(H1, T1), pid(N2))F
eqt(tuple(H1, T1), int(N2))Feqt(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)Feqt(tuplenil(H1), a)F
eqt(tuplenil(H1), excl)Feqt(tuplenil(H1), false)F
eqt(tuplenil(H1), lock)Feqt(tuplenil(H1), locker)F
eqt(tuplenil(H1), mcrlrecord)Feqt(tuplenil(H1), ok)F
eqt(tuplenil(H1), pending)Feqt(tuplenil(H1), release)F
eqt(tuplenil(H1), request)Feqt(tuplenil(H1), resource)F
eqt(tuplenil(H1), tag)Feqt(tuplenil(H1), true)F
eqt(tuplenil(H1), undefined)Feqt(tuplenil(H1), pid(N2))F
eqt(tuplenil(H1), int(N2))Feqt(tuplenil(H1), cons(H2, T2))F
eqt(tuplenil(H1), tuple(H2, T2))Feqt(tuplenil(H1), tuplenil(H2))eqt(H1, H2)
element(int(s(0)), tuplenil(T1))T1element(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)Recordrecord_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)nillocker2_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)nillocker2_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)nillocker2_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)falselocker2_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))Feqs(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))S1tops(stack(E1, S1))E1
istops(E1, empty)Fistops(E1, stack(E2, S1))eqt(E1, E2)
eqc(nocalls, nocalls)Teqc(nocalls, calls(E2, S2, CS2))F
eqc(calls(E1, S1, CS1), nocalls)Feqc(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)

Original Signature

Termination of terms over the following signature is verified: tuplenil, record_new, tuple, tag, gen_tag, imp, locker2_map_promote_pending, pops, locker2_check_availables, mcrlrecord, pending, request, empty, false, ok, istops, locker2_add_pending, andt, case2, append, element, case1, case0, tops, push1, case6, case5, or, int, case4, record_extract, locker, case9, case8, locker2_map_add_pending, calls, eqc, and, not, 0, locker2_promote_pending, locker2_claim_lock, locker2_adduniq, stack, release, locker2_obtainables, F, locker2_remove_pending, push, T, gen_modtageq, record_update, undefined, if, record_updates, eqt, excllock, delete, eqs, cons, member, locker2_map_claim_lock, locker2_obtainable, a, pushs, resource, lock, true, locker2_release_lock, pid, equal, subtract, locker2_check_available, s, excl, nil, eq, nocalls

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 8: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

or(T, T)Tor(F, T)T
or(T, F)Tor(F, F)F
and(T, B)Band(B, T)B
and(F, B)Fand(B, F)F
imp(T, B)Bimp(F, B)T
not(T)Fnot(F)T
if(T, B1, B2)B1if(F, B1, B2)B2
eq(T, T)Teq(F, F)T
eq(T, F)Feq(F, T)F
eqt(nil, undefined)Feqt(nil, pid(N2))F
eqt(nil, int(N2))Feqt(nil, cons(H2, T2))F
eqt(nil, tuple(H2, T2))Feqt(nil, tuplenil(H2))F
eqt(a, nil)Feqt(a, a)T
eqt(a, excl)Feqt(a, false)F
eqt(a, lock)Feqt(a, locker)F
eqt(a, mcrlrecord)Feqt(a, ok)F
eqt(a, pending)Feqt(a, release)F
eqt(a, request)Feqt(a, resource)F
eqt(a, tag)Feqt(a, true)F
eqt(a, undefined)Feqt(a, pid(N2))F
eqt(a, int(N2))Feqt(a, cons(H2, T2))F
eqt(a, tuple(H2, T2))Feqt(a, tuplenil(H2))F
eqt(excl, nil)Feqt(excl, a)F
eqt(excl, excl)Teqt(excl, false)F
eqt(excl, lock)Feqt(excl, locker)F
eqt(excl, mcrlrecord)Feqt(excl, ok)F
eqt(excl, pending)Feqt(excl, release)F
eqt(excl, request)Feqt(excl, resource)F
eqt(excl, tag)Feqt(excl, true)F
eqt(excl, undefined)Feqt(excl, pid(N2))F
eqt(excl, eqt(false, int(N2)))Feqt(false, cons(H2, T2))F
eqt(false, tuple(H2, T2))Feqt(false, tuplenil(H2))F
eqt(lock, nil)Feqt(lock, a)F
eqt(lock, excl)Feqt(lock, false)F
eqt(lock, lock)Teqt(lock, locker)F
eqt(lock, mcrlrecord)Feqt(lock, ok)F
eqt(lock, pending)Feqt(lock, release)F
eqt(lock, request)Feqt(lock, resource)F
eqt(lock, tag)Feqt(lock, true)F
eqt(lock, undefined)Feqt(lock, pid(N2))F
eqt(lock, int(N2))Feqt(lock, cons(H2, T2))F
eqt(lock, tuple(H2, T2))Feqt(lock, tuplenil(H2))F
eqt(locker, nil)Feqt(locker, a)F
eqt(locker, excl)Feqt(locker, false)F
eqt(locker, lock)Feqt(locker, locker)T
eqt(locker, mcrlrecord)Feqt(locker, ok)F
eqt(locker, pending)Feqt(locker, release)F
eqt(locker, request)Feqt(locker, resource)F
eqt(locker, tag)Feqt(locker, true)F
eqt(locker, undefined)Feqt(locker, pid(N2))F
eqt(locker, int(N2))Feqt(locker, cons(H2, T2))F
eqt(locker, tuple(H2, T2))Feqt(locker, tuplenil(H2))F
eqt(mcrlrecord, nil)Feqt(mcrlrecord, a)F
eqt(mcrlrecord, excl)Feqt(mcrlrecord, false)F
eqt(mcrlrecord, lock)Feqt(mcrlrecord, locker)F
eqt(mcrlrecord, mcrlrecord)Teqt(mcrlrecord, ok)F
eqt(mcrlrecord, pending)Feqt(mcrlrecord, release)F
eqt(mcrlrecord, request)Feqt(mcrlrecord, resource)F
eqt(ok, resource)Feqt(ok, tag)F
eqt(ok, true)Feqt(ok, undefined)F
eqt(ok, pid(N2))Feqt(ok, int(N2))F
eqt(ok, cons(H2, T2))Feqt(ok, tuple(H2, T2))F
eqt(ok, tuplenil(H2))Feqt(pending, nil)F
eqt(pending, a)Feqt(pending, excl)F
eqt(pending, false)Feqt(pending, lock)F
eqt(pending, locker)Feqt(pending, mcrlrecord)F
eqt(pending, ok)Feqt(pending, pending)T
eqt(pending, release)Feqt(pending, request)F
eqt(pending, resource)Feqt(pending, tag)F
eqt(pending, true)Feqt(pending, undefined)F
eqt(pending, pid(N2))Feqt(pending, int(N2))F
eqt(pending, cons(H2, T2))Feqt(pending, tuple(H2, T2))F
eqt(pending, tuplenil(H2))Feqt(release, nil)F
eqt(release, a)Feqt(release, excl)F
eqt(release, false)Feqt(release, lock)F
eqt(release, locker)Feqt(release, mcrlrecord)F
eqt(release, ok)Feqt(request, mcrlrecord)F
eqt(request, ok)Feqt(request, pending)F
eqt(request, release)Feqt(request, request)T
eqt(request, resource)Feqt(request, tag)F
eqt(request, true)Feqt(request, undefined)F
eqt(request, pid(N2))Feqt(request, int(N2))F
eqt(request, cons(H2, T2))Feqt(request, tuple(H2, T2))F
eqt(request, tuplenil(H2))Feqt(resource, nil)F
eqt(resource, a)Feqt(resource, excl)F
eqt(resource, false)Feqt(resource, lock)F
eqt(resource, locker)Feqt(resource, mcrlrecord)F
eqt(resource, ok)Feqt(resource, pending)F
eqt(resource, release)Feqt(resource, request)F
eqt(resource, resource)Teqt(resource, tag)F
eqt(resource, true)Feqt(resource, undefined)F
eqt(resource, pid(N2))Feqt(resource, int(N2))F
eqt(resource, cons(H2, T2))Feqt(resource, tuple(H2, T2))F
eqt(resource, tuplenil(H2))Feqt(tag, nil)F
eqt(tag, a)Feqt(tag, excl)F
eqt(tag, false)Feqt(tag, lock)F
eqt(tag, locker)Feqt(tag, mcrlrecord)F
eqt(tag, ok)Feqt(tag, pending)F
eqt(tag, release)Feqt(tag, request)F
eqt(tag, resource)Feqt(tag, tag)T
eqt(tag, true)Feqt(tag, undefined)F
eqt(tag, pid(N2))Feqt(tag, int(N2))F
eqt(tag, cons(H2, T2))Feqt(tag, tuple(H2, T2))F
eqt(tag, tuplenil(H2))Feqt(true, nil)F
eqt(true, a)Feqt(true, excl)F
eqt(true, false)Feqt(true, lock)F
eqt(true, locker)Feqt(true, mcrlrecord)F
eqt(true, ok)Feqt(true, pending)F
eqt(true, release)Feqt(true, request)F
eqt(true, resource)Feqt(true, tag)F
eqt(true, true)Teqt(true, undefined)F
eqt(true, pid(N2))Feqt(true, int(N2))F
eqt(true, cons(H2, T2))Feqt(true, tuple(H2, T2))F
eqt(true, tuplenil(H2))Feqt(undefined, nil)F
eqt(undefined, a)Feqt(undefined, tuplenil(H2))F
eqt(pid(N1), nil)Feqt(pid(N1), a)F
eqt(pid(N1), excl)Feqt(pid(N1), false)F
eqt(pid(N1), lock)Feqt(pid(N1), locker)F
eqt(pid(N1), mcrlrecord)Feqt(pid(N1), ok)F
eqt(pid(N1), pending)Feqt(pid(N1), release)F
eqt(pid(N1), request)Feqt(pid(N1), resource)F
eqt(pid(N1), tag)Feqt(pid(N1), true)F
eqt(pid(N1), undefined)Feqt(pid(N1), pid(N2))eqt(N1, N2)
eqt(pid(N1), int(N2))Feqt(pid(N1), cons(H2, T2))F
eqt(pid(N1), tuple(H2, T2))Feqt(pid(N1), tuplenil(H2))F
eqt(int(N1), nil)Feqt(int(N1), a)F
eqt(int(N1), excl)Feqt(int(N1), false)F
eqt(int(N1), lock)Feqt(int(N1), locker)F
eqt(int(N1), mcrlrecord)Feqt(int(N1), ok)F
eqt(int(N1), pending)Feqt(int(N1), release)F
eqt(int(N1), request)Feqt(int(N1), resource)F
eqt(int(N1), tag)Feqt(int(N1), true)F
eqt(int(N1), undefined)Feqt(cons(H1, T1), resource)F
eqt(cons(H1, T1), tag)Feqt(cons(H1, T1), true)F
eqt(cons(H1, T1), undefined)Feqt(cons(H1, T1), pid(N2))F
eqt(cons(H1, T1), int(N2))Feqt(cons(H1, T1), cons(H2, T2))and(eqt(H1, H2), eqt(T1, T2))
eqt(cons(H1, T1), tuple(H2, T2))Feqt(cons(H1, T1), tuplenil(H2))F
eqt(tuple(H1, T1), nil)Feqt(tuple(H1, T1), a)F
eqt(tuple(H1, T1), excl)Feqt(tuple(H1, T1), false)F
eqt(tuple(H1, T1), lock)Feqt(tuple(H1, T1), locker)F
eqt(tuple(H1, T1), mcrlrecord)Feqt(tuple(H1, T1), ok)F
eqt(tuple(H1, T1), pending)Feqt(tuple(H1, T1), release)F
eqt(tuple(H1, T1), request)Feqt(tuple(H1, T1), resource)F
eqt(tuple(H1, T1), tag)Feqt(tuple(H1, T1), true)F
eqt(tuple(H1, T1), undefined)Feqt(tuple(H1, T1), pid(N2))F
eqt(tuple(H1, T1), int(N2))Feqt(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)Feqt(tuplenil(H1), a)F
eqt(tuplenil(H1), excl)Feqt(tuplenil(H1), false)F
eqt(tuplenil(H1), lock)Feqt(tuplenil(H1), locker)F
eqt(tuplenil(H1), mcrlrecord)Feqt(tuplenil(H1), ok)F
eqt(tuplenil(H1), pending)Feqt(tuplenil(H1), release)F
eqt(tuplenil(H1), request)Feqt(tuplenil(H1), resource)F
eqt(tuplenil(H1), tag)Feqt(tuplenil(H1), true)F
eqt(tuplenil(H1), undefined)Feqt(tuplenil(H1), pid(N2))F
eqt(tuplenil(H1), int(N2))Feqt(tuplenil(H1), cons(H2, T2))F
eqt(tuplenil(H1), tuple(H2, T2))Feqt(tuplenil(H1), tuplenil(H2))eqt(H1, H2)
element(int(s(0)), tuplenil(T1))T1element(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)Recordrecord_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)nillocker2_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)nillocker2_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)nillocker2_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)falselocker2_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))Feqs(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))S1tops(stack(E1, S1))E1
istops(E1, empty)Fistops(E1, stack(E2, S1))eqt(E1, E2)
eqc(nocalls, nocalls)Teqc(nocalls, calls(E2, S2, CS2))F
eqc(calls(E1, S1, CS1), nocalls)Feqc(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)

Original Signature

Termination of terms over the following signature is verified: tuplenil, record_new, tuple, tag, gen_tag, imp, locker2_map_promote_pending, pops, locker2_check_availables, mcrlrecord, pending, request, empty, false, ok, istops, locker2_add_pending, andt, case2, append, element, case1, case0, tops, push1, case6, case5, or, int, case4, record_extract, locker, case9, case8, locker2_map_add_pending, calls, eqc, and, not, 0, locker2_promote_pending, locker2_claim_lock, locker2_adduniq, stack, release, locker2_obtainables, F, locker2_remove_pending, push, T, gen_modtageq, record_update, undefined, if, record_updates, eqt, excllock, delete, eqs, cons, member, locker2_map_claim_lock, locker2_obtainable, a, pushs, resource, lock, true, locker2_release_lock, pid, equal, subtract, locker2_check_available, s, excl, nil, eq, nocalls

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 9: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

or(T, T)Tor(F, T)T
or(T, F)Tor(F, F)F
and(T, B)Band(B, T)B
and(F, B)Fand(B, F)F
imp(T, B)Bimp(F, B)T
not(T)Fnot(F)T
if(T, B1, B2)B1if(F, B1, B2)B2
eq(T, T)Teq(F, F)T
eq(T, F)Feq(F, T)F
eqt(nil, undefined)Feqt(nil, pid(N2))F
eqt(nil, int(N2))Feqt(nil, cons(H2, T2))F
eqt(nil, tuple(H2, T2))Feqt(nil, tuplenil(H2))F
eqt(a, nil)Feqt(a, a)T
eqt(a, excl)Feqt(a, false)F
eqt(a, lock)Feqt(a, locker)F
eqt(a, mcrlrecord)Feqt(a, ok)F
eqt(a, pending)Feqt(a, release)F
eqt(a, request)Feqt(a, resource)F
eqt(a, tag)Feqt(a, true)F
eqt(a, undefined)Feqt(a, pid(N2))F
eqt(a, int(N2))Feqt(a, cons(H2, T2))F
eqt(a, tuple(H2, T2))Feqt(a, tuplenil(H2))F
eqt(excl, nil)Feqt(excl, a)F
eqt(excl, excl)Teqt(excl, false)F
eqt(excl, lock)Feqt(excl, locker)F
eqt(excl, mcrlrecord)Feqt(excl, ok)F
eqt(excl, pending)Feqt(excl, release)F
eqt(excl, request)Feqt(excl, resource)F
eqt(excl, tag)Feqt(excl, true)F
eqt(excl, undefined)Feqt(excl, pid(N2))F
eqt(excl, eqt(false, int(N2)))Feqt(false, cons(H2, T2))F
eqt(false, tuple(H2, T2))Feqt(false, tuplenil(H2))F
eqt(lock, nil)Feqt(lock, a)F
eqt(lock, excl)Feqt(lock, false)F
eqt(lock, lock)Teqt(lock, locker)F
eqt(lock, mcrlrecord)Feqt(lock, ok)F
eqt(lock, pending)Feqt(lock, release)F
eqt(lock, request)Feqt(lock, resource)F
eqt(lock, tag)Feqt(lock, true)F
eqt(lock, undefined)Feqt(lock, pid(N2))F
eqt(lock, int(N2))Feqt(lock, cons(H2, T2))F
eqt(lock, tuple(H2, T2))Feqt(lock, tuplenil(H2))F
eqt(locker, nil)Feqt(locker, a)F
eqt(locker, excl)Feqt(locker, false)F
eqt(locker, lock)Feqt(locker, locker)T
eqt(locker, mcrlrecord)Feqt(locker, ok)F
eqt(locker, pending)Feqt(locker, release)F
eqt(locker, request)Feqt(locker, resource)F
eqt(locker, tag)Feqt(locker, true)F
eqt(locker, undefined)Feqt(locker, pid(N2))F
eqt(locker, int(N2))Feqt(locker, cons(H2, T2))F
eqt(locker, tuple(H2, T2))Feqt(locker, tuplenil(H2))F
eqt(mcrlrecord, nil)Feqt(mcrlrecord, a)F
eqt(mcrlrecord, excl)Feqt(mcrlrecord, false)F
eqt(mcrlrecord, lock)Feqt(mcrlrecord, locker)F
eqt(mcrlrecord, mcrlrecord)Teqt(mcrlrecord, ok)F
eqt(mcrlrecord, pending)Feqt(mcrlrecord, release)F
eqt(mcrlrecord, request)Feqt(mcrlrecord, resource)F
eqt(ok, resource)Feqt(ok, tag)F
eqt(ok, true)Feqt(ok, undefined)F
eqt(ok, pid(N2))Feqt(ok, int(N2))F
eqt(ok, cons(H2, T2))Feqt(ok, tuple(H2, T2))F
eqt(ok, tuplenil(H2))Feqt(pending, nil)F
eqt(pending, a)Feqt(pending, excl)F
eqt(pending, false)Feqt(pending, lock)F
eqt(pending, locker)Feqt(pending, mcrlrecord)F
eqt(pending, ok)Feqt(pending, pending)T
eqt(pending, release)Feqt(pending, request)F
eqt(pending, resource)Feqt(pending, tag)F
eqt(pending, true)Feqt(pending, undefined)F
eqt(pending, pid(N2))Feqt(pending, int(N2))F
eqt(pending, cons(H2, T2))Feqt(pending, tuple(H2, T2))F
eqt(pending, tuplenil(H2))Feqt(release, nil)F
eqt(release, a)Feqt(release, excl)F
eqt(release, false)Feqt(release, lock)F
eqt(release, locker)Feqt(release, mcrlrecord)F
eqt(release, ok)Feqt(request, mcrlrecord)F
eqt(request, ok)Feqt(request, pending)F
eqt(request, release)Feqt(request, request)T
eqt(request, resource)Feqt(request, tag)F
eqt(request, true)Feqt(request, undefined)F
eqt(request, pid(N2))Feqt(request, int(N2))F
eqt(request, cons(H2, T2))Feqt(request, tuple(H2, T2))F
eqt(request, tuplenil(H2))Feqt(resource, nil)F
eqt(resource, a)Feqt(resource, excl)F
eqt(resource, false)Feqt(resource, lock)F
eqt(resource, locker)Feqt(resource, mcrlrecord)F
eqt(resource, ok)Feqt(resource, pending)F
eqt(resource, release)Feqt(resource, request)F
eqt(resource, resource)Teqt(resource, tag)F
eqt(resource, true)Feqt(resource, undefined)F
eqt(resource, pid(N2))Feqt(resource, int(N2))F
eqt(resource, cons(H2, T2))Feqt(resource, tuple(H2, T2))F
eqt(resource, tuplenil(H2))Feqt(tag, nil)F
eqt(tag, a)Feqt(tag, excl)F
eqt(tag, false)Feqt(tag, lock)F
eqt(tag, locker)Feqt(tag, mcrlrecord)F
eqt(tag, ok)Feqt(tag, pending)F
eqt(tag, release)Feqt(tag, request)F
eqt(tag, resource)Feqt(tag, tag)T
eqt(tag, true)Feqt(tag, undefined)F
eqt(tag, pid(N2))Feqt(tag, int(N2))F
eqt(tag, cons(H2, T2))Feqt(tag, tuple(H2, T2))F
eqt(tag, tuplenil(H2))Feqt(true, nil)F
eqt(true, a)Feqt(true, excl)F
eqt(true, false)Feqt(true, lock)F
eqt(true, locker)Feqt(true, mcrlrecord)F
eqt(true, ok)Feqt(true, pending)F
eqt(true, release)Feqt(true, request)F
eqt(true, resource)Feqt(true, tag)F
eqt(true, true)Teqt(true, undefined)F
eqt(true, pid(N2))Feqt(true, int(N2))F
eqt(true, cons(H2, T2))Feqt(true, tuple(H2, T2))F
eqt(true, tuplenil(H2))Feqt(undefined, nil)F
eqt(undefined, a)Feqt(undefined, tuplenil(H2))F
eqt(pid(N1), nil)Feqt(pid(N1), a)F
eqt(pid(N1), excl)Feqt(pid(N1), false)F
eqt(pid(N1), lock)Feqt(pid(N1), locker)F
eqt(pid(N1), mcrlrecord)Feqt(pid(N1), ok)F
eqt(pid(N1), pending)Feqt(pid(N1), release)F
eqt(pid(N1), request)Feqt(pid(N1), resource)F
eqt(pid(N1), tag)Feqt(pid(N1), true)F
eqt(pid(N1), undefined)Feqt(pid(N1), pid(N2))eqt(N1, N2)
eqt(pid(N1), int(N2))Feqt(pid(N1), cons(H2, T2))F
eqt(pid(N1), tuple(H2, T2))Feqt(pid(N1), tuplenil(H2))F
eqt(int(N1), nil)Feqt(int(N1), a)F
eqt(int(N1), excl)Feqt(int(N1), false)F
eqt(int(N1), lock)Feqt(int(N1), locker)F
eqt(int(N1), mcrlrecord)Feqt(int(N1), ok)F
eqt(int(N1), pending)Feqt(int(N1), release)F
eqt(int(N1), request)Feqt(int(N1), resource)F
eqt(int(N1), tag)Feqt(int(N1), true)F
eqt(int(N1), undefined)Feqt(cons(H1, T1), resource)F
eqt(cons(H1, T1), tag)Feqt(cons(H1, T1), true)F
eqt(cons(H1, T1), undefined)Feqt(cons(H1, T1), pid(N2))F
eqt(cons(H1, T1), int(N2))Feqt(cons(H1, T1), cons(H2, T2))and(eqt(H1, H2), eqt(T1, T2))
eqt(cons(H1, T1), tuple(H2, T2))Feqt(cons(H1, T1), tuplenil(H2))F
eqt(tuple(H1, T1), nil)Feqt(tuple(H1, T1), a)F
eqt(tuple(H1, T1), excl)Feqt(tuple(H1, T1), false)F
eqt(tuple(H1, T1), lock)Feqt(tuple(H1, T1), locker)F
eqt(tuple(H1, T1), mcrlrecord)Feqt(tuple(H1, T1), ok)F
eqt(tuple(H1, T1), pending)Feqt(tuple(H1, T1), release)F
eqt(tuple(H1, T1), request)Feqt(tuple(H1, T1), resource)F
eqt(tuple(H1, T1), tag)Feqt(tuple(H1, T1), true)F
eqt(tuple(H1, T1), undefined)Feqt(tuple(H1, T1), pid(N2))F
eqt(tuple(H1, T1), int(N2))Feqt(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)Feqt(tuplenil(H1), a)F
eqt(tuplenil(H1), excl)Feqt(tuplenil(H1), false)F
eqt(tuplenil(H1), lock)Feqt(tuplenil(H1), locker)F
eqt(tuplenil(H1), mcrlrecord)Feqt(tuplenil(H1), ok)F
eqt(tuplenil(H1), pending)Feqt(tuplenil(H1), release)F
eqt(tuplenil(H1), request)Feqt(tuplenil(H1), resource)F
eqt(tuplenil(H1), tag)Feqt(tuplenil(H1), true)F
eqt(tuplenil(H1), undefined)Feqt(tuplenil(H1), pid(N2))F
eqt(tuplenil(H1), int(N2))Feqt(tuplenil(H1), cons(H2, T2))F
eqt(tuplenil(H1), tuple(H2, T2))Feqt(tuplenil(H1), tuplenil(H2))eqt(H1, H2)
element(int(s(0)), tuplenil(T1))T1element(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)Recordrecord_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)nillocker2_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)nillocker2_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)nillocker2_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)falselocker2_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))Feqs(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))S1tops(stack(E1, S1))E1
istops(E1, empty)Fistops(E1, stack(E2, S1))eqt(E1, E2)
eqc(nocalls, nocalls)Teqc(nocalls, calls(E2, S2, CS2))F
eqc(calls(E1, S1, CS1), nocalls)Feqc(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)

Original Signature

Termination of terms over the following signature is verified: tuplenil, record_new, tuple, tag, gen_tag, imp, locker2_map_promote_pending, pops, locker2_check_availables, mcrlrecord, pending, request, empty, false, ok, istops, locker2_add_pending, andt, case2, append, element, case1, case0, tops, push1, case6, case5, or, int, case4, record_extract, locker, case9, case8, locker2_map_add_pending, calls, eqc, and, not, 0, locker2_promote_pending, locker2_claim_lock, locker2_adduniq, stack, release, locker2_obtainables, F, locker2_remove_pending, push, T, gen_modtageq, record_update, undefined, if, record_updates, eqt, excllock, delete, eqs, cons, member, locker2_map_claim_lock, locker2_obtainable, a, pushs, resource, lock, true, locker2_release_lock, pid, equal, subtract, locker2_check_available, s, excl, nil, eq, nocalls

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 10: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

eqt#(pid(N1), pid(N2))eqt#(N1, N2)eqt#(tuple(H1, T1), tuple(H2, T2))eqt#(T1, T2)
eqt#(tuple(H1, T1), tuple(H2, T2))eqt#(H1, H2)eqt#(cons(H1, T1), cons(H2, T2))eqt#(H1, H2)
eqt#(tuplenil(H1), tuplenil(H2))eqt#(H1, H2)eqt#(cons(H1, T1), cons(H2, T2))eqt#(T1, T2)

Rewrite Rules

or(T, T)Tor(F, T)T
or(T, F)Tor(F, F)F
and(T, B)Band(B, T)B
and(F, B)Fand(B, F)F
imp(T, B)Bimp(F, B)T
not(T)Fnot(F)T
if(T, B1, B2)B1if(F, B1, B2)B2
eq(T, T)Teq(F, F)T
eq(T, F)Feq(F, T)F
eqt(nil, undefined)Feqt(nil, pid(N2))F
eqt(nil, int(N2))Feqt(nil, cons(H2, T2))F
eqt(nil, tuple(H2, T2))Feqt(nil, tuplenil(H2))F
eqt(a, nil)Feqt(a, a)T
eqt(a, excl)Feqt(a, false)F
eqt(a, lock)Feqt(a, locker)F
eqt(a, mcrlrecord)Feqt(a, ok)F
eqt(a, pending)Feqt(a, release)F
eqt(a, request)Feqt(a, resource)F
eqt(a, tag)Feqt(a, true)F
eqt(a, undefined)Feqt(a, pid(N2))F
eqt(a, int(N2))Feqt(a, cons(H2, T2))F
eqt(a, tuple(H2, T2))Feqt(a, tuplenil(H2))F
eqt(excl, nil)Feqt(excl, a)F
eqt(excl, excl)Teqt(excl, false)F
eqt(excl, lock)Feqt(excl, locker)F
eqt(excl, mcrlrecord)Feqt(excl, ok)F
eqt(excl, pending)Feqt(excl, release)F
eqt(excl, request)Feqt(excl, resource)F
eqt(excl, tag)Feqt(excl, true)F
eqt(excl, undefined)Feqt(excl, pid(N2))F
eqt(excl, eqt(false, int(N2)))Feqt(false, cons(H2, T2))F
eqt(false, tuple(H2, T2))Feqt(false, tuplenil(H2))F
eqt(lock, nil)Feqt(lock, a)F
eqt(lock, excl)Feqt(lock, false)F
eqt(lock, lock)Teqt(lock, locker)F
eqt(lock, mcrlrecord)Feqt(lock, ok)F
eqt(lock, pending)Feqt(lock, release)F
eqt(lock, request)Feqt(lock, resource)F
eqt(lock, tag)Feqt(lock, true)F
eqt(lock, undefined)Feqt(lock, pid(N2))F
eqt(lock, int(N2))Feqt(lock, cons(H2, T2))F
eqt(lock, tuple(H2, T2))Feqt(lock, tuplenil(H2))F
eqt(locker, nil)Feqt(locker, a)F
eqt(locker, excl)Feqt(locker, false)F
eqt(locker, lock)Feqt(locker, locker)T
eqt(locker, mcrlrecord)Feqt(locker, ok)F
eqt(locker, pending)Feqt(locker, release)F
eqt(locker, request)Feqt(locker, resource)F
eqt(locker, tag)Feqt(locker, true)F
eqt(locker, undefined)Feqt(locker, pid(N2))F
eqt(locker, int(N2))Feqt(locker, cons(H2, T2))F
eqt(locker, tuple(H2, T2))Feqt(locker, tuplenil(H2))F
eqt(mcrlrecord, nil)Feqt(mcrlrecord, a)F
eqt(mcrlrecord, excl)Feqt(mcrlrecord, false)F
eqt(mcrlrecord, lock)Feqt(mcrlrecord, locker)F
eqt(mcrlrecord, mcrlrecord)Teqt(mcrlrecord, ok)F
eqt(mcrlrecord, pending)Feqt(mcrlrecord, release)F
eqt(mcrlrecord, request)Feqt(mcrlrecord, resource)F
eqt(ok, resource)Feqt(ok, tag)F
eqt(ok, true)Feqt(ok, undefined)F
eqt(ok, pid(N2))Feqt(ok, int(N2))F
eqt(ok, cons(H2, T2))Feqt(ok, tuple(H2, T2))F
eqt(ok, tuplenil(H2))Feqt(pending, nil)F
eqt(pending, a)Feqt(pending, excl)F
eqt(pending, false)Feqt(pending, lock)F
eqt(pending, locker)Feqt(pending, mcrlrecord)F
eqt(pending, ok)Feqt(pending, pending)T
eqt(pending, release)Feqt(pending, request)F
eqt(pending, resource)Feqt(pending, tag)F
eqt(pending, true)Feqt(pending, undefined)F
eqt(pending, pid(N2))Feqt(pending, int(N2))F
eqt(pending, cons(H2, T2))Feqt(pending, tuple(H2, T2))F
eqt(pending, tuplenil(H2))Feqt(release, nil)F
eqt(release, a)Feqt(release, excl)F
eqt(release, false)Feqt(release, lock)F
eqt(release, locker)Feqt(release, mcrlrecord)F
eqt(release, ok)Feqt(request, mcrlrecord)F
eqt(request, ok)Feqt(request, pending)F
eqt(request, release)Feqt(request, request)T
eqt(request, resource)Feqt(request, tag)F
eqt(request, true)Feqt(request, undefined)F
eqt(request, pid(N2))Feqt(request, int(N2))F
eqt(request, cons(H2, T2))Feqt(request, tuple(H2, T2))F
eqt(request, tuplenil(H2))Feqt(resource, nil)F
eqt(resource, a)Feqt(resource, excl)F
eqt(resource, false)Feqt(resource, lock)F
eqt(resource, locker)Feqt(resource, mcrlrecord)F
eqt(resource, ok)Feqt(resource, pending)F
eqt(resource, release)Feqt(resource, request)F
eqt(resource, resource)Teqt(resource, tag)F
eqt(resource, true)Feqt(resource, undefined)F
eqt(resource, pid(N2))Feqt(resource, int(N2))F
eqt(resource, cons(H2, T2))Feqt(resource, tuple(H2, T2))F
eqt(resource, tuplenil(H2))Feqt(tag, nil)F
eqt(tag, a)Feqt(tag, excl)F
eqt(tag, false)Feqt(tag, lock)F
eqt(tag, locker)Feqt(tag, mcrlrecord)F
eqt(tag, ok)Feqt(tag, pending)F
eqt(tag, release)Feqt(tag, request)F
eqt(tag, resource)Feqt(tag, tag)T
eqt(tag, true)Feqt(tag, undefined)F
eqt(tag, pid(N2))Feqt(tag, int(N2))F
eqt(tag, cons(H2, T2))Feqt(tag, tuple(H2, T2))F
eqt(tag, tuplenil(H2))Feqt(true, nil)F
eqt(true, a)Feqt(true, excl)F
eqt(true, false)Feqt(true, lock)F
eqt(true, locker)Feqt(true, mcrlrecord)F
eqt(true, ok)Feqt(true, pending)F
eqt(true, release)Feqt(true, request)F
eqt(true, resource)Feqt(true, tag)F
eqt(true, true)Teqt(true, undefined)F
eqt(true, pid(N2))Feqt(true, int(N2))F
eqt(true, cons(H2, T2))Feqt(true, tuple(H2, T2))F
eqt(true, tuplenil(H2))Feqt(undefined, nil)F
eqt(undefined, a)Feqt(undefined, tuplenil(H2))F
eqt(pid(N1), nil)Feqt(pid(N1), a)F
eqt(pid(N1), excl)Feqt(pid(N1), false)F
eqt(pid(N1), lock)Feqt(pid(N1), locker)F
eqt(pid(N1), mcrlrecord)Feqt(pid(N1), ok)F
eqt(pid(N1), pending)Feqt(pid(N1), release)F
eqt(pid(N1), request)Feqt(pid(N1), resource)F
eqt(pid(N1), tag)Feqt(pid(N1), true)F
eqt(pid(N1), undefined)Feqt(pid(N1), pid(N2))eqt(N1, N2)
eqt(pid(N1), int(N2))Feqt(pid(N1), cons(H2, T2))F
eqt(pid(N1), tuple(H2, T2))Feqt(pid(N1), tuplenil(H2))F
eqt(int(N1), nil)Feqt(int(N1), a)F
eqt(int(N1), excl)Feqt(int(N1), false)F
eqt(int(N1), lock)Feqt(int(N1), locker)F
eqt(int(N1), mcrlrecord)Feqt(int(N1), ok)F
eqt(int(N1), pending)Feqt(int(N1), release)F
eqt(int(N1), request)Feqt(int(N1), resource)F
eqt(int(N1), tag)Feqt(int(N1), true)F
eqt(int(N1), undefined)Feqt(cons(H1, T1), resource)F
eqt(cons(H1, T1), tag)Feqt(cons(H1, T1), true)F
eqt(cons(H1, T1), undefined)Feqt(cons(H1, T1), pid(N2))F
eqt(cons(H1, T1), int(N2))Feqt(cons(H1, T1), cons(H2, T2))and(eqt(H1, H2), eqt(T1, T2))
eqt(cons(H1, T1), tuple(H2, T2))Feqt(cons(H1, T1), tuplenil(H2))F
eqt(tuple(H1, T1), nil)Feqt(tuple(H1, T1), a)F
eqt(tuple(H1, T1), excl)Feqt(tuple(H1, T1), false)F
eqt(tuple(H1, T1), lock)Feqt(tuple(H1, T1), locker)F
eqt(tuple(H1, T1), mcrlrecord)Feqt(tuple(H1, T1), ok)F
eqt(tuple(H1, T1), pending)Feqt(tuple(H1, T1), release)F
eqt(tuple(H1, T1), request)Feqt(tuple(H1, T1), resource)F
eqt(tuple(H1, T1), tag)Feqt(tuple(H1, T1), true)F
eqt(tuple(H1, T1), undefined)Feqt(tuple(H1, T1), pid(N2))F
eqt(tuple(H1, T1), int(N2))Feqt(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)Feqt(tuplenil(H1), a)F
eqt(tuplenil(H1), excl)Feqt(tuplenil(H1), false)F
eqt(tuplenil(H1), lock)Feqt(tuplenil(H1), locker)F
eqt(tuplenil(H1), mcrlrecord)Feqt(tuplenil(H1), ok)F
eqt(tuplenil(H1), pending)Feqt(tuplenil(H1), release)F
eqt(tuplenil(H1), request)Feqt(tuplenil(H1), resource)F
eqt(tuplenil(H1), tag)Feqt(tuplenil(H1), true)F
eqt(tuplenil(H1), undefined)Feqt(tuplenil(H1), pid(N2))F
eqt(tuplenil(H1), int(N2))Feqt(tuplenil(H1), cons(H2, T2))F
eqt(tuplenil(H1), tuple(H2, T2))Feqt(tuplenil(H1), tuplenil(H2))eqt(H1, H2)
element(int(s(0)), tuplenil(T1))T1element(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)Recordrecord_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)nillocker2_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)nillocker2_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)nillocker2_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)falselocker2_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))Feqs(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))S1tops(stack(E1, S1))E1
istops(E1, empty)Fistops(E1, stack(E2, S1))eqt(E1, E2)
eqc(nocalls, nocalls)Teqc(nocalls, calls(E2, S2, CS2))F
eqc(calls(E1, S1, CS1), nocalls)Feqc(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)

Original Signature

Termination of terms over the following signature is verified: tuplenil, record_new, tuple, tag, gen_tag, imp, locker2_map_promote_pending, pops, locker2_check_availables, mcrlrecord, pending, request, empty, false, ok, istops, locker2_add_pending, andt, case2, append, element, case1, case0, tops, push1, case6, case5, or, int, case4, record_extract, locker, case9, case8, locker2_map_add_pending, calls, eqc, and, not, 0, locker2_promote_pending, locker2_claim_lock, locker2_adduniq, stack, release, locker2_obtainables, F, locker2_remove_pending, push, T, gen_modtageq, record_update, undefined, if, record_updates, eqt, excllock, delete, eqs, cons, member, locker2_map_claim_lock, locker2_obtainable, a, pushs, resource, lock, true, locker2_release_lock, pid, equal, subtract, locker2_check_available, s, excl, nil, eq, nocalls

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

eqt#(pid(N1), pid(N2))eqt#(N1, N2)eqt#(tuple(H1, T1), tuple(H2, T2))eqt#(T1, T2)
eqt#(cons(H1, T1), cons(H2, T2))eqt#(H1, H2)eqt#(tuple(H1, T1), tuple(H2, T2))eqt#(H1, H2)
eqt#(tuplenil(H1), tuplenil(H2))eqt#(H1, H2)eqt#(cons(H1, T1), cons(H2, T2))eqt#(T1, T2)

Problem 11: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

or(T, T)Tor(F, T)T
or(T, F)Tor(F, F)F
and(T, B)Band(B, T)B
and(F, B)Fand(B, F)F
imp(T, B)Bimp(F, B)T
not(T)Fnot(F)T
if(T, B1, B2)B1if(F, B1, B2)B2
eq(T, T)Teq(F, F)T
eq(T, F)Feq(F, T)F
eqt(nil, undefined)Feqt(nil, pid(N2))F
eqt(nil, int(N2))Feqt(nil, cons(H2, T2))F
eqt(nil, tuple(H2, T2))Feqt(nil, tuplenil(H2))F
eqt(a, nil)Feqt(a, a)T
eqt(a, excl)Feqt(a, false)F
eqt(a, lock)Feqt(a, locker)F
eqt(a, mcrlrecord)Feqt(a, ok)F
eqt(a, pending)Feqt(a, release)F
eqt(a, request)Feqt(a, resource)F
eqt(a, tag)Feqt(a, true)F
eqt(a, undefined)Feqt(a, pid(N2))F
eqt(a, int(N2))Feqt(a, cons(H2, T2))F
eqt(a, tuple(H2, T2))Feqt(a, tuplenil(H2))F
eqt(excl, nil)Feqt(excl, a)F
eqt(excl, excl)Teqt(excl, false)F
eqt(excl, lock)Feqt(excl, locker)F
eqt(excl, mcrlrecord)Feqt(excl, ok)F
eqt(excl, pending)Feqt(excl, release)F
eqt(excl, request)Feqt(excl, resource)F
eqt(excl, tag)Feqt(excl, true)F
eqt(excl, undefined)Feqt(excl, pid(N2))F
eqt(excl, eqt(false, int(N2)))Feqt(false, cons(H2, T2))F
eqt(false, tuple(H2, T2))Feqt(false, tuplenil(H2))F
eqt(lock, nil)Feqt(lock, a)F
eqt(lock, excl)Feqt(lock, false)F
eqt(lock, lock)Teqt(lock, locker)F
eqt(lock, mcrlrecord)Feqt(lock, ok)F
eqt(lock, pending)Feqt(lock, release)F
eqt(lock, request)Feqt(lock, resource)F
eqt(lock, tag)Feqt(lock, true)F
eqt(lock, undefined)Feqt(lock, pid(N2))F
eqt(lock, int(N2))Feqt(lock, cons(H2, T2))F
eqt(lock, tuple(H2, T2))Feqt(lock, tuplenil(H2))F
eqt(locker, nil)Feqt(locker, a)F
eqt(locker, excl)Feqt(locker, false)F
eqt(locker, lock)Feqt(locker, locker)T
eqt(locker, mcrlrecord)Feqt(locker, ok)F
eqt(locker, pending)Feqt(locker, release)F
eqt(locker, request)Feqt(locker, resource)F
eqt(locker, tag)Feqt(locker, true)F
eqt(locker, undefined)Feqt(locker, pid(N2))F
eqt(locker, int(N2))Feqt(locker, cons(H2, T2))F
eqt(locker, tuple(H2, T2))Feqt(locker, tuplenil(H2))F
eqt(mcrlrecord, nil)Feqt(mcrlrecord, a)F
eqt(mcrlrecord, excl)Feqt(mcrlrecord, false)F
eqt(mcrlrecord, lock)Feqt(mcrlrecord, locker)F
eqt(mcrlrecord, mcrlrecord)Teqt(mcrlrecord, ok)F
eqt(mcrlrecord, pending)Feqt(mcrlrecord, release)F
eqt(mcrlrecord, request)Feqt(mcrlrecord, resource)F
eqt(ok, resource)Feqt(ok, tag)F
eqt(ok, true)Feqt(ok, undefined)F
eqt(ok, pid(N2))Feqt(ok, int(N2))F
eqt(ok, cons(H2, T2))Feqt(ok, tuple(H2, T2))F
eqt(ok, tuplenil(H2))Feqt(pending, nil)F
eqt(pending, a)Feqt(pending, excl)F
eqt(pending, false)Feqt(pending, lock)F
eqt(pending, locker)Feqt(pending, mcrlrecord)F
eqt(pending, ok)Feqt(pending, pending)T
eqt(pending, release)Feqt(pending, request)F
eqt(pending, resource)Feqt(pending, tag)F
eqt(pending, true)Feqt(pending, undefined)F
eqt(pending, pid(N2))Feqt(pending, int(N2))F
eqt(pending, cons(H2, T2))Feqt(pending, tuple(H2, T2))F
eqt(pending, tuplenil(H2))Feqt(release, nil)F
eqt(release, a)Feqt(release, excl)F
eqt(release, false)Feqt(release, lock)F
eqt(release, locker)Feqt(release, mcrlrecord)F
eqt(release, ok)Feqt(request, mcrlrecord)F
eqt(request, ok)Feqt(request, pending)F
eqt(request, release)Feqt(request, request)T
eqt(request, resource)Feqt(request, tag)F
eqt(request, true)Feqt(request, undefined)F
eqt(request, pid(N2))Feqt(request, int(N2))F
eqt(request, cons(H2, T2))Feqt(request, tuple(H2, T2))F
eqt(request, tuplenil(H2))Feqt(resource, nil)F
eqt(resource, a)Feqt(resource, excl)F
eqt(resource, false)Feqt(resource, lock)F
eqt(resource, locker)Feqt(resource, mcrlrecord)F
eqt(resource, ok)Feqt(resource, pending)F
eqt(resource, release)Feqt(resource, request)F
eqt(resource, resource)Teqt(resource, tag)F
eqt(resource, true)Feqt(resource, undefined)F
eqt(resource, pid(N2))Feqt(resource, int(N2))F
eqt(resource, cons(H2, T2))Feqt(resource, tuple(H2, T2))F
eqt(resource, tuplenil(H2))Feqt(tag, nil)F
eqt(tag, a)Feqt(tag, excl)F
eqt(tag, false)Feqt(tag, lock)F
eqt(tag, locker)Feqt(tag, mcrlrecord)F
eqt(tag, ok)Feqt(tag, pending)F
eqt(tag, release)Feqt(tag, request)F
eqt(tag, resource)Feqt(tag, tag)T
eqt(tag, true)Feqt(tag, undefined)F
eqt(tag, pid(N2))Feqt(tag, int(N2))F
eqt(tag, cons(H2, T2))Feqt(tag, tuple(H2, T2))F
eqt(tag, tuplenil(H2))Feqt(true, nil)F
eqt(true, a)Feqt(true, excl)F
eqt(true, false)Feqt(true, lock)F
eqt(true, locker)Feqt(true, mcrlrecord)F
eqt(true, ok)Feqt(true, pending)F
eqt(true, release)Feqt(true, request)F
eqt(true, resource)Feqt(true, tag)F
eqt(true, true)Teqt(true, undefined)F
eqt(true, pid(N2))Feqt(true, int(N2))F
eqt(true, cons(H2, T2))Feqt(true, tuple(H2, T2))F
eqt(true, tuplenil(H2))Feqt(undefined, nil)F
eqt(undefined, a)Feqt(undefined, tuplenil(H2))F
eqt(pid(N1), nil)Feqt(pid(N1), a)F
eqt(pid(N1), excl)Feqt(pid(N1), false)F
eqt(pid(N1), lock)Feqt(pid(N1), locker)F
eqt(pid(N1), mcrlrecord)Feqt(pid(N1), ok)F
eqt(pid(N1), pending)Feqt(pid(N1), release)F
eqt(pid(N1), request)Feqt(pid(N1), resource)F
eqt(pid(N1), tag)Feqt(pid(N1), true)F
eqt(pid(N1), undefined)Feqt(pid(N1), pid(N2))eqt(N1, N2)
eqt(pid(N1), int(N2))Feqt(pid(N1), cons(H2, T2))F
eqt(pid(N1), tuple(H2, T2))Feqt(pid(N1), tuplenil(H2))F
eqt(int(N1), nil)Feqt(int(N1), a)F
eqt(int(N1), excl)Feqt(int(N1), false)F
eqt(int(N1), lock)Feqt(int(N1), locker)F
eqt(int(N1), mcrlrecord)Feqt(int(N1), ok)F
eqt(int(N1), pending)Feqt(int(N1), release)F
eqt(int(N1), request)Feqt(int(N1), resource)F
eqt(int(N1), tag)Feqt(int(N1), true)F
eqt(int(N1), undefined)Feqt(cons(H1, T1), resource)F
eqt(cons(H1, T1), tag)Feqt(cons(H1, T1), true)F
eqt(cons(H1, T1), undefined)Feqt(cons(H1, T1), pid(N2))F
eqt(cons(H1, T1), int(N2))Feqt(cons(H1, T1), cons(H2, T2))and(eqt(H1, H2), eqt(T1, T2))
eqt(cons(H1, T1), tuple(H2, T2))Feqt(cons(H1, T1), tuplenil(H2))F
eqt(tuple(H1, T1), nil)Feqt(tuple(H1, T1), a)F
eqt(tuple(H1, T1), excl)Feqt(tuple(H1, T1), false)F
eqt(tuple(H1, T1), lock)Feqt(tuple(H1, T1), locker)F
eqt(tuple(H1, T1), mcrlrecord)Feqt(tuple(H1, T1), ok)F
eqt(tuple(H1, T1), pending)Feqt(tuple(H1, T1), release)F
eqt(tuple(H1, T1), request)Feqt(tuple(H1, T1), resource)F
eqt(tuple(H1, T1), tag)Feqt(tuple(H1, T1), true)F
eqt(tuple(H1, T1), undefined)Feqt(tuple(H1, T1), pid(N2))F
eqt(tuple(H1, T1), int(N2))Feqt(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)Feqt(tuplenil(H1), a)F
eqt(tuplenil(H1), excl)Feqt(tuplenil(H1), false)F
eqt(tuplenil(H1), lock)Feqt(tuplenil(H1), locker)F
eqt(tuplenil(H1), mcrlrecord)Feqt(tuplenil(H1), ok)F
eqt(tuplenil(H1), pending)Feqt(tuplenil(H1), release)F
eqt(tuplenil(H1), request)Feqt(tuplenil(H1), resource)F
eqt(tuplenil(H1), tag)Feqt(tuplenil(H1), true)F
eqt(tuplenil(H1), undefined)Feqt(tuplenil(H1), pid(N2))F
eqt(tuplenil(H1), int(N2))Feqt(tuplenil(H1), cons(H2, T2))F
eqt(tuplenil(H1), tuple(H2, T2))Feqt(tuplenil(H1), tuplenil(H2))eqt(H1, H2)
element(int(s(0)), tuplenil(T1))T1element(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)Recordrecord_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)nillocker2_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)nillocker2_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)nillocker2_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)falselocker2_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))Feqs(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))S1tops(stack(E1, S1))E1
istops(E1, empty)Fistops(E1, stack(E2, S1))eqt(E1, E2)
eqc(nocalls, nocalls)Teqc(nocalls, calls(E2, S2, CS2))F
eqc(calls(E1, S1, CS1), nocalls)Feqc(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)

Original Signature

Termination of terms over the following signature is verified: tuplenil, record_new, tuple, tag, gen_tag, imp, locker2_map_promote_pending, pops, locker2_check_availables, mcrlrecord, pending, request, empty, false, ok, istops, locker2_add_pending, andt, case2, append, element, case1, case0, tops, push1, case6, case5, or, int, case4, record_extract, locker, case9, case8, locker2_map_add_pending, calls, eqc, and, not, 0, locker2_promote_pending, locker2_claim_lock, locker2_adduniq, stack, release, locker2_obtainables, F, locker2_remove_pending, push, T, gen_modtageq, record_update, undefined, if, record_updates, eqt, excllock, delete, eqs, cons, member, locker2_map_claim_lock, locker2_obtainable, a, pushs, resource, lock, true, locker2_release_lock, pid, equal, subtract, locker2_check_available, s, excl, nil, eq, nocalls

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 12: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

or(T, T)Tor(F, T)T
or(T, F)Tor(F, F)F
and(T, B)Band(B, T)B
and(F, B)Fand(B, F)F
imp(T, B)Bimp(F, B)T
not(T)Fnot(F)T
if(T, B1, B2)B1if(F, B1, B2)B2
eq(T, T)Teq(F, F)T
eq(T, F)Feq(F, T)F
eqt(nil, undefined)Feqt(nil, pid(N2))F
eqt(nil, int(N2))Feqt(nil, cons(H2, T2))F
eqt(nil, tuple(H2, T2))Feqt(nil, tuplenil(H2))F
eqt(a, nil)Feqt(a, a)T
eqt(a, excl)Feqt(a, false)F
eqt(a, lock)Feqt(a, locker)F
eqt(a, mcrlrecord)Feqt(a, ok)F
eqt(a, pending)Feqt(a, release)F
eqt(a, request)Feqt(a, resource)F
eqt(a, tag)Feqt(a, true)F
eqt(a, undefined)Feqt(a, pid(N2))F
eqt(a, int(N2))Feqt(a, cons(H2, T2))F
eqt(a, tuple(H2, T2))Feqt(a, tuplenil(H2))F
eqt(excl, nil)Feqt(excl, a)F
eqt(excl, excl)Teqt(excl, false)F
eqt(excl, lock)Feqt(excl, locker)F
eqt(excl, mcrlrecord)Feqt(excl, ok)F
eqt(excl, pending)Feqt(excl, release)F
eqt(excl, request)Feqt(excl, resource)F
eqt(excl, tag)Feqt(excl, true)F
eqt(excl, undefined)Feqt(excl, pid(N2))F
eqt(excl, eqt(false, int(N2)))Feqt(false, cons(H2, T2))F
eqt(false, tuple(H2, T2))Feqt(false, tuplenil(H2))F
eqt(lock, nil)Feqt(lock, a)F
eqt(lock, excl)Feqt(lock, false)F
eqt(lock, lock)Teqt(lock, locker)F
eqt(lock, mcrlrecord)Feqt(lock, ok)F
eqt(lock, pending)Feqt(lock, release)F
eqt(lock, request)Feqt(lock, resource)F
eqt(lock, tag)Feqt(lock, true)F
eqt(lock, undefined)Feqt(lock, pid(N2))F
eqt(lock, int(N2))Feqt(lock, cons(H2, T2))F
eqt(lock, tuple(H2, T2))Feqt(lock, tuplenil(H2))F
eqt(locker, nil)Feqt(locker, a)F
eqt(locker, excl)Feqt(locker, false)F
eqt(locker, lock)Feqt(locker, locker)T
eqt(locker, mcrlrecord)Feqt(locker, ok)F
eqt(locker, pending)Feqt(locker, release)F
eqt(locker, request)Feqt(locker, resource)F
eqt(locker, tag)Feqt(locker, true)F
eqt(locker, undefined)Feqt(locker, pid(N2))F
eqt(locker, int(N2))Feqt(locker, cons(H2, T2))F
eqt(locker, tuple(H2, T2))Feqt(locker, tuplenil(H2))F
eqt(mcrlrecord, nil)Feqt(mcrlrecord, a)F
eqt(mcrlrecord, excl)Feqt(mcrlrecord, false)F
eqt(mcrlrecord, lock)Feqt(mcrlrecord, locker)F
eqt(mcrlrecord, mcrlrecord)Teqt(mcrlrecord, ok)F
eqt(mcrlrecord, pending)Feqt(mcrlrecord, release)F
eqt(mcrlrecord, request)Feqt(mcrlrecord, resource)F
eqt(ok, resource)Feqt(ok, tag)F
eqt(ok, true)Feqt(ok, undefined)F
eqt(ok, pid(N2))Feqt(ok, int(N2))F
eqt(ok, cons(H2, T2))Feqt(ok, tuple(H2, T2))F
eqt(ok, tuplenil(H2))Feqt(pending, nil)F
eqt(pending, a)Feqt(pending, excl)F
eqt(pending, false)Feqt(pending, lock)F
eqt(pending, locker)Feqt(pending, mcrlrecord)F
eqt(pending, ok)Feqt(pending, pending)T
eqt(pending, release)Feqt(pending, request)F
eqt(pending, resource)Feqt(pending, tag)F
eqt(pending, true)Feqt(pending, undefined)F
eqt(pending, pid(N2))Feqt(pending, int(N2))F
eqt(pending, cons(H2, T2))Feqt(pending, tuple(H2, T2))F
eqt(pending, tuplenil(H2))Feqt(release, nil)F
eqt(release, a)Feqt(release, excl)F
eqt(release, false)Feqt(release, lock)F
eqt(release, locker)Feqt(release, mcrlrecord)F
eqt(release, ok)Feqt(request, mcrlrecord)F
eqt(request, ok)Feqt(request, pending)F
eqt(request, release)Feqt(request, request)T
eqt(request, resource)Feqt(request, tag)F
eqt(request, true)Feqt(request, undefined)F
eqt(request, pid(N2))Feqt(request, int(N2))F
eqt(request, cons(H2, T2))Feqt(request, tuple(H2, T2))F
eqt(request, tuplenil(H2))Feqt(resource, nil)F
eqt(resource, a)Feqt(resource, excl)F
eqt(resource, false)Feqt(resource, lock)F
eqt(resource, locker)Feqt(resource, mcrlrecord)F
eqt(resource, ok)Feqt(resource, pending)F
eqt(resource, release)Feqt(resource, request)F
eqt(resource, resource)Teqt(resource, tag)F
eqt(resource, true)Feqt(resource, undefined)F
eqt(resource, pid(N2))Feqt(resource, int(N2))F
eqt(resource, cons(H2, T2))Feqt(resource, tuple(H2, T2))F
eqt(resource, tuplenil(H2))Feqt(tag, nil)F
eqt(tag, a)Feqt(tag, excl)F
eqt(tag, false)Feqt(tag, lock)F
eqt(tag, locker)Feqt(tag, mcrlrecord)F
eqt(tag, ok)Feqt(tag, pending)F
eqt(tag, release)Feqt(tag, request)F
eqt(tag, resource)Feqt(tag, tag)T
eqt(tag, true)Feqt(tag, undefined)F
eqt(tag, pid(N2))Feqt(tag, int(N2))F
eqt(tag, cons(H2, T2))Feqt(tag, tuple(H2, T2))F
eqt(tag, tuplenil(H2))Feqt(true, nil)F
eqt(true, a)Feqt(true, excl)F
eqt(true, false)Feqt(true, lock)F
eqt(true, locker)Feqt(true, mcrlrecord)F
eqt(true, ok)Feqt(true, pending)F
eqt(true, release)Feqt(true, request)F
eqt(true, resource)Feqt(true, tag)F
eqt(true, true)Teqt(true, undefined)F
eqt(true, pid(N2))Feqt(true, int(N2))F
eqt(true, cons(H2, T2))Feqt(true, tuple(H2, T2))F
eqt(true, tuplenil(H2))Feqt(undefined, nil)F
eqt(undefined, a)Feqt(undefined, tuplenil(H2))F
eqt(pid(N1), nil)Feqt(pid(N1), a)F
eqt(pid(N1), excl)Feqt(pid(N1), false)F
eqt(pid(N1), lock)Feqt(pid(N1), locker)F
eqt(pid(N1), mcrlrecord)Feqt(pid(N1), ok)F
eqt(pid(N1), pending)Feqt(pid(N1), release)F
eqt(pid(N1), request)Feqt(pid(N1), resource)F
eqt(pid(N1), tag)Feqt(pid(N1), true)F
eqt(pid(N1), undefined)Feqt(pid(N1), pid(N2))eqt(N1, N2)
eqt(pid(N1), int(N2))Feqt(pid(N1), cons(H2, T2))F
eqt(pid(N1), tuple(H2, T2))Feqt(pid(N1), tuplenil(H2))F
eqt(int(N1), nil)Feqt(int(N1), a)F
eqt(int(N1), excl)Feqt(int(N1), false)F
eqt(int(N1), lock)Feqt(int(N1), locker)F
eqt(int(N1), mcrlrecord)Feqt(int(N1), ok)F
eqt(int(N1), pending)Feqt(int(N1), release)F
eqt(int(N1), request)Feqt(int(N1), resource)F
eqt(int(N1), tag)Feqt(int(N1), true)F
eqt(int(N1), undefined)Feqt(cons(H1, T1), resource)F
eqt(cons(H1, T1), tag)Feqt(cons(H1, T1), true)F
eqt(cons(H1, T1), undefined)Feqt(cons(H1, T1), pid(N2))F
eqt(cons(H1, T1), int(N2))Feqt(cons(H1, T1), cons(H2, T2))and(eqt(H1, H2), eqt(T1, T2))
eqt(cons(H1, T1), tuple(H2, T2))Feqt(cons(H1, T1), tuplenil(H2))F
eqt(tuple(H1, T1), nil)Feqt(tuple(H1, T1), a)F
eqt(tuple(H1, T1), excl)Feqt(tuple(H1, T1), false)F
eqt(tuple(H1, T1), lock)Feqt(tuple(H1, T1), locker)F
eqt(tuple(H1, T1), mcrlrecord)Feqt(tuple(H1, T1), ok)F
eqt(tuple(H1, T1), pending)Feqt(tuple(H1, T1), release)F
eqt(tuple(H1, T1), request)Feqt(tuple(H1, T1), resource)F
eqt(tuple(H1, T1), tag)Feqt(tuple(H1, T1), true)F
eqt(tuple(H1, T1), undefined)Feqt(tuple(H1, T1), pid(N2))F
eqt(tuple(H1, T1), int(N2))Feqt(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)Feqt(tuplenil(H1), a)F
eqt(tuplenil(H1), excl)Feqt(tuplenil(H1), false)F
eqt(tuplenil(H1), lock)Feqt(tuplenil(H1), locker)F
eqt(tuplenil(H1), mcrlrecord)Feqt(tuplenil(H1), ok)F
eqt(tuplenil(H1), pending)Feqt(tuplenil(H1), release)F
eqt(tuplenil(H1), request)Feqt(tuplenil(H1), resource)F
eqt(tuplenil(H1), tag)Feqt(tuplenil(H1), true)F
eqt(tuplenil(H1), undefined)Feqt(tuplenil(H1), pid(N2))F
eqt(tuplenil(H1), int(N2))Feqt(tuplenil(H1), cons(H2, T2))F
eqt(tuplenil(H1), tuple(H2, T2))Feqt(tuplenil(H1), tuplenil(H2))eqt(H1, H2)
element(int(s(0)), tuplenil(T1))T1element(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)Recordrecord_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)nillocker2_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)nillocker2_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)nillocker2_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)falselocker2_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))Feqs(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))S1tops(stack(E1, S1))E1
istops(E1, empty)Fistops(E1, stack(E2, S1))eqt(E1, E2)
eqc(nocalls, nocalls)Teqc(nocalls, calls(E2, S2, CS2))F
eqc(calls(E1, S1, CS1), nocalls)Feqc(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)

Original Signature

Termination of terms over the following signature is verified: tuplenil, record_new, tuple, tag, gen_tag, imp, locker2_map_promote_pending, pops, locker2_check_availables, mcrlrecord, pending, request, empty, false, ok, istops, locker2_add_pending, andt, case2, append, element, case1, case0, tops, push1, case6, case5, or, int, case4, record_extract, locker, case9, case8, locker2_map_add_pending, calls, eqc, and, not, 0, locker2_promote_pending, locker2_claim_lock, locker2_adduniq, stack, release, locker2_obtainables, F, locker2_remove_pending, push, T, gen_modtageq, record_update, undefined, if, record_updates, eqt, excllock, delete, eqs, cons, member, locker2_map_claim_lock, locker2_obtainable, a, pushs, resource, lock, true, locker2_release_lock, pid, equal, subtract, locker2_check_available, s, excl, nil, eq, nocalls

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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