; @origtpdbfilename ./TRS/Cime/mucrl1.trs
; @xtcfilename "./TRS_Standard/CiME_04/mucrl1.xml"
(format TRS)
(fun or 2)
(fun T 0)
(fun F 0)
(fun and 2)
(fun imp 2)
(fun not 1)
(fun if 3)
(fun eq 2)
(fun eqt 2)
(fun nil 0)
(fun undefined 0)
(fun pid 1)
(fun int 1)
(fun cons 2)
(fun tuple 2)
(fun tuplenil 1)
(fun a 0)
(fun excl 0)
(fun false 0)
(fun lock 0)
(fun locker 0)
(fun mcrlrecord 0)
(fun ok 0)
(fun pending 0)
(fun release 0)
(fun request 0)
(fun resource 0)
(fun tag 0)
(fun true 0)
(fun element 2)
(fun s 1)
(fun |0| 0)
(fun record_new 1)
(fun record_extract 3)
(fun record_update 4)
(fun record_updates 3)
(fun locker2_map_promote_pending 2)
(fun locker2_promote_pending 2)
(fun locker2_map_claim_lock 3)
(fun locker2_claim_lock 3)
(fun locker2_map_add_pending 3)
(fun case0 3)
(fun locker2_remove_pending 2)
(fun subtract 2)
(fun locker2_add_pending 3)
(fun case1 4)
(fun member 2)
(fun append 2)
(fun locker2_release_lock 2)
(fun case2 3)
(fun gen_modtageq 2)
(fun excllock 0)
(fun case4 3)
(fun locker2_obtainables 2)
(fun case5 4)
(fun andt 2)
(fun locker2_obtainable 2)
(fun locker2_check_available 2)
(fun case6 4)
(fun equal 2)
(fun locker2_check_availables 2)
(fun locker2_adduniq 2)
(fun delete 2)
(fun case8 4)
(fun gen_tag 1)
(fun case9 4)
(fun eqs 2)
(fun empty 0)
(fun stack 2)
(fun pushs 2)
(fun pops 1)
(fun tops 1)
(fun istops 2)
(fun eqc 2)
(fun nocalls 0)
(fun calls 3)
(fun push 3)
(fun push1 6)
(rule (or T T) T)
(rule (or F T) T)
(rule (or T F) T)
(rule (or F F) F)
(rule (and T B) B)
(rule (and B T) B)
(rule (and F B) F)
(rule (and B F) F)
(rule (imp T B) B)
(rule (imp F B) T)
(rule (not T) F)
(rule (not F) T)
(rule (if T B1 B2) B1)
(rule (if F B1 B2) B2)
(rule (eq T T) T)
(rule (eq F F) T)
(rule (eq T F) F)
(rule (eq F T) F)
(rule (eqt nil undefined) F)
(rule (eqt nil (pid N2)) F)
(rule (eqt nil (int N2)) F)
(rule (eqt nil (cons H2 T2)) F)
(rule (eqt nil (tuple H2 T2)) F)
(rule (eqt nil (tuplenil H2)) F)
(rule (eqt a nil) F)
(rule (eqt a a) T)
(rule (eqt a excl) F)
(rule (eqt a false) F)
(rule (eqt a lock) F)
(rule (eqt a locker) F)
(rule (eqt a mcrlrecord) F)
(rule (eqt a ok) F)
(rule (eqt a pending) F)
(rule (eqt a release) F)
(rule (eqt a request) F)
(rule (eqt a resource) F)
(rule (eqt a tag) F)
(rule (eqt a true) F)
(rule (eqt a undefined) F)
(rule (eqt a (pid N2)) F)
(rule (eqt a (int N2)) F)
(rule (eqt a (cons H2 T2)) F)
(rule (eqt a (tuple H2 T2)) F)
(rule (eqt a (tuplenil H2)) F)
(rule (eqt excl nil) F)
(rule (eqt excl a) F)
(rule (eqt excl excl) T)
(rule (eqt excl false) F)
(rule (eqt excl lock) F)
(rule (eqt excl locker) F)
(rule (eqt excl mcrlrecord) F)
(rule (eqt excl ok) F)
(rule (eqt excl pending) F)
(rule (eqt excl release) F)
(rule (eqt excl request) F)
(rule (eqt excl resource) F)
(rule (eqt excl tag) F)
(rule (eqt excl true) F)
(rule (eqt excl undefined) F)
(rule (eqt excl (pid N2)) F)
(rule (eqt excl (eqt false (int N2))) F)
(rule (eqt false (cons H2 T2)) F)
(rule (eqt false (tuple H2 T2)) F)
(rule (eqt false (tuplenil H2)) F)
(rule (eqt lock nil) F)
(rule (eqt lock a) F)
(rule (eqt lock excl) F)
(rule (eqt lock false) F)
(rule (eqt lock lock) T)
(rule (eqt lock locker) F)
(rule (eqt lock mcrlrecord) F)
(rule (eqt lock ok) F)
(rule (eqt lock pending) F)
(rule (eqt lock release) F)
(rule (eqt lock request) F)
(rule (eqt lock resource) F)
(rule (eqt lock tag) F)
(rule (eqt lock true) F)
(rule (eqt lock undefined) F)
(rule (eqt lock (pid N2)) F)
(rule (eqt lock (int N2)) F)
(rule (eqt lock (cons H2 T2)) F)
(rule (eqt lock (tuple H2 T2)) F)
(rule (eqt lock (tuplenil H2)) F)
(rule (eqt locker nil) F)
(rule (eqt locker a) F)
(rule (eqt locker excl) F)
(rule (eqt locker false) F)
(rule (eqt locker lock) F)
(rule (eqt locker locker) T)
(rule (eqt locker mcrlrecord) F)
(rule (eqt locker ok) F)
(rule (eqt locker pending) F)
(rule (eqt locker release) F)
(rule (eqt locker request) F)
(rule (eqt locker resource) F)
(rule (eqt locker tag) F)
(rule (eqt locker true) F)
(rule (eqt locker undefined) F)
(rule (eqt locker (pid N2)) F)
(rule (eqt locker (int N2)) F)
(rule (eqt locker (cons H2 T2)) F)
(rule (eqt locker (tuple H2 T2)) F)
(rule (eqt locker (tuplenil H2)) F)
(rule (eqt mcrlrecord nil) F)
(rule (eqt mcrlrecord a) F)
(rule (eqt mcrlrecord excl) F)
(rule (eqt mcrlrecord false) F)
(rule (eqt mcrlrecord lock) F)
(rule (eqt mcrlrecord locker) F)
(rule (eqt mcrlrecord mcrlrecord) T)
(rule (eqt mcrlrecord ok) F)
(rule (eqt mcrlrecord pending) F)
(rule (eqt mcrlrecord release) F)
(rule (eqt mcrlrecord request) F)
(rule (eqt mcrlrecord resource) F)
(rule (eqt ok resource) F)
(rule (eqt ok tag) F)
(rule (eqt ok true) F)
(rule (eqt ok undefined) F)
(rule (eqt ok (pid N2)) F)
(rule (eqt ok (int N2)) F)
(rule (eqt ok (cons H2 T2)) F)
(rule (eqt ok (tuple H2 T2)) F)
(rule (eqt ok (tuplenil H2)) F)
(rule (eqt pending nil) F)
(rule (eqt pending a) F)
(rule (eqt pending excl) F)
(rule (eqt pending false) F)
(rule (eqt pending lock) F)
(rule (eqt pending locker) F)
(rule (eqt pending mcrlrecord) F)
(rule (eqt pending ok) F)
(rule (eqt pending pending) T)
(rule (eqt pending release) F)
(rule (eqt pending request) F)
(rule (eqt pending resource) F)
(rule (eqt pending tag) F)
(rule (eqt pending true) F)
(rule (eqt pending undefined) F)
(rule (eqt pending (pid N2)) F)
(rule (eqt pending (int N2)) F)
(rule (eqt pending (cons H2 T2)) F)
(rule (eqt pending (tuple H2 T2)) F)
(rule (eqt pending (tuplenil H2)) F)
(rule (eqt release nil) F)
(rule (eqt release a) F)
(rule (eqt release excl) F)
(rule (eqt release false) F)
(rule (eqt release lock) F)
(rule (eqt release locker) F)
(rule (eqt release mcrlrecord) F)
(rule (eqt release ok) F)
(rule (eqt request mcrlrecord) F)
(rule (eqt request ok) F)
(rule (eqt request pending) F)
(rule (eqt request release) F)
(rule (eqt request request) T)
(rule (eqt request resource) F)
(rule (eqt request tag) F)
(rule (eqt request true) F)
(rule (eqt request undefined) F)
(rule (eqt request (pid N2)) F)
(rule (eqt request (int N2)) F)
(rule (eqt request (cons H2 T2)) F)
(rule (eqt request (tuple H2 T2)) F)
(rule (eqt request (tuplenil H2)) F)
(rule (eqt resource nil) F)
(rule (eqt resource a) F)
(rule (eqt resource excl) F)
(rule (eqt resource false) F)
(rule (eqt resource lock) F)
(rule (eqt resource locker) F)
(rule (eqt resource mcrlrecord) F)
(rule (eqt resource ok) F)
(rule (eqt resource pending) F)
(rule (eqt resource release) F)
(rule (eqt resource request) F)
(rule (eqt resource resource) T)
(rule (eqt resource tag) F)
(rule (eqt resource true) F)
(rule (eqt resource undefined) F)
(rule (eqt resource (pid N2)) F)
(rule (eqt resource (int N2)) F)
(rule (eqt resource (cons H2 T2)) F)
(rule (eqt resource (tuple H2 T2)) F)
(rule (eqt resource (tuplenil H2)) F)
(rule (eqt tag nil) F)
(rule (eqt tag a) F)
(rule (eqt tag excl) F)
(rule (eqt tag false) F)
(rule (eqt tag lock) F)
(rule (eqt tag locker) F)
(rule (eqt tag mcrlrecord) F)
(rule (eqt tag ok) F)
(rule (eqt tag pending) F)
(rule (eqt tag release) F)
(rule (eqt tag request) F)
(rule (eqt tag resource) F)
(rule (eqt tag tag) T)
(rule (eqt tag true) F)
(rule (eqt tag undefined) F)
(rule (eqt tag (pid N2)) F)
(rule (eqt tag (int N2)) F)
(rule (eqt tag (cons H2 T2)) F)
(rule (eqt tag (tuple H2 T2)) F)
(rule (eqt tag (tuplenil H2)) F)
(rule (eqt true nil) F)
(rule (eqt true a) F)
(rule (eqt true excl) F)
(rule (eqt true false) F)
(rule (eqt true lock) F)
(rule (eqt true locker) F)
(rule (eqt true mcrlrecord) F)
(rule (eqt true ok) F)
(rule (eqt true pending) F)
(rule (eqt true release) F)
(rule (eqt true request) F)
(rule (eqt true resource) F)
(rule (eqt true tag) F)
(rule (eqt true true) T)
(rule (eqt true undefined) F)
(rule (eqt true (pid N2)) F)
(rule (eqt true (int N2)) F)
(rule (eqt true (cons H2 T2)) F)
(rule (eqt true (tuple H2 T2)) F)
(rule (eqt true (tuplenil H2)) F)
(rule (eqt undefined nil) F)
(rule (eqt undefined a) F)
(rule (eqt undefined (tuplenil H2)) F)
(rule (eqt (pid N1) nil) F)
(rule (eqt (pid N1) a) F)
(rule (eqt (pid N1) excl) F)
(rule (eqt (pid N1) false) F)
(rule (eqt (pid N1) lock) F)
(rule (eqt (pid N1) locker) F)
(rule (eqt (pid N1) mcrlrecord) F)
(rule (eqt (pid N1) ok) F)
(rule (eqt (pid N1) pending) F)
(rule (eqt (pid N1) release) F)
(rule (eqt (pid N1) request) F)
(rule (eqt (pid N1) resource) F)
(rule (eqt (pid N1) tag) F)
(rule (eqt (pid N1) true) F)
(rule (eqt (pid N1) undefined) F)
(rule (eqt (pid N1) (pid N2)) (eqt N1 N2))
(rule (eqt (pid N1) (int N2)) F)
(rule (eqt (pid N1) (cons H2 T2)) F)
(rule (eqt (pid N1) (tuple H2 T2)) F)
(rule (eqt (pid N1) (tuplenil H2)) F)
(rule (eqt (int N1) nil) F)
(rule (eqt (int N1) a) F)
(rule (eqt (int N1) excl) F)
(rule (eqt (int N1) false) F)
(rule (eqt (int N1) lock) F)
(rule (eqt (int N1) locker) F)
(rule (eqt (int N1) mcrlrecord) F)
(rule (eqt (int N1) ok) F)
(rule (eqt (int N1) pending) F)
(rule (eqt (int N1) release) F)
(rule (eqt (int N1) request) F)
(rule (eqt (int N1) resource) F)
(rule (eqt (int N1) tag) F)
(rule (eqt (int N1) true) F)
(rule (eqt (int N1) undefined) F)
(rule (eqt (cons H1 T1) resource) F)
(rule (eqt (cons H1 T1) tag) F)
(rule (eqt (cons H1 T1) true) F)
(rule (eqt (cons H1 T1) undefined) F)
(rule (eqt (cons H1 T1) (pid N2)) F)
(rule (eqt (cons H1 T1) (int N2)) F)
(rule (eqt (cons H1 T1) (cons H2 T2)) (and (eqt H1 H2) (eqt T1 T2)))
(rule (eqt (cons H1 T1) (tuple H2 T2)) F)
(rule (eqt (cons H1 T1) (tuplenil H2)) F)
(rule (eqt (tuple H1 T1) nil) F)
(rule (eqt (tuple H1 T1) a) F)
(rule (eqt (tuple H1 T1) excl) F)
(rule (eqt (tuple H1 T1) false) F)
(rule (eqt (tuple H1 T1) lock) F)
(rule (eqt (tuple H1 T1) locker) F)
(rule (eqt (tuple H1 T1) mcrlrecord) F)
(rule (eqt (tuple H1 T1) ok) F)
(rule (eqt (tuple H1 T1) pending) F)
(rule (eqt (tuple H1 T1) release) F)
(rule (eqt (tuple H1 T1) request) F)
(rule (eqt (tuple H1 T1) resource) F)
(rule (eqt (tuple H1 T1) tag) F)
(rule (eqt (tuple H1 T1) true) F)
(rule (eqt (tuple H1 T1) undefined) F)
(rule (eqt (tuple H1 T1) (pid N2)) F)
(rule (eqt (tuple H1 T1) (int N2)) F)
(rule (eqt (tuple H1 T1) (cons H2 T2)) F)
(rule (eqt (tuple H1 T1) (tuple H2 T2)) (and (eqt H1 H2) (eqt T1 T2)))
(rule (eqt (tuple H1 T1) (tuplenil H2)) F)
(rule (eqt (tuplenil H1) nil) F)
(rule (eqt (tuplenil H1) a) F)
(rule (eqt (tuplenil H1) excl) F)
(rule (eqt (tuplenil H1) false) F)
(rule (eqt (tuplenil H1) lock) F)
(rule (eqt (tuplenil H1) locker) F)
(rule (eqt (tuplenil H1) mcrlrecord) F)
(rule (eqt (tuplenil H1) ok) F)
(rule (eqt (tuplenil H1) pending) F)
(rule (eqt (tuplenil H1) release) F)
(rule (eqt (tuplenil H1) request) F)
(rule (eqt (tuplenil H1) resource) F)
(rule (eqt (tuplenil H1) tag) F)
(rule (eqt (tuplenil H1) true) F)
(rule (eqt (tuplenil H1) undefined) F)
(rule (eqt (tuplenil H1) (pid N2)) F)
(rule (eqt (tuplenil H1) (int N2)) F)
(rule (eqt (tuplenil H1) (cons H2 T2)) F)
(rule (eqt (tuplenil H1) (tuple H2 T2)) F)
(rule (eqt (tuplenil H1) (tuplenil H2)) (eqt H1 H2))
(rule (element (int (s |0|)) (tuplenil T1)) T1)
(rule (element (int (s |0|)) (tuple T1 T2)) T1)
(rule (element (int (s (s N1))) (tuple T1 T2)) (element (int (s N1)) T2))
(rule (record_new lock) (tuple mcrlrecord (tuple lock (tuple undefined (tuple nil (tuplenil nil))))))
(rule (record_extract (tuple mcrlrecord (tuple lock (tuple F0 (tuple F1 (tuplenil F2))))) lock resource) (tuple mcrlrecord (tuple lock (tuple F0 (tuple F1 (tuplenil F2))))))
(rule (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))))))
(rule (record_updates Record Name nil) Record)
(rule (record_updates Record Name (cons (tuple Field (tuplenil NewF)) Fields)) (record_updates (record_update Record Name Field NewF) Name Fields))
(rule (locker2_map_promote_pending nil Pending) nil)
(rule (locker2_map_promote_pending (cons Lock Locks) Pending) (cons (locker2_promote_pending Lock Pending) (locker2_map_promote_pending Locks Pending)))
(rule (locker2_map_claim_lock nil Resources Client) nil)
(rule (locker2_map_claim_lock (cons Lock Locks) Resources Client) (cons (locker2_claim_lock Lock Resources Client) (locker2_map_claim_lock Locks Resources Client)))
(rule (locker2_map_add_pending nil Resources Client) nil)
(rule (locker2_promote_pending Lock Client) (case0 Client Lock (record_extract Lock lock pending)))
(rule (case0 Client Lock (cons Client Pendings)) (record_updates Lock lock (cons (tuple excl (tuplenil Client)) (cons (tuple pending (tuplenil Pendings)) nil))))
(rule (case0 Client Lock MCRLFree0) Lock)
(rule (locker2_remove_pending Lock Client) (record_updates Lock lock (cons (tuple pending (tuplenil (subtract (record_extract Lock lock pending) (cons Client nil)))) nil)))
(rule (locker2_add_pending Lock Resources Client) (case1 Client Resources Lock (member (record_extract Lock lock resource) Resources)))
(rule (case1 Client Resources Lock true) (record_updates Lock lock (cons (tuple pending (tuplenil (append (record_extract Lock lock pending) (cons Client nil)))) nil)))
(rule (case1 Client Resources Lock false) Lock)
(rule (locker2_release_lock Lock Client) (case2 Client Lock (gen_modtageq Client (record_extract Lock lock excl))))
(rule (case2 Client Lock true) (record_updates Lock lock (cons (tuple excllock excl) nil)))
(rule (case4 Client Lock MCRLFree1) false)
(rule (locker2_obtainables nil Client) true)
(rule (locker2_obtainables (cons Lock Locks) Client) (case5 Client Locks Lock (member Client (record_extract Lock lock pending))))
(rule (case5 Client Locks Lock true) (andt (locker2_obtainable Lock Client) (locker2_obtainables Locks Client)))
(rule (case5 Client Locks Lock false) (locker2_obtainables Locks Client))
(rule (locker2_check_available Resource nil) false)
(rule (locker2_check_available Resource (cons Lock Locks)) (case6 Locks Lock Resource (equal Resource (record_extract Lock lock resource))))
(rule (case6 Locks Lock Resource true) (andt (equal (record_extract Lock lock excl) nil) (equal (record_extract Lock lock pending) nil)))
(rule (case6 Locks Lock Resource false) (locker2_check_available Resource Locks))
(rule (locker2_check_availables nil Locks) true)
(rule (locker2_check_availables (cons Resource Resources) Locks) (andt (locker2_check_available Resource Locks) (locker2_check_availables Resources Locks)))
(rule (locker2_adduniq nil List) List)
(rule (append (cons Head Tail) List) (cons Head (append Tail List)))
(rule (subtract List nil) List)
(rule (subtract List (cons Head Tail)) (subtract (delete Head List) Tail))
(rule (delete E nil) nil)
(rule (delete E (cons Head Tail)) (case8 Tail Head E (equal E Head)))
(rule (case8 Tail Head E true) Tail)
(rule (case8 Tail Head E false) (cons Head (delete E Tail)))
(rule (gen_tag Pid) (tuple Pid (tuplenil tag)))
(rule (gen_modtageq Client1 Client2) (equal Client1 Client2))
(rule (member E nil) false)
(rule (member E (cons Head Tail)) (case9 Tail Head E (equal E Head)))
(rule (case9 Tail Head E true) true)
(rule (case9 Tail Head E false) (member E Tail))
(rule (eqs empty empty) T)
(rule (eqs empty (stack E2 S2)) F)
(rule (eqs (stack E1 S1) empty) F)
(rule (eqs (stack E1 S1) (stack E2 S2)) (and (eqt E1 E2) (eqs S1 S2)))
(rule (pushs E1 S1) (stack E1 S1))
(rule (pops (stack E1 S1)) S1)
(rule (tops (stack E1 S1)) E1)
(rule (istops E1 empty) F)
(rule (istops E1 (stack E2 S1)) (eqt E1 E2))
(rule (eqc nocalls nocalls) T)
(rule (eqc nocalls (calls E2 S2 CS2)) F)
(rule (eqc (calls E1 S1 CS1) nocalls) F)
(rule (eqc (calls E1 S1 CS1) (calls E2 S2 CS2)) (and (eqt E1 E2) (and (eqs S1 S2) (eqc CS1 CS2))))
(rule (push E1 E2 nocalls) (calls E1 (stack E2 empty) nocalls))
(rule (push E1 E2 (calls E3 S1 CS1)) (push1 E1 E2 E3 S1 CS1 (eqt E1 E3)))
(rule (push1 E1 E2 E3 S1 CS1 T) (calls E3 (pushs E2 S1) CS1))