The rewrite relation of the following TRS is considered.
There are 377 ruless (increase limit for explicit display).
| prec(or) | = | 0 | stat(or) | = | lex | |
| prec(T) | = | 7 | stat(T) | = | mul | |
| prec(F) | = | 2 | stat(F) | = | mul | |
| prec(and) | = | 3 | stat(and) | = | mul | |
| prec(imp) | = | 8 | stat(imp) | = | lex | |
| prec(not) | = | 7 | stat(not) | = | lex | |
| prec(if) | = | 9 | stat(if) | = | mul | |
| prec(eq) | = | 10 | stat(eq) | = | lex | |
| prec(eqt) | = | 7 | stat(eqt) | = | mul | |
| prec(nil) | = | 11 | stat(nil) | = | mul | |
| prec(undefined) | = | 12 | stat(undefined) | = | mul | |
| prec(cons) | = | 7 | stat(cons) | = | mul | |
| prec(tuple) | = | 2 | stat(tuple) | = | lex | |
| prec(a) | = | 13 | stat(a) | = | mul | |
| prec(excl) | = | 14 | stat(excl) | = | mul | |
| prec(false) | = | 2 | stat(false) | = | mul | |
| prec(lock) | = | 11 | stat(lock) | = | mul | |
| prec(locker) | = | 15 | stat(locker) | = | mul | |
| prec(mcrlrecord) | = | 12 | stat(mcrlrecord) | = | mul | |
| prec(ok) | = | 16 | stat(ok) | = | mul | |
| prec(pending) | = | 11 | stat(pending) | = | mul | |
| prec(release) | = | 2 | stat(release) | = | mul | |
| prec(request) | = | 7 | stat(request) | = | mul | |
| prec(resource) | = | 11 | stat(resource) | = | mul | |
| prec(tag) | = | 7 | stat(tag) | = | mul | |
| prec(true) | = | 21 | stat(true) | = | mul | |
| prec(element) | = | 22 | stat(element) | = | lex | |
| prec(0) | = | 23 | stat(0) | = | mul | |
| prec(record_new) | = | 12 | stat(record_new) | = | lex | |
| prec(record_extract) | = | 17 | stat(record_extract) | = | lex | |
| prec(record_update) | = | 2 | stat(record_update) | = | lex | |
| prec(record_updates) | = | 4 | stat(record_updates) | = | lex | |
| prec(locker2_map_promote_pending) | = | 26 | stat(locker2_map_promote_pending) | = | mul | |
| prec(locker2_promote_pending) | = | 25 | stat(locker2_promote_pending) | = | mul | |
| prec(locker2_map_claim_lock) | = | 27 | stat(locker2_map_claim_lock) | = | mul | |
| prec(locker2_claim_lock) | = | 27 | stat(locker2_claim_lock) | = | mul | |
| prec(locker2_map_add_pending) | = | 28 | stat(locker2_map_add_pending) | = | mul | |
| prec(case0) | = | 24 | stat(case0) | = | mul | |
| prec(locker2_remove_pending) | = | 29 | stat(locker2_remove_pending) | = | lex | |
| prec(subtract) | = | 11 | stat(subtract) | = | lex | |
| prec(locker2_add_pending) | = | 31 | stat(locker2_add_pending) | = | mul | |
| prec(case1) | = | 30 | stat(case1) | = | mul | |
| prec(member) | = | 2 | stat(member) | = | lex | |
| prec(append) | = | 18 | stat(append) | = | mul | |
| prec(locker2_release_lock) | = | 34 | stat(locker2_release_lock) | = | mul | |
| prec(case2) | = | 32 | stat(case2) | = | lex | |
| prec(gen_modtageq) | = | 33 | stat(gen_modtageq) | = | mul | |
| prec(excllock) | = | 19 | stat(excllock) | = | mul | |
| prec(case4) | = | 35 | stat(case4) | = | lex | |
| prec(locker2_obtainables) | = | 21 | stat(locker2_obtainables) | = | lex | |
| prec(case5) | = | 21 | stat(case5) | = | lex | |
| prec(andt) | = | 5 | stat(andt) | = | mul | |
| prec(locker2_obtainable) | = | 20 | stat(locker2_obtainable) | = | lex | |
| prec(locker2_check_available) | = | 21 | stat(locker2_check_available) | = | lex | |
| prec(case6) | = | 21 | stat(case6) | = | lex | |
| prec(equal) | = | 1 | stat(equal) | = | lex | |
| prec(locker2_check_availables) | = | 21 | stat(locker2_check_availables) | = | lex | |
| prec(locker2_adduniq) | = | 36 | stat(locker2_adduniq) | = | mul | |
| prec(delete) | = | 11 | stat(delete) | = | lex | |
| prec(case8) | = | 11 | stat(case8) | = | lex | |
| prec(gen_tag) | = | 37 | stat(gen_tag) | = | mul | |
| prec(case9) | = | 2 | stat(case9) | = | lex | |
| prec(eqs) | = | 38 | stat(eqs) | = | mul | |
| prec(empty) | = | 39 | stat(empty) | = | mul | |
| prec(stack) | = | 40 | stat(stack) | = | mul | |
| prec(pushs) | = | 40 | stat(pushs) | = | mul | |
| prec(istops) | = | 7 | stat(istops) | = | mul | |
| prec(eqc) | = | 38 | stat(eqc) | = | mul | |
| prec(nocalls) | = | 41 | stat(nocalls) | = | mul | |
| prec(calls) | = | 6 | stat(calls) | = | lex | |
| prec(push) | = | 43 | stat(push) | = | mul | |
| prec(push1) | = | 42 | stat(push1) | = | mul |
| π(or) | = | [2,1] |
| π(T) | = | [] |
| π(F) | = | [] |
| π(and) | = | [1,2] |
| π(imp) | = | [2,1] |
| π(not) | = | [1] |
| π(if) | = | [1,2,3] |
| π(eq) | = | [2,1] |
| π(eqt) | = | [1,2] |
| π(nil) | = | [] |
| π(undefined) | = | [] |
| π(pid) | = | 1 |
| π(int) | = | 1 |
| π(cons) | = | [1,2] |
| π(tuple) | = | [1,2] |
| π(tuplenil) | = | 1 |
| π(a) | = | [] |
| π(excl) | = | [] |
| π(false) | = | [] |
| π(lock) | = | [] |
| π(locker) | = | [] |
| π(mcrlrecord) | = | [] |
| π(ok) | = | [] |
| π(pending) | = | [] |
| π(release) | = | [] |
| π(request) | = | [] |
| π(resource) | = | [] |
| π(tag) | = | [] |
| π(true) | = | [] |
| π(element) | = | [1,2] |
| π(s) | = | 1 |
| π(0) | = | [] |
| π(record_new) | = | [1] |
| π(record_extract) | = | [2,1,3] |
| π(record_update) | = | [1,2,4,3] |
| π(record_updates) | = | [3,1,2] |
| π(locker2_map_promote_pending) | = | [1,2] |
| π(locker2_promote_pending) | = | [1,2] |
| π(locker2_map_claim_lock) | = | [1,2,3] |
| π(locker2_claim_lock) | = | [1,2,3] |
| π(locker2_map_add_pending) | = | [1,2,3] |
| π(case0) | = | [1,2,3] |
| π(locker2_remove_pending) | = | [1,2] |
| π(subtract) | = | [2,1] |
| π(locker2_add_pending) | = | [1,2,3] |
| π(case1) | = | [1,2,3,4] |
| π(member) | = | [2,1] |
| π(append) | = | [1,2] |
| π(locker2_release_lock) | = | [1,2] |
| π(case2) | = | [1,3,2] |
| π(gen_modtageq) | = | [1,2] |
| π(excllock) | = | [] |
| π(case4) | = | [3,2,1] |
| π(locker2_obtainables) | = | [1,2] |
| π(case5) | = | [2,1,4,3] |
| π(andt) | = | [1,2] |
| π(locker2_obtainable) | = | [2,1] |
| π(locker2_check_available) | = | [1,2] |
| π(case6) | = | [3,1,2,4] |
| π(equal) | = | [1,2] |
| π(locker2_check_availables) | = | [1,2] |
| π(locker2_adduniq) | = | [1,2] |
| π(delete) | = | [1,2] |
| π(case8) | = | [3,1,4,2] |
| π(gen_tag) | = | [1] |
| π(case9) | = | [1,3,2,4] |
| π(eqs) | = | [1,2] |
| π(empty) | = | [] |
| π(stack) | = | [1,2] |
| π(pushs) | = | [1,2] |
| π(pops) | = | 1 |
| π(tops) | = | 1 |
| π(istops) | = | [1,2] |
| π(eqc) | = | [1,2] |
| π(nocalls) | = | [] |
| π(calls) | = | [2,1,3] |
| π(push) | = | [1,2,3] |
| π(push1) | = | [1,2,3,4,5,6] |
There are 374 ruless (increase limit for explicit display).
| prec(pid) | = | 1 | weight(pid) | = | 1 | ||||
| prec(tuplenil) | = | 4 | weight(tuplenil) | = | 0 | ||||
| prec(pushs) | = | 3 | weight(pushs) | = | 0 | ||||
| prec(stack) | = | 2 | weight(stack) | = | 0 | ||||
| prec(eqt) | = | 0 | weight(eqt) | = | 0 |
| eqt(pid(N1),pid(N2)) | → | eqt(N1,N2) | (246) |
| eqt(tuplenil(H1),tuplenil(H2)) | → | eqt(H1,H2) | (314) |
| pushs(E1,S1) | → | stack(E1,S1) | (366) |
There are no rules in the TRS. Hence, it is terminating.