Termination w.r.t. Q proof of /tmp/tmppaogXw/mucrl1.trs

Termination w.r.t. Q of the given QTRS could be proven:

0 QTRS

↳1 QTRSRRRProof (⇔)

↳2 QTRS

↳3 QTRSRRRProof (⇔)

↳4 QTRS

  ↳5 RisEmptyProof (⇔)

    ↳6 TRUE

  ↳7 RisEmptyProof (⇔)

    ↳8 TRUE

  ↳9 RisEmptyProof (⇔)

    ↳10 TRUE

(0) Obligation:

Q restricted rewrite system:
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)

Q is empty.

(1) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Combined order from the following AFS and order.
or(x1, x2) = or(x1, x2)
T = T
F = F
and(x1, x2) = and(x1, x2)
imp(x1, x2) = imp(x1, x2)
not(x1) = not(x1)
if(x1, x2, x3) = if(x1, x2, x3)
eq(x1, x2) = eq(x1, x2)
eqt(x1, x2) = eqt(x1, x2)
nil = nil
undefined = undefined
pid(x1) = pid(x1)
int(x1) = int(x1)
cons(x1, x2) = cons(x1, x2)
tuple(x1, x2) = tuple(x1, x2)
tuplenil(x1) = x1
a = a
excl = excl
false = false
lock = lock
locker = locker
mcrlrecord = mcrlrecord
ok = ok
pending = pending
release = release
request = request
resource = resource
tag = tag
true = true
element(x1, x2) = element(x1, x2)
s(x1) = s(x1)
0 = 0
record_new(x1) = record_new(x1)
record_extract(x1, x2, x3) = record_extract(x1, x2, x3)
record_update(x1, x2, x3, x4) = record_update(x1, x2, x3, x4)
record_updates(x1, x2, x3) = record_updates(x1, x2, x3)
locker2_map_promote_pending(x1, x2) = locker2_map_promote_pending(x1, x2)
locker2_promote_pending(x1, x2) = locker2_promote_pending(x1, x2)
locker2_map_claim_lock(x1, x2, x3) = locker2_map_claim_lock(x1, x2, x3)
locker2_claim_lock(x1, x2, x3) = locker2_claim_lock(x1, x2, x3)
locker2_map_add_pending(x1, x2, x3) = locker2_map_add_pending(x1, x2, x3)
case0(x1, x2, x3) = case0(x1, x2, x3)
locker2_remove_pending(x1, x2) = locker2_remove_pending(x1, x2)
subtract(x1, x2) = subtract(x1, x2)
locker2_add_pending(x1, x2, x3) = locker2_add_pending(x1, x2, x3)
case1(x1, x2, x3, x4) = case1(x1, x2, x3, x4)
member(x1, x2) = member(x1, x2)
append(x1, x2) = append(x1, x2)
locker2_release_lock(x1, x2) = locker2_release_lock(x1, x2)
case2(x1, x2, x3) = case2(x1, x2, x3)
gen_modtageq(x1, x2) = gen_modtageq(x1, x2)
excllock = excllock
case4(x1, x2, x3) = case4(x1, x2, x3)
locker2_obtainables(x1, x2) = locker2_obtainables(x1, x2)
case5(x1, x2, x3, x4) = case5(x1, x2, x3, x4)
andt(x1, x2) = andt(x1, x2)
locker2_obtainable(x1, x2) = locker2_obtainable(x1, x2)
locker2_check_available(x1, x2) = locker2_check_available(x1, x2)
case6(x1, x2, x3, x4) = case6(x1, x2, x3, x4)
equal(x1, x2) = equal(x1, x2)
locker2_check_availables(x1, x2) = locker2_check_availables(x1, x2)
locker2_adduniq(x1, x2) = locker2_adduniq(x1, x2)
delete(x1, x2) = delete(x1, x2)
case8(x1, x2, x3, x4) = case8(x1, x2, x3, x4)
gen_tag(x1) = gen_tag(x1)
case9(x1, x2, x3, x4) = case9(x1, x2, x3, x4)
eqs(x1, x2) = eqs(x1, x2)
empty = empty
stack(x1, x2) = stack(x1, x2)
pushs(x1, x2) = pushs(x1, x2)
pops(x1) = x1
tops(x1) = x1
istops(x1, x2) = istops(x1, x2)
eqc(x1, x2) = eqc(x1, x2)
nocalls = nocalls
calls(x1, x2, x3) = calls(x1, x2, x3)
push(x1, x2, x3) = push(x1, x2, x3)
push1(x1, x2, x3, x4, x5, x6) = push1(x1, x2, x3, x4, x5, x6)

Recursive path order with status [RPO].
Quasi-Precedence:

or₂ > [F, ok] > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
imp₂ > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
not₁ > [F, ok] > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
if₃ > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
eq₂ > [F, ok] > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
pid₁ > eqt₂ > and₂ > [F, ok] > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
a > [F, ok] > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
locker > [F, ok] > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
release > [F, ok] > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
request > [F, ok] > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
element₂ > [int₁, s₁] > [F, ok] > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
0 > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
record_new₁ > [nil, pending, true, record_updates₃, case1₄] > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
record_new₁ > undefined > [F, ok] > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
record_new₁ > mcrlrecord > [F, ok] > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
[locker2_{map_{promote_pending₂}}, locker2_{promote_pending₂}] > case0₃ > [excl, locker2_{check_available₂}, case6₄] > false > [F, ok] > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
[locker2_{map_{promote_pending₂}}, locker2_{promote_pending₂}] > case0₃ > [excl, locker2_{check_available₂}, case6₄] > false > [delete₂, case8₄] > [nil, pending, true, record_updates₃, case1₄] > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
[locker2_{map_{promote_pending₂}}, locker2_{promote_pending₂}] > case0₃ > [excl, locker2_{check_available₂}, case6₄] > resource > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
[locker2_{map_{promote_pending₂}}, locker2_{promote_pending₂}] > case0₃ > [excl, locker2_{check_available₂}, case6₄] > andt₂ > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
locker2_{map_{claim_lock₃}} > [nil, pending, true, record_updates₃, case1₄] > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
locker2_{map_{claim_lock₃}} > locker2_{claim_lock₃} > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
locker2_{map_{add_pending₃}} > [nil, pending, true, record_updates₃, case1₄] > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
locker2_{remove_pending₂} > subtract₂ > [delete₂, case8₄] > [nil, pending, true, record_updates₃, case1₄] > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
locker2_{add_pending₃} > resource > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
locker2_{add_pending₃} > [member₂, case9₄] > false > [F, ok] > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
locker2_{add_pending₃} > [member₂, case9₄] > false > [delete₂, case8₄] > [nil, pending, true, record_updates₃, case1₄] > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
locker2_{release_lock₂} > case2₃ > [excl, locker2_{check_available₂}, case6₄] > false > [F, ok] > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
locker2_{release_lock₂} > case2₃ > [excl, locker2_{check_available₂}, case6₄] > false > [delete₂, case8₄] > [nil, pending, true, record_updates₃, case1₄] > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
locker2_{release_lock₂} > case2₃ > [excl, locker2_{check_available₂}, case6₄] > resource > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
locker2_{release_lock₂} > case2₃ > [excl, locker2_{check_available₂}, case6₄] > andt₂ > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
locker2_{release_lock₂} > case2₃ > excllock > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
locker2_{release_lock₂} > gen_modtageq₂ > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
case4₃ > false > [F, ok] > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
case4₃ > false > [delete₂, case8₄] > [nil, pending, true, record_updates₃, case1₄] > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
[locker2_{obtainables₂}, case5₄] > [member₂, case9₄] > false > [F, ok] > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
[locker2_{obtainables₂}, case5₄] > [member₂, case9₄] > false > [delete₂, case8₄] > [nil, pending, true, record_updates₃, case1₄] > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
[locker2_{obtainables₂}, case5₄] > andt₂ > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
[locker2_{obtainables₂}, case5₄] > locker2_{obtainable₂} > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
locker2_{check_{availables₂}} > [excl, locker2_{check_available₂}, case6₄] > false > [F, ok] > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
locker2_{check_{availables₂}} > [excl, locker2_{check_available₂}, case6₄] > false > [delete₂, case8₄] > [nil, pending, true, record_updates₃, case1₄] > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
locker2_{check_{availables₂}} > [excl, locker2_{check_available₂}, case6₄] > resource > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
locker2_{check_{availables₂}} > [excl, locker2_{check_available₂}, case6₄] > andt₂ > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
locker2_adduniq₂ > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
gen_tag₁ > tag > [F, ok] > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
[empty, push₃] > [stack₂, pushs₂, push1₆] > eqs₂ > eqt₂ > and₂ > [F, ok] > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
[empty, push₃] > [stack₂, pushs₂, push1₆] > calls₃ > [F, ok] > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
[empty, push₃] > nocalls > calls₃ > [F, ok] > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
istops₂ > eqt₂ > and₂ > [F, ok] > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]
eqc₂ > eqs₂ > eqt₂ > and₂ > [F, ok] > [T, cons₂, tuple₂, lock, record_extract₃, record_update₄, append₂, equal₂]

Status:

eq₂: multiset
case8₄: [1,3,2,4]
push₃: [2,3,1]
delete₂: [2,1]
locker2_{remove_pending₂}: [1,2]
locker2_{map_{promote_pending₂}}: [1,2]
member₂: [1,2]
gen_modtageq₂: multiset
gen_tag₁: [1]
equal₂: multiset
pushs₂: multiset
locker2_{check_available₂}: [2,1]
record_new₁: multiset
excllock: multiset
eqt₂: [2,1]
nil: multiset
element₂: [2,1]
locker2_{release_lock₂}: multiset
locker2_{obtainables₂}: [2,1]
T: multiset
locker2_{add_pending₃}: multiset
resource: multiset
locker: multiset
true: multiset
empty: multiset
eqc₂: [1,2]
push1₆: multiset
locker2_{obtainable₂}: multiset
locker2_{check_{availables₂}}: [2,1]
case2₃: multiset
pid₁: multiset
ok: multiset
F: multiset
lock: multiset
or₂: multiset
calls₃: multiset
eqs₂: [1,2]
and₂: [2,1]
locker2_{claim_lock₃}: multiset
append₂: [1,2]
andt₂: multiset
stack₂: multiset
case6₄: [1,3,4,2]
if₃: multiset
pending: multiset
not₁: multiset
int₁: multiset
istops₂: multiset
locker2_{map_{claim_lock₃}}: [3,2,1]
s₁: multiset
record_update₄: [1,3,2,4]
undefined: multiset
tag: multiset
mcrlrecord: multiset
a: multiset
request: multiset
excl: multiset
subtract₂: [2,1]
record_updates₃: [2,3,1]
locker2_{promote_pending₂}: [1,2]
case4₃: [2,3,1]
nocalls: multiset
case1₄: [4,3,1,2]
0: multiset
cons₂: [1,2]
locker2_{map_{add_pending₃}}: [1,3,2]
case5₄: [1,2,4,3]
record_extract₃: multiset
release: multiset
case0₃: multiset
case9₄: [3,1,2,4]
false: multiset
imp₂: multiset
tuple₂: [1,2]
locker2_adduniq₂: multiset

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

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
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))
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)

(2) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

eqt(tuplenil(H1), tuplenil(H2)) → eqt(H1, H2)
pushs(E1, S1) → stack(E1, S1)

Q is empty.

(3) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(eqt(x₁, x₂)) = x₁ + x₂
POL(pushs(x₁, x₂)) = 1 + x₁ + x₂
POL(stack(x₁, x₂)) = x₁ + x₂
POL(tuplenil(x₁)) = 1 + x₁

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

eqt(tuplenil(H1), tuplenil(H2)) → eqt(H1, H2)
pushs(E1, S1) → stack(E1, S1)

(4) Obligation:

Q restricted rewrite system:
R is empty.
Q is empty.

(5) RisEmptyProof (EQUIVALENT transformation)

The TRS R is empty. Hence, termination is trivially proven.

(6) TRUE

(7) RisEmptyProof (EQUIVALENT transformation)

The TRS R is empty. Hence, termination is trivially proven.

(8) TRUE

(9) RisEmptyProof (EQUIVALENT transformation)

The TRS R is empty. Hence, termination is trivially proven.

(0) Obligation:

(1) QTRSRRRProof (EQUIVALENT transformation)

(2) Obligation:

(3) QTRSRRRProof (EQUIVALENT transformation)

(4) Obligation:

(5) RisEmptyProof (EQUIVALENT transformation)

(6) TRUE

(7) RisEmptyProof (EQUIVALENT transformation)

(8) TRUE

(9) RisEmptyProof (EQUIVALENT transformation)

(10) TRUE