or(T, T) → T
or(F, T) → T
or(T, F) → T
or(F, F) → F
and(T, B) → B
and(B, T) → B
and(F, B) → F
and(B, F) → F
imp(T, B) → B
imp(F, B) → T
not(T) → F
not(F) → T
if(T, B1, B2) → B1
if(F, B1, B2) → B2
eq(T, T) → T
eq(F, F) → T
eq(T, F) → F
eq(F, T) → F
eqt(nil, undefined) → F
eqt(nil, pid(N2)) → F
eqt(nil, int(N2)) → F
eqt(nil, cons(H2, T2)) → F
eqt(nil, tuple(H2, T2)) → F
eqt(nil, tuplenil(H2)) → F
eqt(a, nil) → F
eqt(a, a) → T
eqt(a, excl) → F
eqt(a, false) → F
eqt(a, lock) → F
eqt(a, locker) → F
eqt(a, mcrlrecord) → F
eqt(a, ok) → F
eqt(a, pending) → F
eqt(a, release) → F
eqt(a, request) → F
eqt(a, resource) → F
eqt(a, tag) → F
eqt(a, true) → F
eqt(a, undefined) → F
eqt(a, pid(N2)) → F
eqt(a, int(N2)) → F
eqt(a, cons(H2, T2)) → F
eqt(a, tuple(H2, T2)) → F
eqt(a, tuplenil(H2)) → F
eqt(excl, nil) → F
eqt(excl, a) → F
eqt(excl, excl) → T
eqt(excl, false) → F
eqt(excl, lock) → F
eqt(excl, locker) → F
eqt(excl, mcrlrecord) → F
eqt(excl, ok) → F
eqt(excl, pending) → F
eqt(excl, release) → F
eqt(excl, request) → F
eqt(excl, resource) → F
eqt(excl, tag) → F
eqt(excl, true) → F
eqt(excl, undefined) → F
eqt(excl, pid(N2)) → F
eqt(excl, eqt(false, int(N2))) → F
eqt(false, cons(H2, T2)) → F
eqt(false, tuple(H2, T2)) → F
eqt(false, tuplenil(H2)) → F
eqt(lock, nil) → F
eqt(lock, a) → F
eqt(lock, excl) → F
eqt(lock, false) → F
eqt(lock, lock) → T
eqt(lock, locker) → F
eqt(lock, mcrlrecord) → F
eqt(lock, ok) → F
eqt(lock, pending) → F
eqt(lock, release) → F
eqt(lock, request) → F
eqt(lock, resource) → F
eqt(lock, tag) → F
eqt(lock, true) → F
eqt(lock, undefined) → F
eqt(lock, pid(N2)) → F
eqt(lock, int(N2)) → F
eqt(lock, cons(H2, T2)) → F
eqt(lock, tuple(H2, T2)) → F
eqt(lock, tuplenil(H2)) → F
eqt(locker, nil) → F
eqt(locker, a) → F
eqt(locker, excl) → F
eqt(locker, false) → F
eqt(locker, lock) → F
eqt(locker, locker) → T
eqt(locker, mcrlrecord) → F
eqt(locker, ok) → F
eqt(locker, pending) → F
eqt(locker, release) → F
eqt(locker, request) → F
eqt(locker, resource) → F
eqt(locker, tag) → F
eqt(locker, true) → F
eqt(locker, undefined) → F
eqt(locker, pid(N2)) → F
eqt(locker, int(N2)) → F
eqt(locker, cons(H2, T2)) → F
eqt(locker, tuple(H2, T2)) → F
eqt(locker, tuplenil(H2)) → F
eqt(mcrlrecord, nil) → F
eqt(mcrlrecord, a) → F
eqt(mcrlrecord, excl) → F
eqt(mcrlrecord, false) → F
eqt(mcrlrecord, lock) → F
eqt(mcrlrecord, locker) → F
eqt(mcrlrecord, mcrlrecord) → T
eqt(mcrlrecord, ok) → F
eqt(mcrlrecord, pending) → F
eqt(mcrlrecord, release) → F
eqt(mcrlrecord, request) → F
eqt(mcrlrecord, resource) → F
eqt(ok, resource) → F
eqt(ok, tag) → F
eqt(ok, true) → F
eqt(ok, undefined) → F
eqt(ok, pid(N2)) → F
eqt(ok, int(N2)) → F
eqt(ok, cons(H2, T2)) → F
eqt(ok, tuple(H2, T2)) → F
eqt(ok, tuplenil(H2)) → F
eqt(pending, nil) → F
eqt(pending, a) → F
eqt(pending, excl) → F
eqt(pending, false) → F
eqt(pending, lock) → F
eqt(pending, locker) → F
eqt(pending, mcrlrecord) → F
eqt(pending, ok) → F
eqt(pending, pending) → T
eqt(pending, release) → F
eqt(pending, request) → F
eqt(pending, resource) → F
eqt(pending, tag) → F
eqt(pending, true) → F
eqt(pending, undefined) → F
eqt(pending, pid(N2)) → F
eqt(pending, int(N2)) → F
eqt(pending, cons(H2, T2)) → F
eqt(pending, tuple(H2, T2)) → F
eqt(pending, tuplenil(H2)) → F
eqt(release, nil) → F
eqt(release, a) → F
eqt(release, excl) → F
eqt(release, false) → F
eqt(release, lock) → F
eqt(release, locker) → F
eqt(release, mcrlrecord) → F
eqt(release, ok) → F
eqt(request, mcrlrecord) → F
eqt(request, ok) → F
eqt(request, pending) → F
eqt(request, release) → F
eqt(request, request) → T
eqt(request, resource) → F
eqt(request, tag) → F
eqt(request, true) → F
eqt(request, undefined) → F
eqt(request, pid(N2)) → F
eqt(request, int(N2)) → F
eqt(request, cons(H2, T2)) → F
eqt(request, tuple(H2, T2)) → F
eqt(request, tuplenil(H2)) → F
eqt(resource, nil) → F
eqt(resource, a) → F
eqt(resource, excl) → F
eqt(resource, false) → F
eqt(resource, lock) → F
eqt(resource, locker) → F
eqt(resource, mcrlrecord) → F
eqt(resource, ok) → F
eqt(resource, pending) → F
eqt(resource, release) → F
eqt(resource, request) → F
eqt(resource, resource) → T
eqt(resource, tag) → F
eqt(resource, true) → F
eqt(resource, undefined) → F
eqt(resource, pid(N2)) → F
eqt(resource, int(N2)) → F
eqt(resource, cons(H2, T2)) → F
eqt(resource, tuple(H2, T2)) → F
eqt(resource, tuplenil(H2)) → F
eqt(tag, nil) → F
eqt(tag, a) → F
eqt(tag, excl) → F
eqt(tag, false) → F
eqt(tag, lock) → F
eqt(tag, locker) → F
eqt(tag, mcrlrecord) → F
eqt(tag, ok) → F
eqt(tag, pending) → F
eqt(tag, release) → F
eqt(tag, request) → F
eqt(tag, resource) → F
eqt(tag, tag) → T
eqt(tag, true) → F
eqt(tag, undefined) → F
eqt(tag, pid(N2)) → F
eqt(tag, int(N2)) → F
eqt(tag, cons(H2, T2)) → F
eqt(tag, tuple(H2, T2)) → F
eqt(tag, tuplenil(H2)) → F
eqt(true, nil) → F
eqt(true, a) → F
eqt(true, excl) → F
eqt(true, false) → F
eqt(true, lock) → F
eqt(true, locker) → F
eqt(true, mcrlrecord) → F
eqt(true, ok) → F
eqt(true, pending) → F
eqt(true, release) → F
eqt(true, request) → F
eqt(true, resource) → F
eqt(true, tag) → F
eqt(true, true) → T
eqt(true, undefined) → F
eqt(true, pid(N2)) → F
eqt(true, int(N2)) → F
eqt(true, cons(H2, T2)) → F
eqt(true, tuple(H2, T2)) → F
eqt(true, tuplenil(H2)) → F
eqt(undefined, nil) → F
eqt(undefined, a) → F
eqt(undefined, tuplenil(H2)) → F
eqt(pid(N1), nil) → F
eqt(pid(N1), a) → F
eqt(pid(N1), excl) → F
eqt(pid(N1), false) → F
eqt(pid(N1), lock) → F
eqt(pid(N1), locker) → F
eqt(pid(N1), mcrlrecord) → F
eqt(pid(N1), ok) → F
eqt(pid(N1), pending) → F
eqt(pid(N1), release) → F
eqt(pid(N1), request) → F
eqt(pid(N1), resource) → F
eqt(pid(N1), tag) → F
eqt(pid(N1), true) → F
eqt(pid(N1), undefined) → F
eqt(pid(N1), pid(N2)) → eqt(N1, N2)
eqt(pid(N1), int(N2)) → F
eqt(pid(N1), cons(H2, T2)) → F
eqt(pid(N1), tuple(H2, T2)) → F
eqt(pid(N1), tuplenil(H2)) → F
eqt(int(N1), nil) → F
eqt(int(N1), a) → F
eqt(int(N1), excl) → F
eqt(int(N1), false) → F
eqt(int(N1), lock) → F
eqt(int(N1), locker) → F
eqt(int(N1), mcrlrecord) → F
eqt(int(N1), ok) → F
eqt(int(N1), pending) → F
eqt(int(N1), release) → F
eqt(int(N1), request) → F
eqt(int(N1), resource) → F
eqt(int(N1), tag) → F
eqt(int(N1), true) → F
eqt(int(N1), undefined) → F
eqt(cons(H1, T1), resource) → F
eqt(cons(H1, T1), tag) → F
eqt(cons(H1, T1), true) → F
eqt(cons(H1, T1), undefined) → F
eqt(cons(H1, T1), pid(N2)) → F
eqt(cons(H1, T1), int(N2)) → F
eqt(cons(H1, T1), cons(H2, T2)) → and(eqt(H1, H2), eqt(T1, T2))
eqt(cons(H1, T1), tuple(H2, T2)) → F
eqt(cons(H1, T1), tuplenil(H2)) → F
eqt(tuple(H1, T1), nil) → F
eqt(tuple(H1, T1), a) → F
eqt(tuple(H1, T1), excl) → F
eqt(tuple(H1, T1), false) → F
eqt(tuple(H1, T1), lock) → F
eqt(tuple(H1, T1), locker) → F
eqt(tuple(H1, T1), mcrlrecord) → F
eqt(tuple(H1, T1), ok) → F
eqt(tuple(H1, T1), pending) → F
eqt(tuple(H1, T1), release) → F
eqt(tuple(H1, T1), request) → F
eqt(tuple(H1, T1), resource) → F
eqt(tuple(H1, T1), tag) → F
eqt(tuple(H1, T1), true) → F
eqt(tuple(H1, T1), undefined) → F
eqt(tuple(H1, T1), pid(N2)) → F
eqt(tuple(H1, T1), int(N2)) → F
eqt(tuple(H1, T1), cons(H2, T2)) → F
eqt(tuple(H1, T1), tuple(H2, T2)) → and(eqt(H1, H2), eqt(T1, T2))
eqt(tuple(H1, T1), tuplenil(H2)) → F
eqt(tuplenil(H1), nil) → F
eqt(tuplenil(H1), a) → F
eqt(tuplenil(H1), excl) → F
eqt(tuplenil(H1), false) → F
eqt(tuplenil(H1), lock) → F
eqt(tuplenil(H1), locker) → F
eqt(tuplenil(H1), mcrlrecord) → F
eqt(tuplenil(H1), ok) → F
eqt(tuplenil(H1), pending) → F
eqt(tuplenil(H1), release) → F
eqt(tuplenil(H1), request) → F
eqt(tuplenil(H1), resource) → F
eqt(tuplenil(H1), tag) → F
eqt(tuplenil(H1), true) → F
eqt(tuplenil(H1), undefined) → F
eqt(tuplenil(H1), pid(N2)) → F
eqt(tuplenil(H1), int(N2)) → F
eqt(tuplenil(H1), cons(H2, T2)) → F
eqt(tuplenil(H1), tuple(H2, T2)) → F
eqt(tuplenil(H1), tuplenil(H2)) → eqt(H1, H2)
element(int(s(0)), tuplenil(T1)) → T1
element(int(s(0)), tuple(T1, T2)) → T1
element(int(s(s(N1))), tuple(T1, T2)) → element(int(s(N1)), T2)
record_new(lock) → tuple(mcrlrecord, tuple(lock, tuple(undefined, tuple(nil, tuplenil(nil)))))
record_extract(tuple(mcrlrecord, tuple(lock, tuple(F0, tuple(F1, tuplenil(F2))))), lock, resource) → tuple(mcrlrecord, tuple(lock, tuple(F0, tuple(F1, tuplenil(F2)))))
record_update(tuple(mcrlrecord, tuple(lock, tuple(F0, tuple(F1, tuplenil(F2))))), lock, pending, NewF) → tuple(mcrlrecord, tuple(lock, tuple(F0, tuple(F1, tuplenil(NewF)))))
record_updates(Record, Name, nil) → Record
record_updates(Record, Name, cons(tuple(Field, tuplenil(NewF)), Fields)) → record_updates(record_update(Record, Name, Field, NewF), Name, Fields)
locker2_map_promote_pending(nil, Pending) → nil
locker2_map_promote_pending(cons(Lock, Locks), Pending) → cons(locker2_promote_pending(Lock, Pending), locker2_map_promote_pending(Locks, Pending))
locker2_map_claim_lock(nil, Resources, Client) → nil
locker2_map_claim_lock(cons(Lock, Locks), Resources, Client) → cons(locker2_claim_lock(Lock, Resources, Client), locker2_map_claim_lock(Locks, Resources, Client))
locker2_map_add_pending(nil, Resources, Client) → nil
locker2_promote_pending(Lock, Client) → case0(Client, Lock, record_extract(Lock, lock, pending))
case0(Client, Lock, cons(Client, Pendings)) → record_updates(Lock, lock, cons(tuple(excl, tuplenil(Client)), cons(tuple(pending, tuplenil(Pendings)), nil)))
case0(Client, Lock, MCRLFree0) → Lock
locker2_remove_pending(Lock, Client) → record_updates(Lock, lock, cons(tuple(pending, tuplenil(subtract(record_extract(Lock, lock, pending), cons(Client, nil)))), nil))
locker2_add_pending(Lock, Resources, Client) → case1(Client, Resources, Lock, member(record_extract(Lock, lock, resource), Resources))
case1(Client, Resources, Lock, true) → record_updates(Lock, lock, cons(tuple(pending, tuplenil(append(record_extract(Lock, lock, pending), cons(Client, nil)))), nil))
case1(Client, Resources, Lock, false) → Lock
locker2_release_lock(Lock, Client) → case2(Client, Lock, gen_modtageq(Client, record_extract(Lock, lock, excl)))
case2(Client, Lock, true) → record_updates(Lock, lock, cons(tuple(excllock, excl), nil))
case4(Client, Lock, MCRLFree1) → false
locker2_obtainables(nil, Client) → true
locker2_obtainables(cons(Lock, Locks), Client) → case5(Client, Locks, Lock, member(Client, record_extract(Lock, lock, pending)))
case5(Client, Locks, Lock, true) → andt(locker2_obtainable(Lock, Client), locker2_obtainables(Locks, Client))
case5(Client, Locks, Lock, false) → locker2_obtainables(Locks, Client)
locker2_check_available(Resource, nil) → false
locker2_check_available(Resource, cons(Lock, Locks)) → case6(Locks, Lock, Resource, equal(Resource, record_extract(Lock, lock, resource)))
case6(Locks, Lock, Resource, true) → andt(equal(record_extract(Lock, lock, excl), nil), equal(record_extract(Lock, lock, pending), nil))
case6(Locks, Lock, Resource, false) → locker2_check_available(Resource, Locks)
locker2_check_availables(nil, Locks) → true
locker2_check_availables(cons(Resource, Resources), Locks) → andt(locker2_check_available(Resource, Locks), locker2_check_availables(Resources, Locks))
locker2_adduniq(nil, List) → List
append(cons(Head, Tail), List) → cons(Head, append(Tail, List))
subtract(List, nil) → List
subtract(List, cons(Head, Tail)) → subtract(delete(Head, List), Tail)
delete(E, nil) → nil
delete(E, cons(Head, Tail)) → case8(Tail, Head, E, equal(E, Head))
case8(Tail, Head, E, true) → Tail
case8(Tail, Head, E, false) → cons(Head, delete(E, Tail))
gen_tag(Pid) → tuple(Pid, tuplenil(tag))
gen_modtageq(Client1, Client2) → equal(Client1, Client2)
member(E, nil) → false
member(E, cons(Head, Tail)) → case9(Tail, Head, E, equal(E, Head))
case9(Tail, Head, E, true) → true
case9(Tail, Head, E, false) → member(E, Tail)
eqs(empty, empty) → T
eqs(empty, stack(E2, S2)) → F
eqs(stack(E1, S1), empty) → F
eqs(stack(E1, S1), stack(E2, S2)) → and(eqt(E1, E2), eqs(S1, S2))
pushs(E1, S1) → stack(E1, S1)
pops(stack(E1, S1)) → S1
tops(stack(E1, S1)) → E1
istops(E1, empty) → F
istops(E1, stack(E2, S1)) → eqt(E1, E2)
eqc(nocalls, nocalls) → T
eqc(nocalls, calls(E2, S2, CS2)) → F
eqc(calls(E1, S1, CS1), nocalls) → F
eqc(calls(E1, S1, CS1), calls(E2, S2, CS2)) → and(eqt(E1, E2), and(eqs(S1, S2), eqc(CS1, CS2)))
push(E1, E2, nocalls) → calls(E1, stack(E2, empty), nocalls)
push(E1, E2, calls(E3, S1, CS1)) → push1(E1, E2, E3, S1, CS1, eqt(E1, E3))
push1(E1, E2, E3, S1, CS1, T) → calls(E3, pushs(E2, S1), CS1)
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
or'(T', T') → T'
or'(F', T') → T'
or'(T', F') → T'
or'(F', F') → F'
and'(T', B) → B
and'(B, T') → B
and'(F', B) → F'
and'(B, F') → F'
imp'(T', B) → B
imp'(F', B) → T'
not'(T') → F'
not'(F') → T'
if'(T', B1, B2) → B1
if'(F', B1, B2) → B2
eq'(T', T') → T'
eq'(F', F') → T'
eq'(T', F') → F'
eq'(F', T') → F'
eqt'(nil', undefined') → F'
eqt'(nil', pid'(N2)) → F'
eqt'(nil', int'(N2)) → F'
eqt'(nil', cons'(H2, T2)) → F'
eqt'(nil', tuple'(H2, T2)) → F'
eqt'(nil', tuplenil'(H2)) → F'
eqt'(a', nil') → F'
eqt'(a', a') → T'
eqt'(a', excl') → F'
eqt'(a', false') → F'
eqt'(a', lock') → F'
eqt'(a', locker') → F'
eqt'(a', mcrlrecord') → F'
eqt'(a', ok') → F'
eqt'(a', pending') → F'
eqt'(a', release') → F'
eqt'(a', request') → F'
eqt'(a', resource') → F'
eqt'(a', tag') → F'
eqt'(a', true') → F'
eqt'(a', undefined') → F'
eqt'(a', pid'(N2)) → F'
eqt'(a', int'(N2)) → F'
eqt'(a', cons'(H2, T2)) → F'
eqt'(a', tuple'(H2, T2)) → F'
eqt'(a', tuplenil'(H2)) → F'
eqt'(excl', nil') → F'
eqt'(excl', a') → F'
eqt'(excl', excl') → T'
eqt'(excl', false') → F'
eqt'(excl', lock') → F'
eqt'(excl', locker') → F'
eqt'(excl', mcrlrecord') → F'
eqt'(excl', ok') → F'
eqt'(excl', pending') → F'
eqt'(excl', release') → F'
eqt'(excl', request') → F'
eqt'(excl', resource') → F'
eqt'(excl', tag') → F'
eqt'(excl', true') → F'
eqt'(excl', undefined') → F'
eqt'(excl', pid'(N2)) → F'
eqt'(excl', eqt'(false', int'(N2))) → F'
eqt'(false', cons'(H2, T2)) → F'
eqt'(false', tuple'(H2, T2)) → F'
eqt'(false', tuplenil'(H2)) → F'
eqt'(lock', nil') → F'
eqt'(lock', a') → F'
eqt'(lock', excl') → F'
eqt'(lock', false') → F'
eqt'(lock', lock') → T'
eqt'(lock', locker') → F'
eqt'(lock', mcrlrecord') → F'
eqt'(lock', ok') → F'
eqt'(lock', pending') → F'
eqt'(lock', release') → F'
eqt'(lock', request') → F'
eqt'(lock', resource') → F'
eqt'(lock', tag') → F'
eqt'(lock', true') → F'
eqt'(lock', undefined') → F'
eqt'(lock', pid'(N2)) → F'
eqt'(lock', int'(N2)) → F'
eqt'(lock', cons'(H2, T2)) → F'
eqt'(lock', tuple'(H2, T2)) → F'
eqt'(lock', tuplenil'(H2)) → F'
eqt'(locker', nil') → F'
eqt'(locker', a') → F'
eqt'(locker', excl') → F'
eqt'(locker', false') → F'
eqt'(locker', lock') → F'
eqt'(locker', locker') → T'
eqt'(locker', mcrlrecord') → F'
eqt'(locker', ok') → F'
eqt'(locker', pending') → F'
eqt'(locker', release') → F'
eqt'(locker', request') → F'
eqt'(locker', resource') → F'
eqt'(locker', tag') → F'
eqt'(locker', true') → F'
eqt'(locker', undefined') → F'
eqt'(locker', pid'(N2)) → F'
eqt'(locker', int'(N2)) → F'
eqt'(locker', cons'(H2, T2)) → F'
eqt'(locker', tuple'(H2, T2)) → F'
eqt'(locker', tuplenil'(H2)) → F'
eqt'(mcrlrecord', nil') → F'
eqt'(mcrlrecord', a') → F'
eqt'(mcrlrecord', excl') → F'
eqt'(mcrlrecord', false') → F'
eqt'(mcrlrecord', lock') → F'
eqt'(mcrlrecord', locker') → F'
eqt'(mcrlrecord', mcrlrecord') → T'
eqt'(mcrlrecord', ok') → F'
eqt'(mcrlrecord', pending') → F'
eqt'(mcrlrecord', release') → F'
eqt'(mcrlrecord', request') → F'
eqt'(mcrlrecord', resource') → F'
eqt'(ok', resource') → F'
eqt'(ok', tag') → F'
eqt'(ok', true') → F'
eqt'(ok', undefined') → F'
eqt'(ok', pid'(N2)) → F'
eqt'(ok', int'(N2)) → F'
eqt'(ok', cons'(H2, T2)) → F'
eqt'(ok', tuple'(H2, T2)) → F'
eqt'(ok', tuplenil'(H2)) → F'
eqt'(pending', nil') → F'
eqt'(pending', a') → F'
eqt'(pending', excl') → F'
eqt'(pending', false') → F'
eqt'(pending', lock') → F'
eqt'(pending', locker') → F'
eqt'(pending', mcrlrecord') → F'
eqt'(pending', ok') → F'
eqt'(pending', pending') → T'
eqt'(pending', release') → F'
eqt'(pending', request') → F'
eqt'(pending', resource') → F'
eqt'(pending', tag') → F'
eqt'(pending', true') → F'
eqt'(pending', undefined') → F'
eqt'(pending', pid'(N2)) → F'
eqt'(pending', int'(N2)) → F'
eqt'(pending', cons'(H2, T2)) → F'
eqt'(pending', tuple'(H2, T2)) → F'
eqt'(pending', tuplenil'(H2)) → F'
eqt'(release', nil') → F'
eqt'(release', a') → F'
eqt'(release', excl') → F'
eqt'(release', false') → F'
eqt'(release', lock') → F'
eqt'(release', locker') → F'
eqt'(release', mcrlrecord') → F'
eqt'(release', ok') → F'
eqt'(request', mcrlrecord') → F'
eqt'(request', ok') → F'
eqt'(request', pending') → F'
eqt'(request', release') → F'
eqt'(request', request') → T'
eqt'(request', resource') → F'
eqt'(request', tag') → F'
eqt'(request', true') → F'
eqt'(request', undefined') → F'
eqt'(request', pid'(N2)) → F'
eqt'(request', int'(N2)) → F'
eqt'(request', cons'(H2, T2)) → F'
eqt'(request', tuple'(H2, T2)) → F'
eqt'(request', tuplenil'(H2)) → F'
eqt'(resource', nil') → F'
eqt'(resource', a') → F'
eqt'(resource', excl') → F'
eqt'(resource', false') → F'
eqt'(resource', lock') → F'
eqt'(resource', locker') → F'
eqt'(resource', mcrlrecord') → F'
eqt'(resource', ok') → F'
eqt'(resource', pending') → F'
eqt'(resource', release') → F'
eqt'(resource', request') → F'
eqt'(resource', resource') → T'
eqt'(resource', tag') → F'
eqt'(resource', true') → F'
eqt'(resource', undefined') → F'
eqt'(resource', pid'(N2)) → F'
eqt'(resource', int'(N2)) → F'
eqt'(resource', cons'(H2, T2)) → F'
eqt'(resource', tuple'(H2, T2)) → F'
eqt'(resource', tuplenil'(H2)) → F'
eqt'(tag', nil') → F'
eqt'(tag', a') → F'
eqt'(tag', excl') → F'
eqt'(tag', false') → F'
eqt'(tag', lock') → F'
eqt'(tag', locker') → F'
eqt'(tag', mcrlrecord') → F'
eqt'(tag', ok') → F'
eqt'(tag', pending') → F'
eqt'(tag', release') → F'
eqt'(tag', request') → F'
eqt'(tag', resource') → F'
eqt'(tag', tag') → T'
eqt'(tag', true') → F'
eqt'(tag', undefined') → F'
eqt'(tag', pid'(N2)) → F'
eqt'(tag', int'(N2)) → F'
eqt'(tag', cons'(H2, T2)) → F'
eqt'(tag', tuple'(H2, T2)) → F'
eqt'(tag', tuplenil'(H2)) → F'
eqt'(true', nil') → F'
eqt'(true', a') → F'
eqt'(true', excl') → F'
eqt'(true', false') → F'
eqt'(true', lock') → F'
eqt'(true', locker') → F'
eqt'(true', mcrlrecord') → F'
eqt'(true', ok') → F'
eqt'(true', pending') → F'
eqt'(true', release') → F'
eqt'(true', request') → F'
eqt'(true', resource') → F'
eqt'(true', tag') → F'
eqt'(true', true') → T'
eqt'(true', undefined') → F'
eqt'(true', pid'(N2)) → F'
eqt'(true', int'(N2)) → F'
eqt'(true', cons'(H2, T2)) → F'
eqt'(true', tuple'(H2, T2)) → F'
eqt'(true', tuplenil'(H2)) → F'
eqt'(undefined', nil') → F'
eqt'(undefined', a') → F'
eqt'(undefined', tuplenil'(H2)) → F'
eqt'(pid'(N1), nil') → F'
eqt'(pid'(N1), a') → F'
eqt'(pid'(N1), excl') → F'
eqt'(pid'(N1), false') → F'
eqt'(pid'(N1), lock') → F'
eqt'(pid'(N1), locker') → F'
eqt'(pid'(N1), mcrlrecord') → F'
eqt'(pid'(N1), ok') → F'
eqt'(pid'(N1), pending') → F'
eqt'(pid'(N1), release') → F'
eqt'(pid'(N1), request') → F'
eqt'(pid'(N1), resource') → F'
eqt'(pid'(N1), tag') → F'
eqt'(pid'(N1), true') → F'
eqt'(pid'(N1), undefined') → F'
eqt'(pid'(N1), pid'(N2)) → eqt'(N1, N2)
eqt'(pid'(N1), int'(N2)) → F'
eqt'(pid'(N1), cons'(H2, T2)) → F'
eqt'(pid'(N1), tuple'(H2, T2)) → F'
eqt'(pid'(N1), tuplenil'(H2)) → F'
eqt'(int'(N1), nil') → F'
eqt'(int'(N1), a') → F'
eqt'(int'(N1), excl') → F'
eqt'(int'(N1), false') → F'
eqt'(int'(N1), lock') → F'
eqt'(int'(N1), locker') → F'
eqt'(int'(N1), mcrlrecord') → F'
eqt'(int'(N1), ok') → F'
eqt'(int'(N1), pending') → F'
eqt'(int'(N1), release') → F'
eqt'(int'(N1), request') → F'
eqt'(int'(N1), resource') → F'
eqt'(int'(N1), tag') → F'
eqt'(int'(N1), true') → F'
eqt'(int'(N1), undefined') → F'
eqt'(cons'(H1, T1), resource') → F'
eqt'(cons'(H1, T1), tag') → F'
eqt'(cons'(H1, T1), true') → F'
eqt'(cons'(H1, T1), undefined') → F'
eqt'(cons'(H1, T1), pid'(N2)) → F'
eqt'(cons'(H1, T1), int'(N2)) → F'
eqt'(cons'(H1, T1), cons'(H2, T2)) → and'(eqt'(H1, H2), eqt'(T1, T2))
eqt'(cons'(H1, T1), tuple'(H2, T2)) → F'
eqt'(cons'(H1, T1), tuplenil'(H2)) → F'
eqt'(tuple'(H1, T1), nil') → F'
eqt'(tuple'(H1, T1), a') → F'
eqt'(tuple'(H1, T1), excl') → F'
eqt'(tuple'(H1, T1), false') → F'
eqt'(tuple'(H1, T1), lock') → F'
eqt'(tuple'(H1, T1), locker') → F'
eqt'(tuple'(H1, T1), mcrlrecord') → F'
eqt'(tuple'(H1, T1), ok') → F'
eqt'(tuple'(H1, T1), pending') → F'
eqt'(tuple'(H1, T1), release') → F'
eqt'(tuple'(H1, T1), request') → F'
eqt'(tuple'(H1, T1), resource') → F'
eqt'(tuple'(H1, T1), tag') → F'
eqt'(tuple'(H1, T1), true') → F'
eqt'(tuple'(H1, T1), undefined') → F'
eqt'(tuple'(H1, T1), pid'(N2)) → F'
eqt'(tuple'(H1, T1), int'(N2)) → F'
eqt'(tuple'(H1, T1), cons'(H2, T2)) → F'
eqt'(tuple'(H1, T1), tuple'(H2, T2)) → and'(eqt'(H1, H2), eqt'(T1, T2))
eqt'(tuple'(H1, T1), tuplenil'(H2)) → F'
eqt'(tuplenil'(H1), nil') → F'
eqt'(tuplenil'(H1), a') → F'
eqt'(tuplenil'(H1), excl') → F'
eqt'(tuplenil'(H1), false') → F'
eqt'(tuplenil'(H1), lock') → F'
eqt'(tuplenil'(H1), locker') → F'
eqt'(tuplenil'(H1), mcrlrecord') → F'
eqt'(tuplenil'(H1), ok') → F'
eqt'(tuplenil'(H1), pending') → F'
eqt'(tuplenil'(H1), release') → F'
eqt'(tuplenil'(H1), request') → F'
eqt'(tuplenil'(H1), resource') → F'
eqt'(tuplenil'(H1), tag') → F'
eqt'(tuplenil'(H1), true') → F'
eqt'(tuplenil'(H1), undefined') → F'
eqt'(tuplenil'(H1), pid'(N2)) → F'
eqt'(tuplenil'(H1), int'(N2)) → F'
eqt'(tuplenil'(H1), cons'(H2, T2)) → F'
eqt'(tuplenil'(H1), tuple'(H2, T2)) → F'
eqt'(tuplenil'(H1), tuplenil'(H2)) → eqt'(H1, H2)
element'(int'(s'(0')), tuplenil'(T1)) → T1
element'(int'(s'(0')), tuple'(T1, T2)) → T1
element'(int'(s'(s'(N1))), tuple'(T1, T2)) → element'(int'(s'(N1)), T2)
record_new'(lock') → tuple'(mcrlrecord', tuple'(lock', tuple'(undefined', tuple'(nil', tuplenil'(nil')))))
record_extract'(tuple'(mcrlrecord', tuple'(lock', tuple'(F0, tuple'(F1, tuplenil'(F2))))), lock', resource') → tuple'(mcrlrecord', tuple'(lock', tuple'(F0, tuple'(F1, tuplenil'(F2)))))
record_update'(tuple'(mcrlrecord', tuple'(lock', tuple'(F0, tuple'(F1, tuplenil'(F2))))), lock', pending', NewF) → tuple'(mcrlrecord', tuple'(lock', tuple'(F0, tuple'(F1, tuplenil'(NewF)))))
record_updates'(Record, Name, nil') → Record
record_updates'(Record, Name, cons'(tuple'(Field, tuplenil'(NewF)), Fields)) → record_updates'(record_update'(Record, Name, Field, NewF), Name, Fields)
locker2_map_promote_pending'(nil', Pending) → nil'
locker2_map_promote_pending'(cons'(Lock, Locks), Pending) → cons'(locker2_promote_pending'(Lock, Pending), locker2_map_promote_pending'(Locks, Pending))
locker2_map_claim_lock'(nil', Resources, Client) → nil'
locker2_map_claim_lock'(cons'(Lock, Locks), Resources, Client) → cons'(locker2_claim_lock'(Lock, Resources, Client), locker2_map_claim_lock'(Locks, Resources, Client))
locker2_map_add_pending'(nil', Resources, Client) → nil'
locker2_promote_pending'(Lock, Client) → case0'(Client, Lock, record_extract'(Lock, lock', pending'))
case0'(Client, Lock, cons'(Client, Pendings)) → record_updates'(Lock, lock', cons'(tuple'(excl', tuplenil'(Client)), cons'(tuple'(pending', tuplenil'(Pendings)), nil')))
case0'(Client, Lock, MCRLFree0) → Lock
locker2_remove_pending'(Lock, Client) → record_updates'(Lock, lock', cons'(tuple'(pending', tuplenil'(subtract'(record_extract'(Lock, lock', pending'), cons'(Client, nil')))), nil'))
locker2_add_pending'(Lock, Resources, Client) → case1'(Client, Resources, Lock, member'(record_extract'(Lock, lock', resource'), Resources))
case1'(Client, Resources, Lock, true') → record_updates'(Lock, lock', cons'(tuple'(pending', tuplenil'(append'(record_extract'(Lock, lock', pending'), cons'(Client, nil')))), nil'))
case1'(Client, Resources, Lock, false') → Lock
locker2_release_lock'(Lock, Client) → case2'(Client, Lock, gen_modtageq'(Client, record_extract'(Lock, lock', excl')))
case2'(Client, Lock, true') → record_updates'(Lock, lock', cons'(tuple'(excllock', excl'), nil'))
case4'(Client, Lock, MCRLFree1) → false'
locker2_obtainables'(nil', Client) → true'
locker2_obtainables'(cons'(Lock, Locks), Client) → case5'(Client, Locks, Lock, member'(Client, record_extract'(Lock, lock', pending')))
case5'(Client, Locks, Lock, true') → andt'(locker2_obtainable'(Lock, Client), locker2_obtainables'(Locks, Client))
case5'(Client, Locks, Lock, false') → locker2_obtainables'(Locks, Client)
locker2_check_available'(Resource, nil') → false'
locker2_check_available'(Resource, cons'(Lock, Locks)) → case6'(Locks, Lock, Resource, equal'(Resource, record_extract'(Lock, lock', resource')))
case6'(Locks, Lock, Resource, true') → andt'(equal'(record_extract'(Lock, lock', excl'), nil'), equal'(record_extract'(Lock, lock', pending'), nil'))
case6'(Locks, Lock, Resource, false') → locker2_check_available'(Resource, Locks)
locker2_check_availables'(nil', Locks) → true'
locker2_check_availables'(cons'(Resource, Resources), Locks) → andt'(locker2_check_available'(Resource, Locks), locker2_check_availables'(Resources, Locks))
locker2_adduniq'(nil', List) → List
append'(cons'(Head, Tail), List) → cons'(Head, append'(Tail, List))
subtract'(List, nil') → List
subtract'(List, cons'(Head, Tail)) → subtract'(delete'(Head, List), Tail)
delete'(E, nil') → nil'
delete'(E, cons'(Head, Tail)) → case8'(Tail, Head, E, equal'(E, Head))
case8'(Tail, Head, E, true') → Tail
case8'(Tail, Head, E, false') → cons'(Head, delete'(E, Tail))
gen_tag'(Pid) → tuple'(Pid, tuplenil'(tag'))
gen_modtageq'(Client1, Client2) → equal'(Client1, Client2)
member'(E, nil') → false'
member'(E, cons'(Head, Tail)) → case9'(Tail, Head, E, equal'(E, Head))
case9'(Tail, Head, E, true') → true'
case9'(Tail, Head, E, false') → member'(E, Tail)
eqs'(empty', empty') → T'
eqs'(empty', stack'(E2, S2)) → F'
eqs'(stack'(E1, S1), empty') → F'
eqs'(stack'(E1, S1), stack'(E2, S2)) → and'(eqt'(E1, E2), eqs'(S1, S2))
pushs'(E1, S1) → stack'(E1, S1)
pops'(stack'(E1, S1)) → S1
tops'(stack'(E1, S1)) → E1
istops'(E1, empty') → F'
istops'(E1, stack'(E2, S1)) → eqt'(E1, E2)
eqc'(nocalls', nocalls') → T'
eqc'(nocalls', calls'(E2, S2, CS2)) → F'
eqc'(calls'(E1, S1, CS1), nocalls') → F'
eqc'(calls'(E1, S1, CS1), calls'(E2, S2, CS2)) → and'(eqt'(E1, E2), and'(eqs'(S1, S2), eqc'(CS1, CS2)))
push'(E1, E2, nocalls') → calls'(E1, stack'(E2, empty'), nocalls')
push'(E1, E2, calls'(E3, S1, CS1)) → push1'(E1, E2, E3, S1, CS1, eqt'(E1, E3))
push1'(E1, E2, E3, S1, CS1, T') → calls'(E3, pushs'(E2, S1), CS1)
Sliced the following arguments:
locker2_map_claim_lock'/1
locker2_map_claim_lock'/2
locker2_claim_lock'/0
locker2_claim_lock'/1
locker2_claim_lock'/2
locker2_map_add_pending'/1
locker2_map_add_pending'/2
locker2_add_pending'/2
case1'/0
case1'/1
append'/1
case2'/0
case4'/0
case4'/1
case4'/2
case5'/2
locker2_obtainable'/0
locker2_obtainable'/1
case9'/1
push1'/0
Runtime Complexity TRS:
The TRS R consists of the following rules:
or'(T', T') → T'
or'(F', T') → T'
or'(T', F') → T'
or'(F', F') → F'
and'(T', B) → B
and'(B, T') → B
and'(F', B) → F'
and'(B, F') → F'
imp'(T', B) → B
imp'(F', B) → T'
not'(T') → F'
not'(F') → T'
if'(T', B1, B2) → B1
if'(F', B1, B2) → B2
eq'(T', T') → T'
eq'(F', F') → T'
eq'(T', F') → F'
eq'(F', T') → F'
eqt'(nil', undefined') → F'
eqt'(nil', pid'(N2)) → F'
eqt'(nil', int'(N2)) → F'
eqt'(nil', cons'(H2, T2)) → F'
eqt'(nil', tuple'(H2, T2)) → F'
eqt'(nil', tuplenil'(H2)) → F'
eqt'(a', nil') → F'
eqt'(a', a') → T'
eqt'(a', excl') → F'
eqt'(a', false') → F'
eqt'(a', lock') → F'
eqt'(a', locker') → F'
eqt'(a', mcrlrecord') → F'
eqt'(a', ok') → F'
eqt'(a', pending') → F'
eqt'(a', release') → F'
eqt'(a', request') → F'
eqt'(a', resource') → F'
eqt'(a', tag') → F'
eqt'(a', true') → F'
eqt'(a', undefined') → F'
eqt'(a', pid'(N2)) → F'
eqt'(a', int'(N2)) → F'
eqt'(a', cons'(H2, T2)) → F'
eqt'(a', tuple'(H2, T2)) → F'
eqt'(a', tuplenil'(H2)) → F'
eqt'(excl', nil') → F'
eqt'(excl', a') → F'
eqt'(excl', excl') → T'
eqt'(excl', false') → F'
eqt'(excl', lock') → F'
eqt'(excl', locker') → F'
eqt'(excl', mcrlrecord') → F'
eqt'(excl', ok') → F'
eqt'(excl', pending') → F'
eqt'(excl', release') → F'
eqt'(excl', request') → F'
eqt'(excl', resource') → F'
eqt'(excl', tag') → F'
eqt'(excl', true') → F'
eqt'(excl', undefined') → F'
eqt'(excl', pid'(N2)) → F'
eqt'(excl', eqt'(false', int'(N2))) → F'
eqt'(false', cons'(H2, T2)) → F'
eqt'(false', tuple'(H2, T2)) → F'
eqt'(false', tuplenil'(H2)) → F'
eqt'(lock', nil') → F'
eqt'(lock', a') → F'
eqt'(lock', excl') → F'
eqt'(lock', false') → F'
eqt'(lock', lock') → T'
eqt'(lock', locker') → F'
eqt'(lock', mcrlrecord') → F'
eqt'(lock', ok') → F'
eqt'(lock', pending') → F'
eqt'(lock', release') → F'
eqt'(lock', request') → F'
eqt'(lock', resource') → F'
eqt'(lock', tag') → F'
eqt'(lock', true') → F'
eqt'(lock', undefined') → F'
eqt'(lock', pid'(N2)) → F'
eqt'(lock', int'(N2)) → F'
eqt'(lock', cons'(H2, T2)) → F'
eqt'(lock', tuple'(H2, T2)) → F'
eqt'(lock', tuplenil'(H2)) → F'
eqt'(locker', nil') → F'
eqt'(locker', a') → F'
eqt'(locker', excl') → F'
eqt'(locker', false') → F'
eqt'(locker', lock') → F'
eqt'(locker', locker') → T'
eqt'(locker', mcrlrecord') → F'
eqt'(locker', ok') → F'
eqt'(locker', pending') → F'
eqt'(locker', release') → F'
eqt'(locker', request') → F'
eqt'(locker', resource') → F'
eqt'(locker', tag') → F'
eqt'(locker', true') → F'
eqt'(locker', undefined') → F'
eqt'(locker', pid'(N2)) → F'
eqt'(locker', int'(N2)) → F'
eqt'(locker', cons'(H2, T2)) → F'
eqt'(locker', tuple'(H2, T2)) → F'
eqt'(locker', tuplenil'(H2)) → F'
eqt'(mcrlrecord', nil') → F'
eqt'(mcrlrecord', a') → F'
eqt'(mcrlrecord', excl') → F'
eqt'(mcrlrecord', false') → F'
eqt'(mcrlrecord', lock') → F'
eqt'(mcrlrecord', locker') → F'
eqt'(mcrlrecord', mcrlrecord') → T'
eqt'(mcrlrecord', ok') → F'
eqt'(mcrlrecord', pending') → F'
eqt'(mcrlrecord', release') → F'
eqt'(mcrlrecord', request') → F'
eqt'(mcrlrecord', resource') → F'
eqt'(ok', resource') → F'
eqt'(ok', tag') → F'
eqt'(ok', true') → F'
eqt'(ok', undefined') → F'
eqt'(ok', pid'(N2)) → F'
eqt'(ok', int'(N2)) → F'
eqt'(ok', cons'(H2, T2)) → F'
eqt'(ok', tuple'(H2, T2)) → F'
eqt'(ok', tuplenil'(H2)) → F'
eqt'(pending', nil') → F'
eqt'(pending', a') → F'
eqt'(pending', excl') → F'
eqt'(pending', false') → F'
eqt'(pending', lock') → F'
eqt'(pending', locker') → F'
eqt'(pending', mcrlrecord') → F'
eqt'(pending', ok') → F'
eqt'(pending', pending') → T'
eqt'(pending', release') → F'
eqt'(pending', request') → F'
eqt'(pending', resource') → F'
eqt'(pending', tag') → F'
eqt'(pending', true') → F'
eqt'(pending', undefined') → F'
eqt'(pending', pid'(N2)) → F'
eqt'(pending', int'(N2)) → F'
eqt'(pending', cons'(H2, T2)) → F'
eqt'(pending', tuple'(H2, T2)) → F'
eqt'(pending', tuplenil'(H2)) → F'
eqt'(release', nil') → F'
eqt'(release', a') → F'
eqt'(release', excl') → F'
eqt'(release', false') → F'
eqt'(release', lock') → F'
eqt'(release', locker') → F'
eqt'(release', mcrlrecord') → F'
eqt'(release', ok') → F'
eqt'(request', mcrlrecord') → F'
eqt'(request', ok') → F'
eqt'(request', pending') → F'
eqt'(request', release') → F'
eqt'(request', request') → T'
eqt'(request', resource') → F'
eqt'(request', tag') → F'
eqt'(request', true') → F'
eqt'(request', undefined') → F'
eqt'(request', pid'(N2)) → F'
eqt'(request', int'(N2)) → F'
eqt'(request', cons'(H2, T2)) → F'
eqt'(request', tuple'(H2, T2)) → F'
eqt'(request', tuplenil'(H2)) → F'
eqt'(resource', nil') → F'
eqt'(resource', a') → F'
eqt'(resource', excl') → F'
eqt'(resource', false') → F'
eqt'(resource', lock') → F'
eqt'(resource', locker') → F'
eqt'(resource', mcrlrecord') → F'
eqt'(resource', ok') → F'
eqt'(resource', pending') → F'
eqt'(resource', release') → F'
eqt'(resource', request') → F'
eqt'(resource', resource') → T'
eqt'(resource', tag') → F'
eqt'(resource', true') → F'
eqt'(resource', undefined') → F'
eqt'(resource', pid'(N2)) → F'
eqt'(resource', int'(N2)) → F'
eqt'(resource', cons'(H2, T2)) → F'
eqt'(resource', tuple'(H2, T2)) → F'
eqt'(resource', tuplenil'(H2)) → F'
eqt'(tag', nil') → F'
eqt'(tag', a') → F'
eqt'(tag', excl') → F'
eqt'(tag', false') → F'
eqt'(tag', lock') → F'
eqt'(tag', locker') → F'
eqt'(tag', mcrlrecord') → F'
eqt'(tag', ok') → F'
eqt'(tag', pending') → F'
eqt'(tag', release') → F'
eqt'(tag', request') → F'
eqt'(tag', resource') → F'
eqt'(tag', tag') → T'
eqt'(tag', true') → F'
eqt'(tag', undefined') → F'
eqt'(tag', pid'(N2)) → F'
eqt'(tag', int'(N2)) → F'
eqt'(tag', cons'(H2, T2)) → F'
eqt'(tag', tuple'(H2, T2)) → F'
eqt'(tag', tuplenil'(H2)) → F'
eqt'(true', nil') → F'
eqt'(true', a') → F'
eqt'(true', excl') → F'
eqt'(true', false') → F'
eqt'(true', lock') → F'
eqt'(true', locker') → F'
eqt'(true', mcrlrecord') → F'
eqt'(true', ok') → F'
eqt'(true', pending') → F'
eqt'(true', release') → F'
eqt'(true', request') → F'
eqt'(true', resource') → F'
eqt'(true', tag') → F'
eqt'(true', true') → T'
eqt'(true', undefined') → F'
eqt'(true', pid'(N2)) → F'
eqt'(true', int'(N2)) → F'
eqt'(true', cons'(H2, T2)) → F'
eqt'(true', tuple'(H2, T2)) → F'
eqt'(true', tuplenil'(H2)) → F'
eqt'(undefined', nil') → F'
eqt'(undefined', a') → F'
eqt'(undefined', tuplenil'(H2)) → F'
eqt'(pid'(N1), nil') → F'
eqt'(pid'(N1), a') → F'
eqt'(pid'(N1), excl') → F'
eqt'(pid'(N1), false') → F'
eqt'(pid'(N1), lock') → F'
eqt'(pid'(N1), locker') → F'
eqt'(pid'(N1), mcrlrecord') → F'
eqt'(pid'(N1), ok') → F'
eqt'(pid'(N1), pending') → F'
eqt'(pid'(N1), release') → F'
eqt'(pid'(N1), request') → F'
eqt'(pid'(N1), resource') → F'
eqt'(pid'(N1), tag') → F'
eqt'(pid'(N1), true') → F'
eqt'(pid'(N1), undefined') → F'
eqt'(pid'(N1), pid'(N2)) → eqt'(N1, N2)
eqt'(pid'(N1), int'(N2)) → F'
eqt'(pid'(N1), cons'(H2, T2)) → F'
eqt'(pid'(N1), tuple'(H2, T2)) → F'
eqt'(pid'(N1), tuplenil'(H2)) → F'
eqt'(int'(N1), nil') → F'
eqt'(int'(N1), a') → F'
eqt'(int'(N1), excl') → F'
eqt'(int'(N1), false') → F'
eqt'(int'(N1), lock') → F'
eqt'(int'(N1), locker') → F'
eqt'(int'(N1), mcrlrecord') → F'
eqt'(int'(N1), ok') → F'
eqt'(int'(N1), pending') → F'
eqt'(int'(N1), release') → F'
eqt'(int'(N1), request') → F'
eqt'(int'(N1), resource') → F'
eqt'(int'(N1), tag') → F'
eqt'(int'(N1), true') → F'
eqt'(int'(N1), undefined') → F'
eqt'(cons'(H1, T1), resource') → F'
eqt'(cons'(H1, T1), tag') → F'
eqt'(cons'(H1, T1), true') → F'
eqt'(cons'(H1, T1), undefined') → F'
eqt'(cons'(H1, T1), pid'(N2)) → F'
eqt'(cons'(H1, T1), int'(N2)) → F'
eqt'(cons'(H1, T1), cons'(H2, T2)) → and'(eqt'(H1, H2), eqt'(T1, T2))
eqt'(cons'(H1, T1), tuple'(H2, T2)) → F'
eqt'(cons'(H1, T1), tuplenil'(H2)) → F'
eqt'(tuple'(H1, T1), nil') → F'
eqt'(tuple'(H1, T1), a') → F'
eqt'(tuple'(H1, T1), excl') → F'
eqt'(tuple'(H1, T1), false') → F'
eqt'(tuple'(H1, T1), lock') → F'
eqt'(tuple'(H1, T1), locker') → F'
eqt'(tuple'(H1, T1), mcrlrecord') → F'
eqt'(tuple'(H1, T1), ok') → F'
eqt'(tuple'(H1, T1), pending') → F'
eqt'(tuple'(H1, T1), release') → F'
eqt'(tuple'(H1, T1), request') → F'
eqt'(tuple'(H1, T1), resource') → F'
eqt'(tuple'(H1, T1), tag') → F'
eqt'(tuple'(H1, T1), true') → F'
eqt'(tuple'(H1, T1), undefined') → F'
eqt'(tuple'(H1, T1), pid'(N2)) → F'
eqt'(tuple'(H1, T1), int'(N2)) → F'
eqt'(tuple'(H1, T1), cons'(H2, T2)) → F'
eqt'(tuple'(H1, T1), tuple'(H2, T2)) → and'(eqt'(H1, H2), eqt'(T1, T2))
eqt'(tuple'(H1, T1), tuplenil'(H2)) → F'
eqt'(tuplenil'(H1), nil') → F'
eqt'(tuplenil'(H1), a') → F'
eqt'(tuplenil'(H1), excl') → F'
eqt'(tuplenil'(H1), false') → F'
eqt'(tuplenil'(H1), lock') → F'
eqt'(tuplenil'(H1), locker') → F'
eqt'(tuplenil'(H1), mcrlrecord') → F'
eqt'(tuplenil'(H1), ok') → F'
eqt'(tuplenil'(H1), pending') → F'
eqt'(tuplenil'(H1), release') → F'
eqt'(tuplenil'(H1), request') → F'
eqt'(tuplenil'(H1), resource') → F'
eqt'(tuplenil'(H1), tag') → F'
eqt'(tuplenil'(H1), true') → F'
eqt'(tuplenil'(H1), undefined') → F'
eqt'(tuplenil'(H1), pid'(N2)) → F'
eqt'(tuplenil'(H1), int'(N2)) → F'
eqt'(tuplenil'(H1), cons'(H2, T2)) → F'
eqt'(tuplenil'(H1), tuple'(H2, T2)) → F'
eqt'(tuplenil'(H1), tuplenil'(H2)) → eqt'(H1, H2)
element'(int'(s'(0')), tuplenil'(T1)) → T1
element'(int'(s'(0')), tuple'(T1, T2)) → T1
element'(int'(s'(s'(N1))), tuple'(T1, T2)) → element'(int'(s'(N1)), T2)
record_new'(lock') → tuple'(mcrlrecord', tuple'(lock', tuple'(undefined', tuple'(nil', tuplenil'(nil')))))
record_extract'(tuple'(mcrlrecord', tuple'(lock', tuple'(F0, tuple'(F1, tuplenil'(F2))))), lock', resource') → tuple'(mcrlrecord', tuple'(lock', tuple'(F0, tuple'(F1, tuplenil'(F2)))))
record_update'(tuple'(mcrlrecord', tuple'(lock', tuple'(F0, tuple'(F1, tuplenil'(F2))))), lock', pending', NewF) → tuple'(mcrlrecord', tuple'(lock', tuple'(F0, tuple'(F1, tuplenil'(NewF)))))
record_updates'(Record, Name, nil') → Record
record_updates'(Record, Name, cons'(tuple'(Field, tuplenil'(NewF)), Fields)) → record_updates'(record_update'(Record, Name, Field, NewF), Name, Fields)
locker2_map_promote_pending'(nil', Pending) → nil'
locker2_map_promote_pending'(cons'(Lock, Locks), Pending) → cons'(locker2_promote_pending'(Lock, Pending), locker2_map_promote_pending'(Locks, Pending))
locker2_map_claim_lock'(nil') → nil'
locker2_map_claim_lock'(cons'(Lock, Locks)) → cons'(locker2_claim_lock', locker2_map_claim_lock'(Locks))
locker2_map_add_pending'(nil') → nil'
locker2_promote_pending'(Lock, Client) → case0'(Client, Lock, record_extract'(Lock, lock', pending'))
case0'(Client, Lock, cons'(Client, Pendings)) → record_updates'(Lock, lock', cons'(tuple'(excl', tuplenil'(Client)), cons'(tuple'(pending', tuplenil'(Pendings)), nil')))
case0'(Client, Lock, MCRLFree0) → Lock
locker2_remove_pending'(Lock, Client) → record_updates'(Lock, lock', cons'(tuple'(pending', tuplenil'(subtract'(record_extract'(Lock, lock', pending'), cons'(Client, nil')))), nil'))
locker2_add_pending'(Lock, Resources) → case1'(Lock, member'(record_extract'(Lock, lock', resource'), Resources))
case1'(Lock, true') → record_updates'(Lock, lock', cons'(tuple'(pending', tuplenil'(append'(record_extract'(Lock, lock', pending')))), nil'))
case1'(Lock, false') → Lock
locker2_release_lock'(Lock, Client) → case2'(Lock, gen_modtageq'(Client, record_extract'(Lock, lock', excl')))
case2'(Lock, true') → record_updates'(Lock, lock', cons'(tuple'(excllock', excl'), nil'))
case4' → false'
locker2_obtainables'(nil', Client) → true'
locker2_obtainables'(cons'(Lock, Locks), Client) → case5'(Client, Locks, member'(Client, record_extract'(Lock, lock', pending')))
case5'(Client, Locks, true') → andt'(locker2_obtainable', locker2_obtainables'(Locks, Client))
case5'(Client, Locks, 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)) → cons'(Head, append'(Tail))
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, E, equal'(E, Head))
case9'(Tail, E, true') → true'
case9'(Tail, E, false') → member'(E, Tail)
eqs'(empty', empty') → T'
eqs'(empty', stack'(E2, S2)) → F'
eqs'(stack'(E1, S1), empty') → F'
eqs'(stack'(E1, S1), stack'(E2, S2)) → and'(eqt'(E1, E2), eqs'(S1, S2))
pushs'(E1, S1) → stack'(E1, S1)
pops'(stack'(E1, S1)) → S1
tops'(stack'(E1, S1)) → E1
istops'(E1, empty') → F'
istops'(E1, stack'(E2, S1)) → eqt'(E1, E2)
eqc'(nocalls', nocalls') → T'
eqc'(nocalls', calls'(E2, S2, CS2)) → F'
eqc'(calls'(E1, S1, CS1), nocalls') → F'
eqc'(calls'(E1, S1, CS1), calls'(E2, S2, CS2)) → and'(eqt'(E1, E2), and'(eqs'(S1, S2), eqc'(CS1, CS2)))
push'(E1, E2, nocalls') → calls'(E1, stack'(E2, empty'), nocalls')
push'(E1, E2, calls'(E3, S1, CS1)) → push1'(E2, E3, S1, CS1, eqt'(E1, E3))
push1'(E2, E3, S1, CS1, T') → calls'(E3, pushs'(E2, S1), CS1)
Infered types.
Rules:
or'(T', T') → T'
or'(F', T') → T'
or'(T', F') → T'
or'(F', F') → F'
and'(T', B) → B
and'(B, T') → B
and'(F', B) → F'
and'(B, F') → F'
imp'(T', B) → B
imp'(F', B) → T'
not'(T') → F'
not'(F') → T'
if'(T', B1, B2) → B1
if'(F', B1, B2) → B2
eq'(T', T') → T'
eq'(F', F') → T'
eq'(T', F') → F'
eq'(F', T') → F'
eqt'(nil', undefined') → F'
eqt'(nil', pid'(N2)) → F'
eqt'(nil', int'(N2)) → F'
eqt'(nil', cons'(H2, T2)) → F'
eqt'(nil', tuple'(H2, T2)) → F'
eqt'(nil', tuplenil'(H2)) → F'
eqt'(a', nil') → F'
eqt'(a', a') → T'
eqt'(a', excl') → F'
eqt'(a', false') → F'
eqt'(a', lock') → F'
eqt'(a', locker') → F'
eqt'(a', mcrlrecord') → F'
eqt'(a', ok') → F'
eqt'(a', pending') → F'
eqt'(a', release') → F'
eqt'(a', request') → F'
eqt'(a', resource') → F'
eqt'(a', tag') → F'
eqt'(a', true') → F'
eqt'(a', undefined') → F'
eqt'(a', pid'(N2)) → F'
eqt'(a', int'(N2)) → F'
eqt'(a', cons'(H2, T2)) → F'
eqt'(a', tuple'(H2, T2)) → F'
eqt'(a', tuplenil'(H2)) → F'
eqt'(excl', nil') → F'
eqt'(excl', a') → F'
eqt'(excl', excl') → T'
eqt'(excl', false') → F'
eqt'(excl', lock') → F'
eqt'(excl', locker') → F'
eqt'(excl', mcrlrecord') → F'
eqt'(excl', ok') → F'
eqt'(excl', pending') → F'
eqt'(excl', release') → F'
eqt'(excl', request') → F'
eqt'(excl', resource') → F'
eqt'(excl', tag') → F'
eqt'(excl', true') → F'
eqt'(excl', undefined') → F'
eqt'(excl', pid'(N2)) → F'
eqt'(excl', eqt'(false', int'(N2))) → F'
eqt'(false', cons'(H2, T2)) → F'
eqt'(false', tuple'(H2, T2)) → F'
eqt'(false', tuplenil'(H2)) → F'
eqt'(lock', nil') → F'
eqt'(lock', a') → F'
eqt'(lock', excl') → F'
eqt'(lock', false') → F'
eqt'(lock', lock') → T'
eqt'(lock', locker') → F'
eqt'(lock', mcrlrecord') → F'
eqt'(lock', ok') → F'
eqt'(lock', pending') → F'
eqt'(lock', release') → F'
eqt'(lock', request') → F'
eqt'(lock', resource') → F'
eqt'(lock', tag') → F'
eqt'(lock', true') → F'
eqt'(lock', undefined') → F'
eqt'(lock', pid'(N2)) → F'
eqt'(lock', int'(N2)) → F'
eqt'(lock', cons'(H2, T2)) → F'
eqt'(lock', tuple'(H2, T2)) → F'
eqt'(lock', tuplenil'(H2)) → F'
eqt'(locker', nil') → F'
eqt'(locker', a') → F'
eqt'(locker', excl') → F'
eqt'(locker', false') → F'
eqt'(locker', lock') → F'
eqt'(locker', locker') → T'
eqt'(locker', mcrlrecord') → F'
eqt'(locker', ok') → F'
eqt'(locker', pending') → F'
eqt'(locker', release') → F'
eqt'(locker', request') → F'
eqt'(locker', resource') → F'
eqt'(locker', tag') → F'
eqt'(locker', true') → F'
eqt'(locker', undefined') → F'
eqt'(locker', pid'(N2)) → F'
eqt'(locker', int'(N2)) → F'
eqt'(locker', cons'(H2, T2)) → F'
eqt'(locker', tuple'(H2, T2)) → F'
eqt'(locker', tuplenil'(H2)) → F'
eqt'(mcrlrecord', nil') → F'
eqt'(mcrlrecord', a') → F'
eqt'(mcrlrecord', excl') → F'
eqt'(mcrlrecord', false') → F'
eqt'(mcrlrecord', lock') → F'
eqt'(mcrlrecord', locker') → F'
eqt'(mcrlrecord', mcrlrecord') → T'
eqt'(mcrlrecord', ok') → F'
eqt'(mcrlrecord', pending') → F'
eqt'(mcrlrecord', release') → F'
eqt'(mcrlrecord', request') → F'
eqt'(mcrlrecord', resource') → F'
eqt'(ok', resource') → F'
eqt'(ok', tag') → F'
eqt'(ok', true') → F'
eqt'(ok', undefined') → F'
eqt'(ok', pid'(N2)) → F'
eqt'(ok', int'(N2)) → F'
eqt'(ok', cons'(H2, T2)) → F'
eqt'(ok', tuple'(H2, T2)) → F'
eqt'(ok', tuplenil'(H2)) → F'
eqt'(pending', nil') → F'
eqt'(pending', a') → F'
eqt'(pending', excl') → F'
eqt'(pending', false') → F'
eqt'(pending', lock') → F'
eqt'(pending', locker') → F'
eqt'(pending', mcrlrecord') → F'
eqt'(pending', ok') → F'
eqt'(pending', pending') → T'
eqt'(pending', release') → F'
eqt'(pending', request') → F'
eqt'(pending', resource') → F'
eqt'(pending', tag') → F'
eqt'(pending', true') → F'
eqt'(pending', undefined') → F'
eqt'(pending', pid'(N2)) → F'
eqt'(pending', int'(N2)) → F'
eqt'(pending', cons'(H2, T2)) → F'
eqt'(pending', tuple'(H2, T2)) → F'
eqt'(pending', tuplenil'(H2)) → F'
eqt'(release', nil') → F'
eqt'(release', a') → F'
eqt'(release', excl') → F'
eqt'(release', false') → F'
eqt'(release', lock') → F'
eqt'(release', locker') → F'
eqt'(release', mcrlrecord') → F'
eqt'(release', ok') → F'
eqt'(request', mcrlrecord') → F'
eqt'(request', ok') → F'
eqt'(request', pending') → F'
eqt'(request', release') → F'
eqt'(request', request') → T'
eqt'(request', resource') → F'
eqt'(request', tag') → F'
eqt'(request', true') → F'
eqt'(request', undefined') → F'
eqt'(request', pid'(N2)) → F'
eqt'(request', int'(N2)) → F'
eqt'(request', cons'(H2, T2)) → F'
eqt'(request', tuple'(H2, T2)) → F'
eqt'(request', tuplenil'(H2)) → F'
eqt'(resource', nil') → F'
eqt'(resource', a') → F'
eqt'(resource', excl') → F'
eqt'(resource', false') → F'
eqt'(resource', lock') → F'
eqt'(resource', locker') → F'
eqt'(resource', mcrlrecord') → F'
eqt'(resource', ok') → F'
eqt'(resource', pending') → F'
eqt'(resource', release') → F'
eqt'(resource', request') → F'
eqt'(resource', resource') → T'
eqt'(resource', tag') → F'
eqt'(resource', true') → F'
eqt'(resource', undefined') → F'
eqt'(resource', pid'(N2)) → F'
eqt'(resource', int'(N2)) → F'
eqt'(resource', cons'(H2, T2)) → F'
eqt'(resource', tuple'(H2, T2)) → F'
eqt'(resource', tuplenil'(H2)) → F'
eqt'(tag', nil') → F'
eqt'(tag', a') → F'
eqt'(tag', excl') → F'
eqt'(tag', false') → F'
eqt'(tag', lock') → F'
eqt'(tag', locker') → F'
eqt'(tag', mcrlrecord') → F'
eqt'(tag', ok') → F'
eqt'(tag', pending') → F'
eqt'(tag', release') → F'
eqt'(tag', request') → F'
eqt'(tag', resource') → F'
eqt'(tag', tag') → T'
eqt'(tag', true') → F'
eqt'(tag', undefined') → F'
eqt'(tag', pid'(N2)) → F'
eqt'(tag', int'(N2)) → F'
eqt'(tag', cons'(H2, T2)) → F'
eqt'(tag', tuple'(H2, T2)) → F'
eqt'(tag', tuplenil'(H2)) → F'
eqt'(true', nil') → F'
eqt'(true', a') → F'
eqt'(true', excl') → F'
eqt'(true', false') → F'
eqt'(true', lock') → F'
eqt'(true', locker') → F'
eqt'(true', mcrlrecord') → F'
eqt'(true', ok') → F'
eqt'(true', pending') → F'
eqt'(true', release') → F'
eqt'(true', request') → F'
eqt'(true', resource') → F'
eqt'(true', tag') → F'
eqt'(true', true') → T'
eqt'(true', undefined') → F'
eqt'(true', pid'(N2)) → F'
eqt'(true', int'(N2)) → F'
eqt'(true', cons'(H2, T2)) → F'
eqt'(true', tuple'(H2, T2)) → F'
eqt'(true', tuplenil'(H2)) → F'
eqt'(undefined', nil') → F'
eqt'(undefined', a') → F'
eqt'(undefined', tuplenil'(H2)) → F'
eqt'(pid'(N1), nil') → F'
eqt'(pid'(N1), a') → F'
eqt'(pid'(N1), excl') → F'
eqt'(pid'(N1), false') → F'
eqt'(pid'(N1), lock') → F'
eqt'(pid'(N1), locker') → F'
eqt'(pid'(N1), mcrlrecord') → F'
eqt'(pid'(N1), ok') → F'
eqt'(pid'(N1), pending') → F'
eqt'(pid'(N1), release') → F'
eqt'(pid'(N1), request') → F'
eqt'(pid'(N1), resource') → F'
eqt'(pid'(N1), tag') → F'
eqt'(pid'(N1), true') → F'
eqt'(pid'(N1), undefined') → F'
eqt'(pid'(N1), pid'(N2)) → eqt'(N1, N2)
eqt'(pid'(N1), int'(N2)) → F'
eqt'(pid'(N1), cons'(H2, T2)) → F'
eqt'(pid'(N1), tuple'(H2, T2)) → F'
eqt'(pid'(N1), tuplenil'(H2)) → F'
eqt'(int'(N1), nil') → F'
eqt'(int'(N1), a') → F'
eqt'(int'(N1), excl') → F'
eqt'(int'(N1), false') → F'
eqt'(int'(N1), lock') → F'
eqt'(int'(N1), locker') → F'
eqt'(int'(N1), mcrlrecord') → F'
eqt'(int'(N1), ok') → F'
eqt'(int'(N1), pending') → F'
eqt'(int'(N1), release') → F'
eqt'(int'(N1), request') → F'
eqt'(int'(N1), resource') → F'
eqt'(int'(N1), tag') → F'
eqt'(int'(N1), true') → F'
eqt'(int'(N1), undefined') → F'
eqt'(cons'(H1, T1), resource') → F'
eqt'(cons'(H1, T1), tag') → F'
eqt'(cons'(H1, T1), true') → F'
eqt'(cons'(H1, T1), undefined') → F'
eqt'(cons'(H1, T1), pid'(N2)) → F'
eqt'(cons'(H1, T1), int'(N2)) → F'
eqt'(cons'(H1, T1), cons'(H2, T2)) → and'(eqt'(H1, H2), eqt'(T1, T2))
eqt'(cons'(H1, T1), tuple'(H2, T2)) → F'
eqt'(cons'(H1, T1), tuplenil'(H2)) → F'
eqt'(tuple'(H1, T1), nil') → F'
eqt'(tuple'(H1, T1), a') → F'
eqt'(tuple'(H1, T1), excl') → F'
eqt'(tuple'(H1, T1), false') → F'
eqt'(tuple'(H1, T1), lock') → F'
eqt'(tuple'(H1, T1), locker') → F'
eqt'(tuple'(H1, T1), mcrlrecord') → F'
eqt'(tuple'(H1, T1), ok') → F'
eqt'(tuple'(H1, T1), pending') → F'
eqt'(tuple'(H1, T1), release') → F'
eqt'(tuple'(H1, T1), request') → F'
eqt'(tuple'(H1, T1), resource') → F'
eqt'(tuple'(H1, T1), tag') → F'
eqt'(tuple'(H1, T1), true') → F'
eqt'(tuple'(H1, T1), undefined') → F'
eqt'(tuple'(H1, T1), pid'(N2)) → F'
eqt'(tuple'(H1, T1), int'(N2)) → F'
eqt'(tuple'(H1, T1), cons'(H2, T2)) → F'
eqt'(tuple'(H1, T1), tuple'(H2, T2)) → and'(eqt'(H1, H2), eqt'(T1, T2))
eqt'(tuple'(H1, T1), tuplenil'(H2)) → F'
eqt'(tuplenil'(H1), nil') → F'
eqt'(tuplenil'(H1), a') → F'
eqt'(tuplenil'(H1), excl') → F'
eqt'(tuplenil'(H1), false') → F'
eqt'(tuplenil'(H1), lock') → F'
eqt'(tuplenil'(H1), locker') → F'
eqt'(tuplenil'(H1), mcrlrecord') → F'
eqt'(tuplenil'(H1), ok') → F'
eqt'(tuplenil'(H1), pending') → F'
eqt'(tuplenil'(H1), release') → F'
eqt'(tuplenil'(H1), request') → F'
eqt'(tuplenil'(H1), resource') → F'
eqt'(tuplenil'(H1), tag') → F'
eqt'(tuplenil'(H1), true') → F'
eqt'(tuplenil'(H1), undefined') → F'
eqt'(tuplenil'(H1), pid'(N2)) → F'
eqt'(tuplenil'(H1), int'(N2)) → F'
eqt'(tuplenil'(H1), cons'(H2, T2)) → F'
eqt'(tuplenil'(H1), tuple'(H2, T2)) → F'
eqt'(tuplenil'(H1), tuplenil'(H2)) → eqt'(H1, H2)
element'(int'(s'(0')), tuplenil'(T1)) → T1
element'(int'(s'(0')), tuple'(T1, T2)) → T1
element'(int'(s'(s'(N1))), tuple'(T1, T2)) → element'(int'(s'(N1)), T2)
record_new'(lock') → tuple'(mcrlrecord', tuple'(lock', tuple'(undefined', tuple'(nil', tuplenil'(nil')))))
record_extract'(tuple'(mcrlrecord', tuple'(lock', tuple'(F0, tuple'(F1, tuplenil'(F2))))), lock', resource') → tuple'(mcrlrecord', tuple'(lock', tuple'(F0, tuple'(F1, tuplenil'(F2)))))
record_update'(tuple'(mcrlrecord', tuple'(lock', tuple'(F0, tuple'(F1, tuplenil'(F2))))), lock', pending', NewF) → tuple'(mcrlrecord', tuple'(lock', tuple'(F0, tuple'(F1, tuplenil'(NewF)))))
record_updates'(Record, Name, nil') → Record
record_updates'(Record, Name, cons'(tuple'(Field, tuplenil'(NewF)), Fields)) → record_updates'(record_update'(Record, Name, Field, NewF), Name, Fields)
locker2_map_promote_pending'(nil', Pending) → nil'
locker2_map_promote_pending'(cons'(Lock, Locks), Pending) → cons'(locker2_promote_pending'(Lock, Pending), locker2_map_promote_pending'(Locks, Pending))
locker2_map_claim_lock'(nil') → nil'
locker2_map_claim_lock'(cons'(Lock, Locks)) → cons'(locker2_claim_lock', locker2_map_claim_lock'(Locks))
locker2_map_add_pending'(nil') → nil'
locker2_promote_pending'(Lock, Client) → case0'(Client, Lock, record_extract'(Lock, lock', pending'))
case0'(Client, Lock, cons'(Client, Pendings)) → record_updates'(Lock, lock', cons'(tuple'(excl', tuplenil'(Client)), cons'(tuple'(pending', tuplenil'(Pendings)), nil')))
case0'(Client, Lock, MCRLFree0) → Lock
locker2_remove_pending'(Lock, Client) → record_updates'(Lock, lock', cons'(tuple'(pending', tuplenil'(subtract'(record_extract'(Lock, lock', pending'), cons'(Client, nil')))), nil'))
locker2_add_pending'(Lock, Resources) → case1'(Lock, member'(record_extract'(Lock, lock', resource'), Resources))
case1'(Lock, true') → record_updates'(Lock, lock', cons'(tuple'(pending', tuplenil'(append'(record_extract'(Lock, lock', pending')))), nil'))
case1'(Lock, false') → Lock
locker2_release_lock'(Lock, Client) → case2'(Lock, gen_modtageq'(Client, record_extract'(Lock, lock', excl')))
case2'(Lock, true') → record_updates'(Lock, lock', cons'(tuple'(excllock', excl'), nil'))
case4' → false'
locker2_obtainables'(nil', Client) → true'
locker2_obtainables'(cons'(Lock, Locks), Client) → case5'(Client, Locks, member'(Client, record_extract'(Lock, lock', pending')))
case5'(Client, Locks, true') → andt'(locker2_obtainable', locker2_obtainables'(Locks, Client))
case5'(Client, Locks, 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)) → cons'(Head, append'(Tail))
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, E, equal'(E, Head))
case9'(Tail, E, true') → true'
case9'(Tail, E, false') → member'(E, Tail)
eqs'(empty', empty') → T'
eqs'(empty', stack'(E2, S2)) → F'
eqs'(stack'(E1, S1), empty') → F'
eqs'(stack'(E1, S1), stack'(E2, S2)) → and'(eqt'(E1, E2), eqs'(S1, S2))
pushs'(E1, S1) → stack'(E1, S1)
pops'(stack'(E1, S1)) → S1
tops'(stack'(E1, S1)) → E1
istops'(E1, empty') → F'
istops'(E1, stack'(E2, S1)) → eqt'(E1, E2)
eqc'(nocalls', nocalls') → T'
eqc'(nocalls', calls'(E2, S2, CS2)) → F'
eqc'(calls'(E1, S1, CS1), nocalls') → F'
eqc'(calls'(E1, S1, CS1), calls'(E2, S2, CS2)) → and'(eqt'(E1, E2), and'(eqs'(S1, S2), eqc'(CS1, CS2)))
push'(E1, E2, nocalls') → calls'(E1, stack'(E2, empty'), nocalls')
push'(E1, E2, calls'(E3, S1, CS1)) → push1'(E2, E3, S1, CS1, eqt'(E1, E3))
push1'(E2, E3, S1, CS1, T') → calls'(E3, pushs'(E2, S1), CS1)
Types:
or' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
T' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
F' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
and' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
imp' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
not' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
if' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → if' → if' → if'
eq' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
eqt' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
nil' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
undefined' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
pid' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
int' :: 0':s' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
cons' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
tuple' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
tuplenil' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
a' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
excl' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
false' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
lock' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
locker' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
mcrlrecord' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
ok' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
pending' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
release' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
request' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
resource' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
tag' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
true' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
element' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
s' :: 0':s' → 0':s'
0' :: 0':s'
record_new' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
record_extract' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
record_update' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
record_updates' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
locker2_map_promote_pending' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
locker2_promote_pending' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
locker2_map_claim_lock' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
locker2_claim_lock' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
locker2_map_add_pending' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
case0' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
locker2_remove_pending' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
subtract' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
locker2_add_pending' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
case1' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
member' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
append' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
locker2_release_lock' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
case2' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
gen_modtageq' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
excllock' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
case4' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
locker2_obtainables' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
case5' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
andt' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
locker2_obtainable' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
locker2_check_available' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
case6' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
equal' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
locker2_check_availables' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
locker2_adduniq' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → locker2_adduniq' → locker2_adduniq'
delete' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
case8' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
gen_tag' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
case9' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
eqs' :: empty':stack' → empty':stack' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
empty' :: empty':stack'
stack' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → empty':stack' → empty':stack'
pushs' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → empty':stack' → empty':stack'
pops' :: empty':stack' → empty':stack'
tops' :: empty':stack' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
istops' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → empty':stack' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
eqc' :: nocalls':calls' → nocalls':calls' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
nocalls' :: nocalls':calls'
calls' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → empty':stack' → nocalls':calls' → nocalls':calls'
push' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → nocalls':calls' → nocalls':calls'
push1' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → empty':stack' → nocalls':calls' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → nocalls':calls'
_hole_T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'1 :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
_hole_if'2 :: if'
_hole_0':s'3 :: 0':s'
_hole_locker2_adduniq'4 :: locker2_adduniq'
_hole_empty':stack'5 :: empty':stack'
_hole_nocalls':calls'6 :: nocalls':calls'
_gen_T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'7 :: Nat → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
_gen_0':s'8 :: Nat → 0':s'
_gen_empty':stack'9 :: Nat → empty':stack'
_gen_nocalls':calls'10 :: Nat → nocalls':calls'
Heuristically decided to analyse the following defined symbols:
eqt', element', record_updates', locker2_map_promote_pending', locker2_map_claim_lock', subtract', member', append', locker2_obtainables', locker2_check_available', locker2_check_availables', delete', eqs', eqc'
They will be analysed ascendingly in the following order:
eqt' < eqs'
eqt' < eqc'
delete' < subtract'
member' < locker2_obtainables'
locker2_check_available' < locker2_check_availables'
eqs' < eqc'
Rules:
or'(T', T') → T'
or'(F', T') → T'
or'(T', F') → T'
or'(F', F') → F'
and'(T', B) → B
and'(B, T') → B
and'(F', B) → F'
and'(B, F') → F'
imp'(T', B) → B
imp'(F', B) → T'
not'(T') → F'
not'(F') → T'
if'(T', B1, B2) → B1
if'(F', B1, B2) → B2
eq'(T', T') → T'
eq'(F', F') → T'
eq'(T', F') → F'
eq'(F', T') → F'
eqt'(nil', undefined') → F'
eqt'(nil', pid'(N2)) → F'
eqt'(nil', int'(N2)) → F'
eqt'(nil', cons'(H2, T2)) → F'
eqt'(nil', tuple'(H2, T2)) → F'
eqt'(nil', tuplenil'(H2)) → F'
eqt'(a', nil') → F'
eqt'(a', a') → T'
eqt'(a', excl') → F'
eqt'(a', false') → F'
eqt'(a', lock') → F'
eqt'(a', locker') → F'
eqt'(a', mcrlrecord') → F'
eqt'(a', ok') → F'
eqt'(a', pending') → F'
eqt'(a', release') → F'
eqt'(a', request') → F'
eqt'(a', resource') → F'
eqt'(a', tag') → F'
eqt'(a', true') → F'
eqt'(a', undefined') → F'
eqt'(a', pid'(N2)) → F'
eqt'(a', int'(N2)) → F'
eqt'(a', cons'(H2, T2)) → F'
eqt'(a', tuple'(H2, T2)) → F'
eqt'(a', tuplenil'(H2)) → F'
eqt'(excl', nil') → F'
eqt'(excl', a') → F'
eqt'(excl', excl') → T'
eqt'(excl', false') → F'
eqt'(excl', lock') → F'
eqt'(excl', locker') → F'
eqt'(excl', mcrlrecord') → F'
eqt'(excl', ok') → F'
eqt'(excl', pending') → F'
eqt'(excl', release') → F'
eqt'(excl', request') → F'
eqt'(excl', resource') → F'
eqt'(excl', tag') → F'
eqt'(excl', true') → F'
eqt'(excl', undefined') → F'
eqt'(excl', pid'(N2)) → F'
eqt'(excl', eqt'(false', int'(N2))) → F'
eqt'(false', cons'(H2, T2)) → F'
eqt'(false', tuple'(H2, T2)) → F'
eqt'(false', tuplenil'(H2)) → F'
eqt'(lock', nil') → F'
eqt'(lock', a') → F'
eqt'(lock', excl') → F'
eqt'(lock', false') → F'
eqt'(lock', lock') → T'
eqt'(lock', locker') → F'
eqt'(lock', mcrlrecord') → F'
eqt'(lock', ok') → F'
eqt'(lock', pending') → F'
eqt'(lock', release') → F'
eqt'(lock', request') → F'
eqt'(lock', resource') → F'
eqt'(lock', tag') → F'
eqt'(lock', true') → F'
eqt'(lock', undefined') → F'
eqt'(lock', pid'(N2)) → F'
eqt'(lock', int'(N2)) → F'
eqt'(lock', cons'(H2, T2)) → F'
eqt'(lock', tuple'(H2, T2)) → F'
eqt'(lock', tuplenil'(H2)) → F'
eqt'(locker', nil') → F'
eqt'(locker', a') → F'
eqt'(locker', excl') → F'
eqt'(locker', false') → F'
eqt'(locker', lock') → F'
eqt'(locker', locker') → T'
eqt'(locker', mcrlrecord') → F'
eqt'(locker', ok') → F'
eqt'(locker', pending') → F'
eqt'(locker', release') → F'
eqt'(locker', request') → F'
eqt'(locker', resource') → F'
eqt'(locker', tag') → F'
eqt'(locker', true') → F'
eqt'(locker', undefined') → F'
eqt'(locker', pid'(N2)) → F'
eqt'(locker', int'(N2)) → F'
eqt'(locker', cons'(H2, T2)) → F'
eqt'(locker', tuple'(H2, T2)) → F'
eqt'(locker', tuplenil'(H2)) → F'
eqt'(mcrlrecord', nil') → F'
eqt'(mcrlrecord', a') → F'
eqt'(mcrlrecord', excl') → F'
eqt'(mcrlrecord', false') → F'
eqt'(mcrlrecord', lock') → F'
eqt'(mcrlrecord', locker') → F'
eqt'(mcrlrecord', mcrlrecord') → T'
eqt'(mcrlrecord', ok') → F'
eqt'(mcrlrecord', pending') → F'
eqt'(mcrlrecord', release') → F'
eqt'(mcrlrecord', request') → F'
eqt'(mcrlrecord', resource') → F'
eqt'(ok', resource') → F'
eqt'(ok', tag') → F'
eqt'(ok', true') → F'
eqt'(ok', undefined') → F'
eqt'(ok', pid'(N2)) → F'
eqt'(ok', int'(N2)) → F'
eqt'(ok', cons'(H2, T2)) → F'
eqt'(ok', tuple'(H2, T2)) → F'
eqt'(ok', tuplenil'(H2)) → F'
eqt'(pending', nil') → F'
eqt'(pending', a') → F'
eqt'(pending', excl') → F'
eqt'(pending', false') → F'
eqt'(pending', lock') → F'
eqt'(pending', locker') → F'
eqt'(pending', mcrlrecord') → F'
eqt'(pending', ok') → F'
eqt'(pending', pending') → T'
eqt'(pending', release') → F'
eqt'(pending', request') → F'
eqt'(pending', resource') → F'
eqt'(pending', tag') → F'
eqt'(pending', true') → F'
eqt'(pending', undefined') → F'
eqt'(pending', pid'(N2)) → F'
eqt'(pending', int'(N2)) → F'
eqt'(pending', cons'(H2, T2)) → F'
eqt'(pending', tuple'(H2, T2)) → F'
eqt'(pending', tuplenil'(H2)) → F'
eqt'(release', nil') → F'
eqt'(release', a') → F'
eqt'(release', excl') → F'
eqt'(release', false') → F'
eqt'(release', lock') → F'
eqt'(release', locker') → F'
eqt'(release', mcrlrecord') → F'
eqt'(release', ok') → F'
eqt'(request', mcrlrecord') → F'
eqt'(request', ok') → F'
eqt'(request', pending') → F'
eqt'(request', release') → F'
eqt'(request', request') → T'
eqt'(request', resource') → F'
eqt'(request', tag') → F'
eqt'(request', true') → F'
eqt'(request', undefined') → F'
eqt'(request', pid'(N2)) → F'
eqt'(request', int'(N2)) → F'
eqt'(request', cons'(H2, T2)) → F'
eqt'(request', tuple'(H2, T2)) → F'
eqt'(request', tuplenil'(H2)) → F'
eqt'(resource', nil') → F'
eqt'(resource', a') → F'
eqt'(resource', excl') → F'
eqt'(resource', false') → F'
eqt'(resource', lock') → F'
eqt'(resource', locker') → F'
eqt'(resource', mcrlrecord') → F'
eqt'(resource', ok') → F'
eqt'(resource', pending') → F'
eqt'(resource', release') → F'
eqt'(resource', request') → F'
eqt'(resource', resource') → T'
eqt'(resource', tag') → F'
eqt'(resource', true') → F'
eqt'(resource', undefined') → F'
eqt'(resource', pid'(N2)) → F'
eqt'(resource', int'(N2)) → F'
eqt'(resource', cons'(H2, T2)) → F'
eqt'(resource', tuple'(H2, T2)) → F'
eqt'(resource', tuplenil'(H2)) → F'
eqt'(tag', nil') → F'
eqt'(tag', a') → F'
eqt'(tag', excl') → F'
eqt'(tag', false') → F'
eqt'(tag', lock') → F'
eqt'(tag', locker') → F'
eqt'(tag', mcrlrecord') → F'
eqt'(tag', ok') → F'
eqt'(tag', pending') → F'
eqt'(tag', release') → F'
eqt'(tag', request') → F'
eqt'(tag', resource') → F'
eqt'(tag', tag') → T'
eqt'(tag', true') → F'
eqt'(tag', undefined') → F'
eqt'(tag', pid'(N2)) → F'
eqt'(tag', int'(N2)) → F'
eqt'(tag', cons'(H2, T2)) → F'
eqt'(tag', tuple'(H2, T2)) → F'
eqt'(tag', tuplenil'(H2)) → F'
eqt'(true', nil') → F'
eqt'(true', a') → F'
eqt'(true', excl') → F'
eqt'(true', false') → F'
eqt'(true', lock') → F'
eqt'(true', locker') → F'
eqt'(true', mcrlrecord') → F'
eqt'(true', ok') → F'
eqt'(true', pending') → F'
eqt'(true', release') → F'
eqt'(true', request') → F'
eqt'(true', resource') → F'
eqt'(true', tag') → F'
eqt'(true', true') → T'
eqt'(true', undefined') → F'
eqt'(true', pid'(N2)) → F'
eqt'(true', int'(N2)) → F'
eqt'(true', cons'(H2, T2)) → F'
eqt'(true', tuple'(H2, T2)) → F'
eqt'(true', tuplenil'(H2)) → F'
eqt'(undefined', nil') → F'
eqt'(undefined', a') → F'
eqt'(undefined', tuplenil'(H2)) → F'
eqt'(pid'(N1), nil') → F'
eqt'(pid'(N1), a') → F'
eqt'(pid'(N1), excl') → F'
eqt'(pid'(N1), false') → F'
eqt'(pid'(N1), lock') → F'
eqt'(pid'(N1), locker') → F'
eqt'(pid'(N1), mcrlrecord') → F'
eqt'(pid'(N1), ok') → F'
eqt'(pid'(N1), pending') → F'
eqt'(pid'(N1), release') → F'
eqt'(pid'(N1), request') → F'
eqt'(pid'(N1), resource') → F'
eqt'(pid'(N1), tag') → F'
eqt'(pid'(N1), true') → F'
eqt'(pid'(N1), undefined') → F'
eqt'(pid'(N1), pid'(N2)) → eqt'(N1, N2)
eqt'(pid'(N1), int'(N2)) → F'
eqt'(pid'(N1), cons'(H2, T2)) → F'
eqt'(pid'(N1), tuple'(H2, T2)) → F'
eqt'(pid'(N1), tuplenil'(H2)) → F'
eqt'(int'(N1), nil') → F'
eqt'(int'(N1), a') → F'
eqt'(int'(N1), excl') → F'
eqt'(int'(N1), false') → F'
eqt'(int'(N1), lock') → F'
eqt'(int'(N1), locker') → F'
eqt'(int'(N1), mcrlrecord') → F'
eqt'(int'(N1), ok') → F'
eqt'(int'(N1), pending') → F'
eqt'(int'(N1), release') → F'
eqt'(int'(N1), request') → F'
eqt'(int'(N1), resource') → F'
eqt'(int'(N1), tag') → F'
eqt'(int'(N1), true') → F'
eqt'(int'(N1), undefined') → F'
eqt'(cons'(H1, T1), resource') → F'
eqt'(cons'(H1, T1), tag') → F'
eqt'(cons'(H1, T1), true') → F'
eqt'(cons'(H1, T1), undefined') → F'
eqt'(cons'(H1, T1), pid'(N2)) → F'
eqt'(cons'(H1, T1), int'(N2)) → F'
eqt'(cons'(H1, T1), cons'(H2, T2)) → and'(eqt'(H1, H2), eqt'(T1, T2))
eqt'(cons'(H1, T1), tuple'(H2, T2)) → F'
eqt'(cons'(H1, T1), tuplenil'(H2)) → F'
eqt'(tuple'(H1, T1), nil') → F'
eqt'(tuple'(H1, T1), a') → F'
eqt'(tuple'(H1, T1), excl') → F'
eqt'(tuple'(H1, T1), false') → F'
eqt'(tuple'(H1, T1), lock') → F'
eqt'(tuple'(H1, T1), locker') → F'
eqt'(tuple'(H1, T1), mcrlrecord') → F'
eqt'(tuple'(H1, T1), ok') → F'
eqt'(tuple'(H1, T1), pending') → F'
eqt'(tuple'(H1, T1), release') → F'
eqt'(tuple'(H1, T1), request') → F'
eqt'(tuple'(H1, T1), resource') → F'
eqt'(tuple'(H1, T1), tag') → F'
eqt'(tuple'(H1, T1), true') → F'
eqt'(tuple'(H1, T1), undefined') → F'
eqt'(tuple'(H1, T1), pid'(N2)) → F'
eqt'(tuple'(H1, T1), int'(N2)) → F'
eqt'(tuple'(H1, T1), cons'(H2, T2)) → F'
eqt'(tuple'(H1, T1), tuple'(H2, T2)) → and'(eqt'(H1, H2), eqt'(T1, T2))
eqt'(tuple'(H1, T1), tuplenil'(H2)) → F'
eqt'(tuplenil'(H1), nil') → F'
eqt'(tuplenil'(H1), a') → F'
eqt'(tuplenil'(H1), excl') → F'
eqt'(tuplenil'(H1), false') → F'
eqt'(tuplenil'(H1), lock') → F'
eqt'(tuplenil'(H1), locker') → F'
eqt'(tuplenil'(H1), mcrlrecord') → F'
eqt'(tuplenil'(H1), ok') → F'
eqt'(tuplenil'(H1), pending') → F'
eqt'(tuplenil'(H1), release') → F'
eqt'(tuplenil'(H1), request') → F'
eqt'(tuplenil'(H1), resource') → F'
eqt'(tuplenil'(H1), tag') → F'
eqt'(tuplenil'(H1), true') → F'
eqt'(tuplenil'(H1), undefined') → F'
eqt'(tuplenil'(H1), pid'(N2)) → F'
eqt'(tuplenil'(H1), int'(N2)) → F'
eqt'(tuplenil'(H1), cons'(H2, T2)) → F'
eqt'(tuplenil'(H1), tuple'(H2, T2)) → F'
eqt'(tuplenil'(H1), tuplenil'(H2)) → eqt'(H1, H2)
element'(int'(s'(0')), tuplenil'(T1)) → T1
element'(int'(s'(0')), tuple'(T1, T2)) → T1
element'(int'(s'(s'(N1))), tuple'(T1, T2)) → element'(int'(s'(N1)), T2)
record_new'(lock') → tuple'(mcrlrecord', tuple'(lock', tuple'(undefined', tuple'(nil', tuplenil'(nil')))))
record_extract'(tuple'(mcrlrecord', tuple'(lock', tuple'(F0, tuple'(F1, tuplenil'(F2))))), lock', resource') → tuple'(mcrlrecord', tuple'(lock', tuple'(F0, tuple'(F1, tuplenil'(F2)))))
record_update'(tuple'(mcrlrecord', tuple'(lock', tuple'(F0, tuple'(F1, tuplenil'(F2))))), lock', pending', NewF) → tuple'(mcrlrecord', tuple'(lock', tuple'(F0, tuple'(F1, tuplenil'(NewF)))))
record_updates'(Record, Name, nil') → Record
record_updates'(Record, Name, cons'(tuple'(Field, tuplenil'(NewF)), Fields)) → record_updates'(record_update'(Record, Name, Field, NewF), Name, Fields)
locker2_map_promote_pending'(nil', Pending) → nil'
locker2_map_promote_pending'(cons'(Lock, Locks), Pending) → cons'(locker2_promote_pending'(Lock, Pending), locker2_map_promote_pending'(Locks, Pending))
locker2_map_claim_lock'(nil') → nil'
locker2_map_claim_lock'(cons'(Lock, Locks)) → cons'(locker2_claim_lock', locker2_map_claim_lock'(Locks))
locker2_map_add_pending'(nil') → nil'
locker2_promote_pending'(Lock, Client) → case0'(Client, Lock, record_extract'(Lock, lock', pending'))
case0'(Client, Lock, cons'(Client, Pendings)) → record_updates'(Lock, lock', cons'(tuple'(excl', tuplenil'(Client)), cons'(tuple'(pending', tuplenil'(Pendings)), nil')))
case0'(Client, Lock, MCRLFree0) → Lock
locker2_remove_pending'(Lock, Client) → record_updates'(Lock, lock', cons'(tuple'(pending', tuplenil'(subtract'(record_extract'(Lock, lock', pending'), cons'(Client, nil')))), nil'))
locker2_add_pending'(Lock, Resources) → case1'(Lock, member'(record_extract'(Lock, lock', resource'), Resources))
case1'(Lock, true') → record_updates'(Lock, lock', cons'(tuple'(pending', tuplenil'(append'(record_extract'(Lock, lock', pending')))), nil'))
case1'(Lock, false') → Lock
locker2_release_lock'(Lock, Client) → case2'(Lock, gen_modtageq'(Client, record_extract'(Lock, lock', excl')))
case2'(Lock, true') → record_updates'(Lock, lock', cons'(tuple'(excllock', excl'), nil'))
case4' → false'
locker2_obtainables'(nil', Client) → true'
locker2_obtainables'(cons'(Lock, Locks), Client) → case5'(Client, Locks, member'(Client, record_extract'(Lock, lock', pending')))
case5'(Client, Locks, true') → andt'(locker2_obtainable', locker2_obtainables'(Locks, Client))
case5'(Client, Locks, 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)) → cons'(Head, append'(Tail))
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, E, equal'(E, Head))
case9'(Tail, E, true') → true'
case9'(Tail, E, false') → member'(E, Tail)
eqs'(empty', empty') → T'
eqs'(empty', stack'(E2, S2)) → F'
eqs'(stack'(E1, S1), empty') → F'
eqs'(stack'(E1, S1), stack'(E2, S2)) → and'(eqt'(E1, E2), eqs'(S1, S2))
pushs'(E1, S1) → stack'(E1, S1)
pops'(stack'(E1, S1)) → S1
tops'(stack'(E1, S1)) → E1
istops'(E1, empty') → F'
istops'(E1, stack'(E2, S1)) → eqt'(E1, E2)
eqc'(nocalls', nocalls') → T'
eqc'(nocalls', calls'(E2, S2, CS2)) → F'
eqc'(calls'(E1, S1, CS1), nocalls') → F'
eqc'(calls'(E1, S1, CS1), calls'(E2, S2, CS2)) → and'(eqt'(E1, E2), and'(eqs'(S1, S2), eqc'(CS1, CS2)))
push'(E1, E2, nocalls') → calls'(E1, stack'(E2, empty'), nocalls')
push'(E1, E2, calls'(E3, S1, CS1)) → push1'(E2, E3, S1, CS1, eqt'(E1, E3))
push1'(E2, E3, S1, CS1, T') → calls'(E3, pushs'(E2, S1), CS1)
Types:
or' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
T' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
F' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
and' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
imp' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
not' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
if' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → if' → if' → if'
eq' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
eqt' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
nil' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
undefined' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
pid' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
int' :: 0':s' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
cons' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
tuple' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
tuplenil' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
a' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
excl' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
false' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
lock' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
locker' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
mcrlrecord' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
ok' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
pending' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
release' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
request' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
resource' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
tag' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
true' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
element' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
s' :: 0':s' → 0':s'
0' :: 0':s'
record_new' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
record_extract' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
record_update' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
record_updates' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
locker2_map_promote_pending' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
locker2_promote_pending' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
locker2_map_claim_lock' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
locker2_claim_lock' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
locker2_map_add_pending' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
case0' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
locker2_remove_pending' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
subtract' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
locker2_add_pending' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
case1' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
member' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
append' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
locker2_release_lock' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
case2' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
gen_modtageq' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
excllock' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
case4' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
locker2_obtainables' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
case5' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
andt' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
locker2_obtainable' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
locker2_check_available' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
case6' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
equal' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
locker2_check_availables' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
locker2_adduniq' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → locker2_adduniq' → locker2_adduniq'
delete' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
case8' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
gen_tag' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
case9' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
eqs' :: empty':stack' → empty':stack' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
empty' :: empty':stack'
stack' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → empty':stack' → empty':stack'
pushs' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → empty':stack' → empty':stack'
pops' :: empty':stack' → empty':stack'
tops' :: empty':stack' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
istops' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → empty':stack' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
eqc' :: nocalls':calls' → nocalls':calls' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
nocalls' :: nocalls':calls'
calls' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → empty':stack' → nocalls':calls' → nocalls':calls'
push' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → nocalls':calls' → nocalls':calls'
push1' :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → empty':stack' → nocalls':calls' → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal' → nocalls':calls'
_hole_T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'1 :: T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
_hole_if'2 :: if'
_hole_0':s'3 :: 0':s'
_hole_locker2_adduniq'4 :: locker2_adduniq'
_hole_empty':stack'5 :: empty':stack'
_hole_nocalls':calls'6 :: nocalls':calls'
_gen_T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'7 :: Nat → T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'
_gen_0':s'8 :: Nat → 0':s'
_gen_empty':stack'9 :: Nat → empty':stack'
_gen_nocalls':calls'10 :: Nat → nocalls':calls'
Generator Equations:
_gen_T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'7(0) ⇔ T'
_gen_T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'7(+(x, 1)) ⇔ pid'(_gen_T':F':nil':undefined':pid':int':cons':tuple':tuplenil':a':excl':false':lock':locker':mcrlrecord':ok':pending':release':request':resource':tag':true':locker2_claim_lock':excllock':locker2_obtainable':andt':equal'7(x))
_gen_0':s'8(0) ⇔ 0'
_gen_0':s'8(+(x, 1)) ⇔ s'(_gen_0':s'8(x))
_gen_empty':stack'9(0) ⇔ empty'
_gen_empty':stack'9(+(x, 1)) ⇔ stack'(T', _gen_empty':stack'9(x))
_gen_nocalls':calls'10(0) ⇔ nocalls'
_gen_nocalls':calls'10(+(x, 1)) ⇔ calls'(T', empty', _gen_nocalls':calls'10(x))
The following defined symbols remain to be analysed:
eqt', element', record_updates', locker2_map_promote_pending', locker2_map_claim_lock', subtract', member', append', locker2_obtainables', locker2_check_available', locker2_check_availables', delete', eqs', eqc'
They will be analysed ascendingly in the following order:
eqt' < eqs'
eqt' < eqc'
delete' < subtract'
member' < locker2_obtainables'
locker2_check_available' < locker2_check_availables'
eqs' < eqc'