- : unit = ()
- : unit = ()
h : heuristic = <heuristic>
- : unit = ()
APPLY CRITERIA (Marked dependency pairs)

TRS termination of:
[1] or(T,T) -> T
[2] or(F,T) -> T
[3] or(T,F) -> T
[4] or(F,F) -> F
[5] and(T,B) -> B
[6] and(B,T) -> B
[7] and(F,B) -> F
[8] and(B,F) -> F
[9] imp(T,B) -> B
[10] imp(F,B) -> T
[11] not(T) -> F
[12] not(F) -> T
[13] if(T,B1,B2) -> B1
[14] if(F,B1,B2) -> B2
[15] eq(T,T) -> T
[16] eq(F,F) -> T
[17] eq(T,F) -> F
[18] eq(F,T) -> F
[19] eqt(nil,undefined) -> F
[20] eqt(nil,pid(N2)) -> F
[21] eqt(nil,int(N2)) -> F
[22] eqt(nil,cons(H2,T2)) -> F
[23] eqt(nil,tuple(H2,T2)) -> F
[24] eqt(nil,tuplenil(H2)) -> F
[25] eqt(a,nil) -> F
[26] eqt(a,a) -> T
[27] eqt(a,excl) -> F
[28] eqt(a,false) -> F
[29] eqt(a,lock) -> F
[30] eqt(a,locker) -> F
[31] eqt(a,mcrlrecord) -> F
[32] eqt(a,ok) -> F
[33] eqt(a,pending) -> F
[34] eqt(a,release) -> F
[35] eqt(a,request) -> F
[36] eqt(a,resource) -> F
[37] eqt(a,tag) -> F
[38] eqt(a,true) -> F
[39] eqt(a,undefined) -> F
[40] eqt(a,pid(N2)) -> F
[41] eqt(a,int(N2)) -> F
[42] eqt(a,cons(H2,T2)) -> F
[43] eqt(a,tuple(H2,T2)) -> F
[44] eqt(a,tuplenil(H2)) -> F
[45] eqt(excl,nil) -> F
[46] eqt(excl,a) -> F
[47] eqt(excl,excl) -> T
[48] eqt(excl,false) -> F
[49] eqt(excl,lock) -> F
[50] eqt(excl,locker) -> F
[51] eqt(excl,mcrlrecord) -> F
[52] eqt(excl,ok) -> F
[53] eqt(excl,pending) -> F
[54] eqt(excl,release) -> F
[55] eqt(excl,request) -> F
[56] eqt(excl,resource) -> F
[57] eqt(excl,tag) -> F
[58] eqt(excl,true) -> F
[59] eqt(excl,undefined) -> F
[60] eqt(excl,pid(N2)) -> F
[61] eqt(excl,eqt(false,int(N2))) -> F
[62] eqt(false,cons(H2,T2)) -> F
[63] eqt(false,tuple(H2,T2)) -> F
[64] eqt(false,tuplenil(H2)) -> F
[65] eqt(lock,nil) -> F
[66] eqt(lock,a) -> F
[67] eqt(lock,excl) -> F
[68] eqt(lock,false) -> F
[69] eqt(lock,lock) -> T
[70] eqt(lock,locker) -> F
[71] eqt(lock,mcrlrecord) -> F
[72] eqt(lock,ok) -> F
[73] eqt(lock,pending) -> F
[74] eqt(lock,release) -> F
[75] eqt(lock,request) -> F
[76] eqt(lock,resource) -> F
[77] eqt(lock,tag) -> F
[78] eqt(lock,true) -> F
[79] eqt(lock,undefined) -> F
[80] eqt(lock,pid(N2)) -> F
[81] eqt(lock,int(N2)) -> F
[82] eqt(lock,cons(H2,T2)) -> F
[83] eqt(lock,tuple(H2,T2)) -> F
[84] eqt(lock,tuplenil(H2)) -> F
[85] eqt(locker,nil) -> F
[86] eqt(locker,a) -> F
[87] eqt(locker,excl) -> F
[88] eqt(locker,false) -> F
[89] eqt(locker,lock) -> F
[90] eqt(locker,locker) -> T
[91] eqt(locker,mcrlrecord) -> F
[92] eqt(locker,ok) -> F
[93] eqt(locker,pending) -> F
[94] eqt(locker,release) -> F
[95] eqt(locker,request) -> F
[96] eqt(locker,resource) -> F
[97] eqt(locker,tag) -> F
[98] eqt(locker,true) -> F
[99] eqt(locker,undefined) -> F
[100] eqt(locker,pid(N2)) -> F
[101] eqt(locker,int(N2)) -> F
[102] eqt(locker,cons(H2,T2)) -> F
[103] eqt(locker,tuple(H2,T2)) -> F
[104] eqt(locker,tuplenil(H2)) -> F
[105] eqt(mcrlrecord,nil) -> F
[106] eqt(mcrlrecord,a) -> F
[107] eqt(mcrlrecord,excl) -> F
[108] eqt(mcrlrecord,false) -> F
[109] eqt(mcrlrecord,lock) -> F
[110] eqt(mcrlrecord,locker) -> F
[111] eqt(mcrlrecord,mcrlrecord) -> T
[112] eqt(mcrlrecord,ok) -> F
[113] eqt(mcrlrecord,pending) -> F
[114] eqt(mcrlrecord,release) -> F
[115] eqt(mcrlrecord,request) -> F
[116] eqt(mcrlrecord,resource) -> F
[117] eqt(ok,resource) -> F
[118] eqt(ok,tag) -> F
[119] eqt(ok,true) -> F
[120] eqt(ok,undefined) -> F
[121] eqt(ok,pid(N2)) -> F
[122] eqt(ok,int(N2)) -> F
[123] eqt(ok,cons(H2,T2)) -> F
[124] eqt(ok,tuple(H2,T2)) -> F
[125] eqt(ok,tuplenil(H2)) -> F
[126] eqt(pending,nil) -> F
[127] eqt(pending,a) -> F
[128] eqt(pending,excl) -> F
[129] eqt(pending,false) -> F
[130] eqt(pending,lock) -> F
[131] eqt(pending,locker) -> F
[132] eqt(pending,mcrlrecord) -> F
[133] eqt(pending,ok) -> F
[134] eqt(pending,pending) -> T
[135] eqt(pending,release) -> F
[136] eqt(pending,request) -> F
[137] eqt(pending,resource) -> F
[138] eqt(pending,tag) -> F
[139] eqt(pending,true) -> F
[140] eqt(pending,undefined) -> F
[141] eqt(pending,pid(N2)) -> F
[142] eqt(pending,int(N2)) -> F
[143] eqt(pending,cons(H2,T2)) -> F
[144] eqt(pending,tuple(H2,T2)) -> F
[145] eqt(pending,tuplenil(H2)) -> F
[146] eqt(release,nil) -> F
[147] eqt(release,a) -> F
[148] eqt(release,excl) -> F
[149] eqt(release,false) -> F
[150] eqt(release,lock) -> F
[151] eqt(release,locker) -> F
[152] eqt(release,mcrlrecord) -> F
[153] eqt(release,ok) -> F
[154] eqt(request,mcrlrecord) -> F
[155] eqt(request,ok) -> F
[156] eqt(request,pending) -> F
[157] eqt(request,release) -> F
[158] eqt(request,request) -> T
[159] eqt(request,resource) -> F
[160] eqt(request,tag) -> F
[161] eqt(request,true) -> F
[162] eqt(request,undefined) -> F
[163] eqt(request,pid(N2)) -> F
[164] eqt(request,int(N2)) -> F
[165] eqt(request,cons(H2,T2)) -> F
[166] eqt(request,tuple(H2,T2)) -> F
[167] eqt(request,tuplenil(H2)) -> F
[168] eqt(resource,nil) -> F
[169] eqt(resource,a) -> F
[170] eqt(resource,excl) -> F
[171] eqt(resource,false) -> F
[172] eqt(resource,lock) -> F
[173] eqt(resource,locker) -> F
[174] eqt(resource,mcrlrecord) -> F
[175] eqt(resource,ok) -> F
[176] eqt(resource,pending) -> F
[177] eqt(resource,release) -> F
[178] eqt(resource,request) -> F
[179] eqt(resource,resource) -> T
[180] eqt(resource,tag) -> F
[181] eqt(resource,true) -> F
[182] eqt(resource,undefined) -> F
[183] eqt(resource,pid(N2)) -> F
[184] eqt(resource,int(N2)) -> F
[185] eqt(resource,cons(H2,T2)) -> F
[186] eqt(resource,tuple(H2,T2)) -> F
[187] eqt(resource,tuplenil(H2)) -> F
[188] eqt(tag,nil) -> F
[189] eqt(tag,a) -> F
[190] eqt(tag,excl) -> F
[191] eqt(tag,false) -> F
[192] eqt(tag,lock) -> F
[193] eqt(tag,locker) -> F
[194] eqt(tag,mcrlrecord) -> F
[195] eqt(tag,ok) -> F
[196] eqt(tag,pending) -> F
[197] eqt(tag,release) -> F
[198] eqt(tag,request) -> F
[199] eqt(tag,resource) -> F
[200] eqt(tag,tag) -> T
[201] eqt(tag,true) -> F
[202] eqt(tag,undefined) -> F
[203] eqt(tag,pid(N2)) -> F
[204] eqt(tag,int(N2)) -> F
[205] eqt(tag,cons(H2,T2)) -> F
[206] eqt(tag,tuple(H2,T2)) -> F
[207] eqt(tag,tuplenil(H2)) -> F
[208] eqt(true,nil) -> F
[209] eqt(true,a) -> F
[210] eqt(true,excl) -> F
[211] eqt(true,false) -> F
[212] eqt(true,lock) -> F
[213] eqt(true,locker) -> F
[214] eqt(true,mcrlrecord) -> F
[215] eqt(true,ok) -> F
[216] eqt(true,pending) -> F
[217] eqt(true,release) -> F
[218] eqt(true,request) -> F
[219] eqt(true,resource) -> F
[220] eqt(true,tag) -> F
[221] eqt(true,true) -> T
[222] eqt(true,undefined) -> F
[223] eqt(true,pid(N2)) -> F
[224] eqt(true,int(N2)) -> F
[225] eqt(true,cons(H2,T2)) -> F
[226] eqt(true,tuple(H2,T2)) -> F
[227] eqt(true,tuplenil(H2)) -> F
[228] eqt(undefined,nil) -> F
[229] eqt(undefined,a) -> F
[230] eqt(undefined,tuplenil(H2)) -> F
[231] eqt(pid(N1),nil) -> F
[232] eqt(pid(N1),a) -> F
[233] eqt(pid(N1),excl) -> F
[234] eqt(pid(N1),false) -> F
[235] eqt(pid(N1),lock) -> F
[236] eqt(pid(N1),locker) -> F
[237] eqt(pid(N1),mcrlrecord) -> F
[238] eqt(pid(N1),ok) -> F
[239] eqt(pid(N1),pending) -> F
[240] eqt(pid(N1),release) -> F
[241] eqt(pid(N1),request) -> F
[242] eqt(pid(N1),resource) -> F
[243] eqt(pid(N1),tag) -> F
[244] eqt(pid(N1),true) -> F
[245] eqt(pid(N1),undefined) -> F
[246] eqt(pid(N1),pid(N2)) -> eqt(N1,N2)
[247] eqt(pid(N1),int(N2)) -> F
[248] eqt(pid(N1),cons(H2,T2)) -> F
[249] eqt(pid(N1),tuple(H2,T2)) -> F
[250] eqt(pid(N1),tuplenil(H2)) -> F
[251] eqt(int(N1),nil) -> F
[252] eqt(int(N1),a) -> F
[253] eqt(int(N1),excl) -> F
[254] eqt(int(N1),false) -> F
[255] eqt(int(N1),lock) -> F
[256] eqt(int(N1),locker) -> F
[257] eqt(int(N1),mcrlrecord) -> F
[258] eqt(int(N1),ok) -> F
[259] eqt(int(N1),pending) -> F
[260] eqt(int(N1),release) -> F
[261] eqt(int(N1),request) -> F
[262] eqt(int(N1),resource) -> F
[263] eqt(int(N1),tag) -> F
[264] eqt(int(N1),true) -> F
[265] eqt(int(N1),undefined) -> F
[266] eqt(cons(H1,T1),resource) -> F
[267] eqt(cons(H1,T1),tag) -> F
[268] eqt(cons(H1,T1),true) -> F
[269] eqt(cons(H1,T1),undefined) -> F
[270] eqt(cons(H1,T1),pid(N2)) -> F
[271] eqt(cons(H1,T1),int(N2)) -> F
[272] eqt(cons(H1,T1),cons(H2,T2)) -> and(eqt(H1,H2),eqt(T1,T2))
[273] eqt(cons(H1,T1),tuple(H2,T2)) -> F
[274] eqt(cons(H1,T1),tuplenil(H2)) -> F
[275] eqt(tuple(H1,T1),nil) -> F
[276] eqt(tuple(H1,T1),a) -> F
[277] eqt(tuple(H1,T1),excl) -> F
[278] eqt(tuple(H1,T1),false) -> F
[279] eqt(tuple(H1,T1),lock) -> F
[280] eqt(tuple(H1,T1),locker) -> F
[281] eqt(tuple(H1,T1),mcrlrecord) -> F
[282] eqt(tuple(H1,T1),ok) -> F
[283] eqt(tuple(H1,T1),pending) -> F
[284] eqt(tuple(H1,T1),release) -> F
[285] eqt(tuple(H1,T1),request) -> F
[286] eqt(tuple(H1,T1),resource) -> F
[287] eqt(tuple(H1,T1),tag) -> F
[288] eqt(tuple(H1,T1),true) -> F
[289] eqt(tuple(H1,T1),undefined) -> F
[290] eqt(tuple(H1,T1),pid(N2)) -> F
[291] eqt(tuple(H1,T1),int(N2)) -> F
[292] eqt(tuple(H1,T1),cons(H2,T2)) -> F
[293] eqt(tuple(H1,T1),tuple(H2,T2)) -> and(eqt(H1,H2),eqt(T1,T2))
[294] eqt(tuple(H1,T1),tuplenil(H2)) -> F
[295] eqt(tuplenil(H1),nil) -> F
[296] eqt(tuplenil(H1),a) -> F
[297] eqt(tuplenil(H1),excl) -> F
[298] eqt(tuplenil(H1),false) -> F
[299] eqt(tuplenil(H1),lock) -> F
[300] eqt(tuplenil(H1),locker) -> F
[301] eqt(tuplenil(H1),mcrlrecord) -> F
[302] eqt(tuplenil(H1),ok) -> F
[303] eqt(tuplenil(H1),pending) -> F
[304] eqt(tuplenil(H1),release) -> F
[305] eqt(tuplenil(H1),request) -> F
[306] eqt(tuplenil(H1),resource) -> F
[307] eqt(tuplenil(H1),tag) -> F
[308] eqt(tuplenil(H1),true) -> F
[309] eqt(tuplenil(H1),undefined) -> F
[310] eqt(tuplenil(H1),pid(N2)) -> F
[311] eqt(tuplenil(H1),int(N2)) -> F
[312] eqt(tuplenil(H1),cons(H2,T2)) -> F
[313] eqt(tuplenil(H1),tuple(H2,T2)) -> F
[314] eqt(tuplenil(H1),tuplenil(H2)) -> eqt(H1,H2)
[315] element(int(s(0)),tuplenil(T1)) -> T1
[316] element(int(s(0)),tuple(T1,T2)) -> T1
[317] element(int(s(s(N1))),tuple(T1,T2)) -> element(int(s(N1)),T2)
[318] record_new(lock) ->
 tuple(mcrlrecord,tuple(lock,tuple(undefined,tuple(nil,tuplenil(nil)))))
[319] record_extract(tuple(mcrlrecord,
                      tuple(lock,tuple(F0,tuple(F1,tuplenil(F2))))),lock,
       resource) ->
 tuple(mcrlrecord,tuple(lock,tuple(F0,tuple(F1,tuplenil(F2)))))
[320] 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)))))
[321] record_updates(Record,Name,nil) -> Record
[322] record_updates(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields)) ->
 record_updates(record_update(Record,Name,Field,NewF),Name,Fields)
[323] locker2_map_promote_pending(nil,Pending) -> nil
[324] locker2_map_promote_pending(cons(Lock,Locks),Pending) ->
 cons(locker2_promote_pending(Lock,Pending),
  locker2_map_promote_pending(Locks,Pending))
[325] locker2_map_claim_lock(nil,Resources,Client) -> nil
[326] locker2_map_claim_lock(cons(Lock,Locks),Resources,Client) ->
 cons(locker2_claim_lock(Lock,Resources,Client),
  locker2_map_claim_lock(Locks,Resources,Client))
[327] locker2_map_add_pending(nil,Resources,Client) -> nil
[328] locker2_promote_pending(Lock,Client) ->
 case0(Client,Lock,record_extract(Lock,lock,pending))
[329] case0(Client,Lock,cons(Client,Pendings)) ->
 record_updates(Lock,lock,
  cons(tuple(excl,tuplenil(Client)),
   cons(tuple(pending,tuplenil(Pendings)),nil)))
[330] case0(Client,Lock,MCRLFree0) -> Lock
[331] locker2_remove_pending(Lock,Client) ->
 record_updates(Lock,lock,
  cons(tuple(pending,
        tuplenil(subtract(record_extract(Lock,lock,pending),cons(Client,nil)))),
   nil))
[332] locker2_add_pending(Lock,Resources,Client) ->
 case1(Client,Resources,Lock,
  member(record_extract(Lock,lock,resource),Resources))
[333] case1(Client,Resources,Lock,true) ->
 record_updates(Lock,lock,
  cons(tuple(pending,
        tuplenil(append(record_extract(Lock,lock,pending),cons(Client,nil)))),
   nil))
[334] case1(Client,Resources,Lock,false) -> Lock
[335] locker2_release_lock(Lock,Client) ->
 case2(Client,Lock,gen_modtageq(Client,record_extract(Lock,lock,excl)))
[336] case2(Client,Lock,true) ->
 record_updates(Lock,lock,cons(tuple(excllock,excl),nil))
[337] case4(Client,Lock,MCRLFree1) -> false
[338] locker2_obtainables(nil,Client) -> true
[339] locker2_obtainables(cons(Lock,Locks),Client) ->
 case5(Client,Locks,Lock,member(Client,record_extract(Lock,lock,pending)))
[340] case5(Client,Locks,Lock,true) ->
 andt(locker2_obtainable(Lock,Client),locker2_obtainables(Locks,Client))
[341] case5(Client,Locks,Lock,false) -> locker2_obtainables(Locks,Client)
[342] locker2_check_available(Resource,nil) -> false
[343] locker2_check_available(Resource,cons(Lock,Locks)) ->
 case6(Locks,Lock,Resource,equal(Resource,record_extract(Lock,lock,resource)))
[344] case6(Locks,Lock,Resource,true) ->
 andt(equal(record_extract(Lock,lock,excl),nil),
  equal(record_extract(Lock,lock,pending),nil))
[345] case6(Locks,Lock,Resource,false) ->
 locker2_check_available(Resource,Locks)
[346] locker2_check_availables(nil,Locks) -> true
[347] locker2_check_availables(cons(Resource,Resources),Locks) ->
 andt(locker2_check_available(Resource,Locks),
  locker2_check_availables(Resources,Locks))
[348] locker2_adduniq(nil,List) -> List
[349] append(cons(Head,Tail),List) -> cons(Head,append(Tail,List))
[350] subtract(List,nil) -> List
[351] subtract(List,cons(Head,Tail)) -> subtract(delete(Head,List),Tail)
[352] delete(E,nil) -> nil
[353] delete(E,cons(Head,Tail)) -> case8(Tail,Head,E,equal(E,Head))
[354] case8(Tail,Head,E,true) -> Tail
[355] case8(Tail,Head,E,false) -> cons(Head,delete(E,Tail))
[356] gen_tag(Pid) -> tuple(Pid,tuplenil(tag))
[357] gen_modtageq(Client1,Client2) -> equal(Client1,Client2)
[358] member(E,nil) -> false
[359] member(E,cons(Head,Tail)) -> case9(Tail,Head,E,equal(E,Head))
[360] case9(Tail,Head,E,true) -> true
[361] case9(Tail,Head,E,false) -> member(E,Tail)
[362] eqs(empty,empty) -> T
[363] eqs(empty,stack(E2,S2)) -> F
[364] eqs(stack(E1,S1),empty) -> F
[365] eqs(stack(E1,S1),stack(E2,S2)) -> and(eqt(E1,E2),eqs(S1,S2))
[366] pushs(E1,S1) -> stack(E1,S1)
[367] pops(stack(E1,S1)) -> S1
[368] tops(stack(E1,S1)) -> E1
[369] istops(E1,empty) -> F
[370] istops(E1,stack(E2,S1)) -> eqt(E1,E2)
[371] eqc(nocalls,nocalls) -> T
[372] eqc(nocalls,calls(E2,S2,CS2)) -> F
[373] eqc(calls(E1,S1,CS1),nocalls) -> F
[374] eqc(calls(E1,S1,CS1),calls(E2,S2,CS2)) ->
 and(eqt(E1,E2),and(eqs(S1,S2),eqc(CS1,CS2)))
[375] push(E1,E2,nocalls) -> calls(E1,stack(E2,empty),nocalls)
[376] push(E1,E2,calls(E3,S1,CS1)) -> push1(E1,E2,E3,S1,CS1,eqt(E1,E3))
[377] push1(E1,E2,E3,S1,CS1,T) -> calls(E3,pushs(E2,S1),CS1)


Sub problem: 
guided: 

DP termination of:
<Marked_eqt(pid(N1),pid(N2)) , Marked_eqt(N1,N2)>
<Marked_eqt(cons(H1,T1),cons(H2,T2)) , Marked_and(eqt(H1,H2),eqt(T1,T2))>
<Marked_eqt(cons(H1,T1),cons(H2,T2)) , Marked_eqt(H1,H2)>
<Marked_eqt(cons(H1,T1),cons(H2,T2)) , Marked_eqt(T1,T2)>
<Marked_eqt(tuple(H1,T1),tuple(H2,T2)) , Marked_and(eqt(H1,H2),eqt(T1,T2))>
<Marked_eqt(tuple(H1,T1),tuple(H2,T2)) , Marked_eqt(H1,H2)>
<Marked_eqt(tuple(H1,T1),tuple(H2,T2)) , Marked_eqt(T1,T2)>
<Marked_eqt(tuplenil(H1),tuplenil(H2)) , Marked_eqt(H1,H2)>
<Marked_element(int(s(s(N1))),tuple(T1,T2)) , Marked_element(int(s(N1)),T2)>
<Marked_record_updates(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields)) , Marked_record_updates(
                                                                    record_update(
                                                                    Record,
                                                                    Name,
                                                                    Field,
                                                                    NewF),Name,
                                                                    Fields)>
<Marked_record_updates(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields)) , Marked_record_update(
                                                                    Record,
                                                                    Name,Field,
                                                                    NewF)>
<Marked_locker2_map_promote_pending(cons(Lock,Locks),Pending) , Marked_locker2_promote_pending(
                                                                 Lock,
                                                                 Pending)>
<Marked_locker2_map_promote_pending(cons(Lock,Locks),Pending) , Marked_locker2_map_promote_pending(
                                                                 Locks,
                                                                 Pending)>
<Marked_locker2_map_claim_lock(cons(Lock,Locks),Resources,Client) , Marked_locker2_map_claim_lock(
                                                                    Locks,
                                                                    Resources,
                                                                    Client)>
<Marked_locker2_promote_pending(Lock,Client) , Marked_case0(Client,Lock,
                                                record_extract(Lock,lock,
                                                 pending))>
<Marked_locker2_promote_pending(Lock,Client) , Marked_record_extract(
                                                Lock,lock,pending)>
<Marked_case0(Client,Lock,cons(Client,Pendings)) , Marked_record_updates(
                                                    Lock,lock,
                                                    cons(tuple(excl,
                                                          tuplenil(Client)),
                                                     cons(tuple(pending,
                                                           tuplenil(Pendings)),
                                                      nil)))>
<Marked_locker2_remove_pending(Lock,Client) , Marked_record_updates(Lock,
                                               lock,
                                               cons(tuple(pending,
                                                     tuplenil(subtract(
                                                               record_extract(
                                                                Lock,
                                                                lock,
                                                                pending),
                                                               cons(Client,nil)))
                                                      ),nil))>
<Marked_locker2_remove_pending(Lock,Client) , Marked_subtract(record_extract(
                                                               Lock,lock,
                                                               pending),
                                               cons(Client,nil))>
<Marked_locker2_remove_pending(Lock,Client) , Marked_record_extract(Lock,
                                               lock,pending)>
<Marked_locker2_add_pending(Lock,Resources,Client) , Marked_case1(Client,
                                                      Resources,Lock,
                                                      member(record_extract(
                                                              Lock,lock,
                                                              resource),
                                                       Resources))>
<Marked_locker2_add_pending(Lock,Resources,Client) , Marked_member(record_extract(
                                                                    Lock,
                                                                    lock,
                                                                    resource),
                                                      Resources)>
<Marked_locker2_add_pending(Lock,Resources,Client) , Marked_record_extract(
                                                      Lock,lock,resource)>
<Marked_case1(Client,Resources,Lock,true) , Marked_record_updates(Lock,
                                             lock,
                                             cons(tuple(pending,
                                                   tuplenil(append(record_extract(
                                                                    Lock,
                                                                    lock,
                                                                    pending),
                                                             cons(Client,nil)))),
                                              nil))>
<Marked_case1(Client,Resources,Lock,true) , Marked_append(record_extract(
                                                           Lock,lock,
                                                           pending),
                                             cons(Client,nil))>
<Marked_case1(Client,Resources,Lock,true) , Marked_record_extract(Lock,
                                             lock,pending)>
<Marked_locker2_release_lock(Lock,Client) , Marked_case2(Client,Lock,
                                             gen_modtageq(Client,
                                              record_extract(Lock,lock,excl)))>
<Marked_locker2_release_lock(Lock,Client) , Marked_gen_modtageq(Client,
                                             record_extract(Lock,lock,excl))>
<Marked_locker2_release_lock(Lock,Client) , Marked_record_extract(Lock,
                                             lock,excl)>
<Marked_case2(Client,Lock,true) , Marked_record_updates(Lock,lock,
                                   cons(tuple(excllock,excl),nil))>
<Marked_locker2_obtainables(cons(Lock,Locks),Client) , Marked_case5(Client,
                                                        Locks,Lock,
                                                        member(Client,
                                                         record_extract(
                                                          Lock,lock,pending)))>
<Marked_locker2_obtainables(cons(Lock,Locks),Client) , Marked_member(
                                                        Client,
                                                        record_extract(
                                                         Lock,lock,pending))>
<Marked_locker2_obtainables(cons(Lock,Locks),Client) , Marked_record_extract(
                                                        Lock,lock,pending)>
<Marked_case5(Client,Locks,Lock,true) , Marked_locker2_obtainables(Locks,
                                         Client)>
<Marked_case5(Client,Locks,Lock,false) , Marked_locker2_obtainables(Locks,
                                          Client)>
<Marked_locker2_check_available(Resource,cons(Lock,Locks)) , Marked_case6(
                                                              Locks,Lock,
                                                              Resource,
                                                              equal(Resource,
                                                               record_extract(
                                                                Lock,
                                                                lock,
                                                                resource)))>
<Marked_locker2_check_available(Resource,cons(Lock,Locks)) , Marked_record_extract(
                                                              Lock,lock,
                                                              resource)>
<Marked_case6(Locks,Lock,Resource,true) , Marked_record_extract(Lock,lock,excl)>
<Marked_case6(Locks,Lock,Resource,true) , Marked_record_extract(Lock,
                                           lock,pending)>
<Marked_case6(Locks,Lock,Resource,false) , Marked_locker2_check_available(
                                            Resource,Locks)>
<Marked_locker2_check_availables(cons(Resource,Resources),Locks) , Marked_locker2_check_available(
                                                                    Resource,
                                                                    Locks)>
<Marked_locker2_check_availables(cons(Resource,Resources),Locks) , Marked_locker2_check_availables(
                                                                    Resources,
                                                                    Locks)>
<Marked_append(cons(Head,Tail),List) , Marked_append(Tail,List)>
<Marked_subtract(List,cons(Head,Tail)) , Marked_subtract(delete(Head,List),
                                          Tail)>
<Marked_subtract(List,cons(Head,Tail)) , Marked_delete(Head,List)>
<Marked_delete(E,cons(Head,Tail)) , Marked_case8(Tail,Head,E,equal(E,Head))>
<Marked_case8(Tail,Head,E,false) , Marked_delete(E,Tail)>
<Marked_member(E,cons(Head,Tail)) , Marked_case9(Tail,Head,E,equal(E,Head))>
<Marked_case9(Tail,Head,E,false) , Marked_member(E,Tail)>
<Marked_eqs(stack(E1,S1),stack(E2,S2)) , Marked_and(eqt(E1,E2),eqs(S1,S2))>
<Marked_eqs(stack(E1,S1),stack(E2,S2)) , Marked_eqt(E1,E2)>
<Marked_eqs(stack(E1,S1),stack(E2,S2)) , Marked_eqs(S1,S2)>
<Marked_istops(E1,stack(E2,S1)) , Marked_eqt(E1,E2)>
<Marked_eqc(calls(E1,S1,CS1),calls(E2,S2,CS2)) , Marked_and(eqt(E1,E2),
                                                  and(eqs(S1,S2),eqc(CS1,CS2)))>
<Marked_eqc(calls(E1,S1,CS1),calls(E2,S2,CS2)) , Marked_eqt(E1,E2)>
<Marked_eqc(calls(E1,S1,CS1),calls(E2,S2,CS2)) , Marked_and(eqs(S1,S2),
                                                  eqc(CS1,CS2))>
<Marked_eqc(calls(E1,S1,CS1),calls(E2,S2,CS2)) , Marked_eqs(S1,S2)>
<Marked_eqc(calls(E1,S1,CS1),calls(E2,S2,CS2)) , Marked_eqc(CS1,CS2)>
<Marked_push(E1,E2,calls(E3,S1,CS1)) , Marked_push1(E1,E2,E3,S1,CS1,eqt(E1,E3))>
<Marked_push(E1,E2,calls(E3,S1,CS1)) , Marked_eqt(E1,E3)>
<Marked_push1(E1,E2,E3,S1,CS1,T) , Marked_pushs(E2,S1)>
 
END GUIDED
APPLY CRITERIA (Graph splitting)
Found 11 components:

{  <Marked_element(int(s(s(N1))),tuple(T1,T2)) , Marked_element(int(s(N1)),T2)> 
      --> <Marked_element(int(s(s(N1))),tuple(T1,T2)) , Marked_element(
                                                         int(s(N1)),T2)>
}

{  <Marked_locker2_map_promote_pending(cons(Lock,Locks),Pending) , Marked_locker2_map_promote_pending(
                                                                    Locks,
                                                                    Pending)> 
      --> <Marked_locker2_map_promote_pending(cons(Lock,Locks),Pending) , Marked_locker2_map_promote_pending(
                                                                    Locks,
                                                                    Pending)>
}

{  <Marked_locker2_map_claim_lock(cons(Lock,Locks),Resources,Client) , Marked_locker2_map_claim_lock(
                                                                    Locks,
                                                                    Resources,
                                                                    Client)> 
      --> <Marked_locker2_map_claim_lock(cons(Lock,Locks),Resources,Client) , Marked_locker2_map_claim_lock(
                                                                    Locks,
                                                                    Resources,
                                                                    Client)>
}

{  <Marked_record_updates(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields)) , Marked_record_updates(
                                                                    record_update(
                                                                    Record,
                                                                    Name,
                                                                    Field,
                                                                    NewF),Name,
                                                                    Fields)> 
      --> <Marked_record_updates(Record,Name,
            cons(tuple(Field,tuplenil(NewF)),Fields)) , Marked_record_updates(
                                                         record_update(
                                                          Record,Name,
                                                          Field,NewF),
                                                         Name,Fields)>
}

{  <Marked_case5(Client,Locks,Lock,false) , Marked_locker2_obtainables(
                                             Locks,Client)> 
      --> <Marked_locker2_obtainables(cons(Lock,Locks),Client) , Marked_case5(
                                                                  Client,
                                                                  Locks,
                                                                  Lock,
                                                                  member(
                                                                   Client,
                                                                   record_extract(
                                                                    Lock,
                                                                    lock,
                                                                    pending)))>
  <Marked_case5(Client,Locks,Lock,true) , Marked_locker2_obtainables(
                                           Locks,Client)> 
     --> <Marked_locker2_obtainables(cons(Lock,Locks),Client) , Marked_case5(
                                                                 Client,
                                                                 Locks,
                                                                 Lock,
                                                                 member(
                                                                  Client,
                                                                  record_extract(
                                                                   Lock,
                                                                   lock,
                                                                   pending)))>
  <Marked_locker2_obtainables(cons(Lock,Locks),Client) , Marked_case5(
                                                          Client,Locks,
                                                          Lock,
                                                          member(Client,
                                                           record_extract(
                                                            Lock,lock,
                                                            pending)))> 
     --> <Marked_case5(Client,Locks,Lock,false) , Marked_locker2_obtainables(
                                                   Locks,Client)>
  <Marked_locker2_obtainables(cons(Lock,Locks),Client) , Marked_case5(
                                                          Client,Locks,
                                                          Lock,
                                                          member(Client,
                                                           record_extract(
                                                            Lock,lock,
                                                            pending)))> 
     --> <Marked_case5(Client,Locks,Lock,true) , Marked_locker2_obtainables(
                                                  Locks,Client)>
}

{  <Marked_locker2_check_availables(cons(Resource,Resources),Locks) , Marked_locker2_check_availables(
                                                                    Resources,
                                                                    Locks)> 
      --> <Marked_locker2_check_availables(cons(Resource,Resources),Locks) , Marked_locker2_check_availables(
                                                                    Resources,
                                                                    Locks)>
}

{  <Marked_append(cons(Head,Tail),List) , Marked_append(Tail,List)> 
      --> <Marked_append(cons(Head,Tail),List) , Marked_append(Tail,List)>
}

{  <Marked_subtract(List,cons(Head,Tail)) , Marked_subtract(delete(Head,List),
                                             Tail)> 
      --> <Marked_subtract(List,cons(Head,Tail)) , Marked_subtract(delete(
                                                                    Head,
                                                                    List),
                                                    Tail)>
}

{  <Marked_eqc(calls(E1,S1,CS1),calls(E2,S2,CS2)) , Marked_eqc(CS1,CS2)> 
      --> <Marked_eqc(calls(E1,S1,CS1),calls(E2,S2,CS2)) , Marked_eqc(CS1,CS2)>
}

{  <Marked_eqs(stack(E1,S1),stack(E2,S2)) , Marked_eqs(S1,S2)> 
      --> <Marked_eqs(stack(E1,S1),stack(E2,S2)) , Marked_eqs(S1,S2)>
}

{  <Marked_eqt(tuplenil(H1),tuplenil(H2)) , Marked_eqt(H1,H2)> 
      --> <Marked_eqt(tuplenil(H1),tuplenil(H2)) , Marked_eqt(H1,H2)>
  <Marked_eqt(tuplenil(H1),tuplenil(H2)) , Marked_eqt(H1,H2)> 
     --> <Marked_eqt(tuple(H1,T1),tuple(H2,T2)) , Marked_eqt(T1,T2)>
  <Marked_eqt(tuplenil(H1),tuplenil(H2)) , Marked_eqt(H1,H2)> 
     --> <Marked_eqt(tuple(H1,T1),tuple(H2,T2)) , Marked_eqt(H1,H2)>
  <Marked_eqt(tuplenil(H1),tuplenil(H2)) , Marked_eqt(H1,H2)> 
     --> <Marked_eqt(cons(H1,T1),cons(H2,T2)) , Marked_eqt(T1,T2)>
  <Marked_eqt(tuplenil(H1),tuplenil(H2)) , Marked_eqt(H1,H2)> 
     --> <Marked_eqt(cons(H1,T1),cons(H2,T2)) , Marked_eqt(H1,H2)>
  <Marked_eqt(tuplenil(H1),tuplenil(H2)) , Marked_eqt(H1,H2)> 
     --> <Marked_eqt(pid(N1),pid(N2)) , Marked_eqt(N1,N2)>
  <Marked_eqt(tuple(H1,T1),tuple(H2,T2)) , Marked_eqt(T1,T2)> 
     --> <Marked_eqt(tuplenil(H1),tuplenil(H2)) , Marked_eqt(H1,H2)>
  <Marked_eqt(tuple(H1,T1),tuple(H2,T2)) , Marked_eqt(T1,T2)> 
     --> <Marked_eqt(tuple(H1,T1),tuple(H2,T2)) , Marked_eqt(T1,T2)>
  <Marked_eqt(tuple(H1,T1),tuple(H2,T2)) , Marked_eqt(T1,T2)> 
     --> <Marked_eqt(tuple(H1,T1),tuple(H2,T2)) , Marked_eqt(H1,H2)>
  <Marked_eqt(tuple(H1,T1),tuple(H2,T2)) , Marked_eqt(T1,T2)> 
     --> <Marked_eqt(cons(H1,T1),cons(H2,T2)) , Marked_eqt(T1,T2)>
  <Marked_eqt(tuple(H1,T1),tuple(H2,T2)) , Marked_eqt(T1,T2)> 
     --> <Marked_eqt(cons(H1,T1),cons(H2,T2)) , Marked_eqt(H1,H2)>
  <Marked_eqt(tuple(H1,T1),tuple(H2,T2)) , Marked_eqt(T1,T2)> 
     --> <Marked_eqt(pid(N1),pid(N2)) , Marked_eqt(N1,N2)>
  <Marked_eqt(tuple(H1,T1),tuple(H2,T2)) , Marked_eqt(H1,H2)> 
     --> <Marked_eqt(tuplenil(H1),tuplenil(H2)) , Marked_eqt(H1,H2)>
  <Marked_eqt(tuple(H1,T1),tuple(H2,T2)) , Marked_eqt(H1,H2)> 
     --> <Marked_eqt(tuple(H1,T1),tuple(H2,T2)) , Marked_eqt(T1,T2)>
  <Marked_eqt(tuple(H1,T1),tuple(H2,T2)) , Marked_eqt(H1,H2)> 
     --> <Marked_eqt(tuple(H1,T1),tuple(H2,T2)) , Marked_eqt(H1,H2)>
  <Marked_eqt(tuple(H1,T1),tuple(H2,T2)) , Marked_eqt(H1,H2)> 
     --> <Marked_eqt(cons(H1,T1),cons(H2,T2)) , Marked_eqt(T1,T2)>
  <Marked_eqt(tuple(H1,T1),tuple(H2,T2)) , Marked_eqt(H1,H2)> 
     --> <Marked_eqt(cons(H1,T1),cons(H2,T2)) , Marked_eqt(H1,H2)>
  <Marked_eqt(tuple(H1,T1),tuple(H2,T2)) , Marked_eqt(H1,H2)> 
     --> <Marked_eqt(pid(N1),pid(N2)) , Marked_eqt(N1,N2)>
  <Marked_eqt(cons(H1,T1),cons(H2,T2)) , Marked_eqt(T1,T2)> 
     --> <Marked_eqt(tuplenil(H1),tuplenil(H2)) , Marked_eqt(H1,H2)>
  <Marked_eqt(cons(H1,T1),cons(H2,T2)) , Marked_eqt(T1,T2)> 
     --> <Marked_eqt(tuple(H1,T1),tuple(H2,T2)) , Marked_eqt(T1,T2)>
  <Marked_eqt(cons(H1,T1),cons(H2,T2)) , Marked_eqt(T1,T2)> 
     --> <Marked_eqt(tuple(H1,T1),tuple(H2,T2)) , Marked_eqt(H1,H2)>
  <Marked_eqt(cons(H1,T1),cons(H2,T2)) , Marked_eqt(T1,T2)> 
     --> <Marked_eqt(cons(H1,T1),cons(H2,T2)) , Marked_eqt(T1,T2)>
  <Marked_eqt(cons(H1,T1),cons(H2,T2)) , Marked_eqt(T1,T2)> 
     --> <Marked_eqt(cons(H1,T1),cons(H2,T2)) , Marked_eqt(H1,H2)>
  <Marked_eqt(cons(H1,T1),cons(H2,T2)) , Marked_eqt(T1,T2)> 
     --> <Marked_eqt(pid(N1),pid(N2)) , Marked_eqt(N1,N2)>
  <Marked_eqt(cons(H1,T1),cons(H2,T2)) , Marked_eqt(H1,H2)> 
     --> <Marked_eqt(tuplenil(H1),tuplenil(H2)) , Marked_eqt(H1,H2)>
  <Marked_eqt(cons(H1,T1),cons(H2,T2)) , Marked_eqt(H1,H2)> 
     --> <Marked_eqt(tuple(H1,T1),tuple(H2,T2)) , Marked_eqt(T1,T2)>
  <Marked_eqt(cons(H1,T1),cons(H2,T2)) , Marked_eqt(H1,H2)> 
     --> <Marked_eqt(tuple(H1,T1),tuple(H2,T2)) , Marked_eqt(H1,H2)>
  <Marked_eqt(cons(H1,T1),cons(H2,T2)) , Marked_eqt(H1,H2)> 
     --> <Marked_eqt(cons(H1,T1),cons(H2,T2)) , Marked_eqt(T1,T2)>
  <Marked_eqt(cons(H1,T1),cons(H2,T2)) , Marked_eqt(H1,H2)> 
     --> <Marked_eqt(cons(H1,T1),cons(H2,T2)) , Marked_eqt(H1,H2)>
  <Marked_eqt(cons(H1,T1),cons(H2,T2)) , Marked_eqt(H1,H2)> 
     --> <Marked_eqt(pid(N1),pid(N2)) , Marked_eqt(N1,N2)>
  <Marked_eqt(pid(N1),pid(N2)) , Marked_eqt(N1,N2)> 
     --> <Marked_eqt(tuplenil(H1),tuplenil(H2)) , Marked_eqt(H1,H2)>
  <Marked_eqt(pid(N1),pid(N2)) , Marked_eqt(N1,N2)> 
     --> <Marked_eqt(tuple(H1,T1),tuple(H2,T2)) , Marked_eqt(T1,T2)>
  <Marked_eqt(pid(N1),pid(N2)) , Marked_eqt(N1,N2)> 
     --> <Marked_eqt(tuple(H1,T1),tuple(H2,T2)) , Marked_eqt(H1,H2)>
  <Marked_eqt(pid(N1),pid(N2)) , Marked_eqt(N1,N2)> 
     --> <Marked_eqt(cons(H1,T1),cons(H2,T2)) , Marked_eqt(T1,T2)>
  <Marked_eqt(pid(N1),pid(N2)) , Marked_eqt(N1,N2)> 
     --> <Marked_eqt(cons(H1,T1),cons(H2,T2)) , Marked_eqt(H1,H2)>
  <Marked_eqt(pid(N1),pid(N2)) , Marked_eqt(N1,N2)> 
     --> <Marked_eqt(pid(N1),pid(N2)) , Marked_eqt(N1,N2)>
}
APPLY CRITERIA (Subterm criterion)

ST: Marked_element -> 2

APPLY CRITERIA (Subterm criterion)

ST: Marked_locker2_map_promote_pending -> 1

APPLY CRITERIA (Subterm criterion)

ST: Marked_locker2_map_claim_lock -> 1

APPLY CRITERIA (Subterm criterion)

ST: Marked_record_updates -> 3

APPLY CRITERIA (Subterm criterion)

ST: Marked_case5 -> 2
Marked_locker2_obtainables -> 1

APPLY CRITERIA (Subterm criterion)

ST: Marked_locker2_check_availables -> 1

APPLY CRITERIA (Subterm criterion)

ST: Marked_append -> 1

APPLY CRITERIA (Subterm criterion)

ST: Marked_subtract -> 2

APPLY CRITERIA (Subterm criterion)

ST: Marked_eqc -> 1

APPLY CRITERIA (Subterm criterion)

ST: Marked_eqs -> 1

APPLY CRITERIA (Subterm criterion)

ST: Marked_eqt -> 2

APPLY CRITERIA (Graph splitting)
Found 0 components:
APPLY CRITERIA (Graph splitting)
Found 0 components:
APPLY CRITERIA (Graph splitting)
Found 0 components:
APPLY CRITERIA (Graph splitting)
Found 0 components:
APPLY CRITERIA (Graph splitting)
Found 0 components:
APPLY CRITERIA (Graph splitting)
Found 0 components:
APPLY CRITERIA (Graph splitting)
Found 0 components:
APPLY CRITERIA (Graph splitting)
Found 0 components:
APPLY CRITERIA (Graph splitting)
Found 0 components:
APPLY CRITERIA (Graph splitting)
Found 0 components:
APPLY CRITERIA (Graph splitting)
Found 0 components:
SOLVED
{
 
TRS termination of:
[1] or(T,T) -> T
[2] or(F,T) -> T
[3] or(T,F) -> T
[4] or(F,F) -> F
[5] and(T,B) -> B
[6] and(B,T) -> B
[7] and(F,B) -> F
[8] and(B,F) -> F
[9] imp(T,B) -> B
[10] imp(F,B) -> T
[11] not(T) -> F
[12] not(F) -> T
[13] if(T,B1,B2) -> B1
[14] if(F,B1,B2) -> B2
[15] eq(T,T) -> T
[16] eq(F,F) -> T
[17] eq(T,F) -> F
[18] eq(F,T) -> F
[19] eqt(nil,undefined) -> F
[20] eqt(nil,pid(N2)) -> F
[21] eqt(nil,int(N2)) -> F
[22] eqt(nil,cons(H2,T2)) -> F
[23] eqt(nil,tuple(H2,T2)) -> F
[24] eqt(nil,tuplenil(H2)) -> F
[25] eqt(a,nil) -> F
[26] eqt(a,a) -> T
[27] eqt(a,excl) -> F
[28] eqt(a,false) -> F
[29] eqt(a,lock) -> F
[30] eqt(a,locker) -> F
[31] eqt(a,mcrlrecord) -> F
[32] eqt(a,ok) -> F
[33] eqt(a,pending) -> F
[34] eqt(a,release) -> F
[35] eqt(a,request) -> F
[36] eqt(a,resource) -> F
[37] eqt(a,tag) -> F
[38] eqt(a,true) -> F
[39] eqt(a,undefined) -> F
[40] eqt(a,pid(N2)) -> F
[41] eqt(a,int(N2)) -> F
[42] eqt(a,cons(H2,T2)) -> F
[43] eqt(a,tuple(H2,T2)) -> F
[44] eqt(a,tuplenil(H2)) -> F
[45] eqt(excl,nil) -> F
[46] eqt(excl,a) -> F
[47] eqt(excl,excl) -> T
[48] eqt(excl,false) -> F
[49] eqt(excl,lock) -> F
[50] eqt(excl,locker) -> F
[51] eqt(excl,mcrlrecord) -> F
[52] eqt(excl,ok) -> F
[53] eqt(excl,pending) -> F
[54] eqt(excl,release) -> F
[55] eqt(excl,request) -> F
[56] eqt(excl,resource) -> F
[57] eqt(excl,tag) -> F
[58] eqt(excl,true) -> F
[59] eqt(excl,undefined) -> F
[60] eqt(excl,pid(N2)) -> F
[61] eqt(excl,eqt(false,int(N2))) -> F
[62] eqt(false,cons(H2,T2)) -> F
[63] eqt(false,tuple(H2,T2)) -> F
[64] eqt(false,tuplenil(H2)) -> F
[65] eqt(lock,nil) -> F
[66] eqt(lock,a) -> F
[67] eqt(lock,excl) -> F
[68] eqt(lock,false) -> F
[69] eqt(lock,lock) -> T
[70] eqt(lock,locker) -> F
[71] eqt(lock,mcrlrecord) -> F
[72] eqt(lock,ok) -> F
[73] eqt(lock,pending) -> F
[74] eqt(lock,release) -> F
[75] eqt(lock,request) -> F
[76] eqt(lock,resource) -> F
[77] eqt(lock,tag) -> F
[78] eqt(lock,true) -> F
[79] eqt(lock,undefined) -> F
[80] eqt(lock,pid(N2)) -> F
[81] eqt(lock,int(N2)) -> F
[82] eqt(lock,cons(H2,T2)) -> F
[83] eqt(lock,tuple(H2,T2)) -> F
[84] eqt(lock,tuplenil(H2)) -> F
[85] eqt(locker,nil) -> F
[86] eqt(locker,a) -> F
[87] eqt(locker,excl) -> F
[88] eqt(locker,false) -> F
[89] eqt(locker,lock) -> F
[90] eqt(locker,locker) -> T
[91] eqt(locker,mcrlrecord) -> F
[92] eqt(locker,ok) -> F
[93] eqt(locker,pending) -> F
[94] eqt(locker,release) -> F
[95] eqt(locker,request) -> F
[96] eqt(locker,resource) -> F
[97] eqt(locker,tag) -> F
[98] eqt(locker,true) -> F
[99] eqt(locker,undefined) -> F
[100] eqt(locker,pid(N2)) -> F
[101] eqt(locker,int(N2)) -> F
[102] eqt(locker,cons(H2,T2)) -> F
[103] eqt(locker,tuple(H2,T2)) -> F
[104] eqt(locker,tuplenil(H2)) -> F
[105] eqt(mcrlrecord,nil) -> F
[106] eqt(mcrlrecord,a) -> F
[107] eqt(mcrlrecord,excl) -> F
[108] eqt(mcrlrecord,false) -> F
[109] eqt(mcrlrecord,lock) -> F
[110] eqt(mcrlrecord,locker) -> F
[111] eqt(mcrlrecord,mcrlrecord) -> T
[112] eqt(mcrlrecord,ok) -> F
[113] eqt(mcrlrecord,pending) -> F
[114] eqt(mcrlrecord,release) -> F
[115] eqt(mcrlrecord,request) -> F
[116] eqt(mcrlrecord,resource) -> F
[117] eqt(ok,resource) -> F
[118] eqt(ok,tag) -> F
[119] eqt(ok,true) -> F
[120] eqt(ok,undefined) -> F
[121] eqt(ok,pid(N2)) -> F
[122] eqt(ok,int(N2)) -> F
[123] eqt(ok,cons(H2,T2)) -> F
[124] eqt(ok,tuple(H2,T2)) -> F
[125] eqt(ok,tuplenil(H2)) -> F
[126] eqt(pending,nil) -> F
[127] eqt(pending,a) -> F
[128] eqt(pending,excl) -> F
[129] eqt(pending,false) -> F
[130] eqt(pending,lock) -> F
[131] eqt(pending,locker) -> F
[132] eqt(pending,mcrlrecord) -> F
[133] eqt(pending,ok) -> F
[134] eqt(pending,pending) -> T
[135] eqt(pending,release) -> F
[136] eqt(pending,request) -> F
[137] eqt(pending,resource) -> F
[138] eqt(pending,tag) -> F
[139] eqt(pending,true) -> F
[140] eqt(pending,undefined) -> F
[141] eqt(pending,pid(N2)) -> F
[142] eqt(pending,int(N2)) -> F
[143] eqt(pending,cons(H2,T2)) -> F
[144] eqt(pending,tuple(H2,T2)) -> F
[145] eqt(pending,tuplenil(H2)) -> F
[146] eqt(release,nil) -> F
[147] eqt(release,a) -> F
[148] eqt(release,excl) -> F
[149] eqt(release,false) -> F
[150] eqt(release,lock) -> F
[151] eqt(release,locker) -> F
[152] eqt(release,mcrlrecord) -> F
[153] eqt(release,ok) -> F
[154] eqt(request,mcrlrecord) -> F
[155] eqt(request,ok) -> F
[156] eqt(request,pending) -> F
[157] eqt(request,release) -> F
[158] eqt(request,request) -> T
[159] eqt(request,resource) -> F
[160] eqt(request,tag) -> F
[161] eqt(request,true) -> F
[162] eqt(request,undefined) -> F
[163] eqt(request,pid(N2)) -> F
[164] eqt(request,int(N2)) -> F
[165] eqt(request,cons(H2,T2)) -> F
[166] eqt(request,tuple(H2,T2)) -> F
[167] eqt(request,tuplenil(H2)) -> F
[168] eqt(resource,nil) -> F
[169] eqt(resource,a) -> F
[170] eqt(resource,excl) -> F
[171] eqt(resource,false) -> F
[172] eqt(resource,lock) -> F
[173] eqt(resource,locker) -> F
[174] eqt(resource,mcrlrecord) -> F
[175] eqt(resource,ok) -> F
[176] eqt(resource,pending) -> F
[177] eqt(resource,release) -> F
[178] eqt(resource,request) -> F
[179] eqt(resource,resource) -> T
[180] eqt(resource,tag) -> F
[181] eqt(resource,true) -> F
[182] eqt(resource,undefined) -> F
[183] eqt(resource,pid(N2)) -> F
[184] eqt(resource,int(N2)) -> F
[185] eqt(resource,cons(H2,T2)) -> F
[186] eqt(resource,tuple(H2,T2)) -> F
[187] eqt(resource,tuplenil(H2)) -> F
[188] eqt(tag,nil) -> F
[189] eqt(tag,a) -> F
[190] eqt(tag,excl) -> F
[191] eqt(tag,false) -> F
[192] eqt(tag,lock) -> F
[193] eqt(tag,locker) -> F
[194] eqt(tag,mcrlrecord) -> F
[195] eqt(tag,ok) -> F
[196] eqt(tag,pending) -> F
[197] eqt(tag,release) -> F
[198] eqt(tag,request) -> F
[199] eqt(tag,resource) -> F
[200] eqt(tag,tag) -> T
[201] eqt(tag,true) -> F
[202] eqt(tag,undefined) -> F
[203] eqt(tag,pid(N2)) -> F
[204] eqt(tag,int(N2)) -> F
[205] eqt(tag,cons(H2,T2)) -> F
[206] eqt(tag,tuple(H2,T2)) -> F
[207] eqt(tag,tuplenil(H2)) -> F
[208] eqt(true,nil) -> F
[209] eqt(true,a) -> F
[210] eqt(true,excl) -> F
[211] eqt(true,false) -> F
[212] eqt(true,lock) -> F
[213] eqt(true,locker) -> F
[214] eqt(true,mcrlrecord) -> F
[215] eqt(true,ok) -> F
[216] eqt(true,pending) -> F
[217] eqt(true,release) -> F
[218] eqt(true,request) -> F
[219] eqt(true,resource) -> F
[220] eqt(true,tag) -> F
[221] eqt(true,true) -> T
[222] eqt(true,undefined) -> F
[223] eqt(true,pid(N2)) -> F
[224] eqt(true,int(N2)) -> F
[225] eqt(true,cons(H2,T2)) -> F
[226] eqt(true,tuple(H2,T2)) -> F
[227] eqt(true,tuplenil(H2)) -> F
[228] eqt(undefined,nil) -> F
[229] eqt(undefined,a) -> F
[230] eqt(undefined,tuplenil(H2)) -> F
[231] eqt(pid(N1),nil) -> F
[232] eqt(pid(N1),a) -> F
[233] eqt(pid(N1),excl) -> F
[234] eqt(pid(N1),false) -> F
[235] eqt(pid(N1),lock) -> F
[236] eqt(pid(N1),locker) -> F
[237] eqt(pid(N1),mcrlrecord) -> F
[238] eqt(pid(N1),ok) -> F
[239] eqt(pid(N1),pending) -> F
[240] eqt(pid(N1),release) -> F
[241] eqt(pid(N1),request) -> F
[242] eqt(pid(N1),resource) -> F
[243] eqt(pid(N1),tag) -> F
[244] eqt(pid(N1),true) -> F
[245] eqt(pid(N1),undefined) -> F
[246] eqt(pid(N1),pid(N2)) -> eqt(N1,N2)
[247] eqt(pid(N1),int(N2)) -> F
[248] eqt(pid(N1),cons(H2,T2)) -> F
[249] eqt(pid(N1),tuple(H2,T2)) -> F
[250] eqt(pid(N1),tuplenil(H2)) -> F
[251] eqt(int(N1),nil) -> F
[252] eqt(int(N1),a) -> F
[253] eqt(int(N1),excl) -> F
[254] eqt(int(N1),false) -> F
[255] eqt(int(N1),lock) -> F
[256] eqt(int(N1),locker) -> F
[257] eqt(int(N1),mcrlrecord) -> F
[258] eqt(int(N1),ok) -> F
[259] eqt(int(N1),pending) -> F
[260] eqt(int(N1),release) -> F
[261] eqt(int(N1),request) -> F
[262] eqt(int(N1),resource) -> F
[263] eqt(int(N1),tag) -> F
[264] eqt(int(N1),true) -> F
[265] eqt(int(N1),undefined) -> F
[266] eqt(cons(H1,T1),resource) -> F
[267] eqt(cons(H1,T1),tag) -> F
[268] eqt(cons(H1,T1),true) -> F
[269] eqt(cons(H1,T1),undefined) -> F
[270] eqt(cons(H1,T1),pid(N2)) -> F
[271] eqt(cons(H1,T1),int(N2)) -> F
[272] eqt(cons(H1,T1),cons(H2,T2)) -> and(eqt(H1,H2),eqt(T1,T2))
[273] eqt(cons(H1,T1),tuple(H2,T2)) -> F
[274] eqt(cons(H1,T1),tuplenil(H2)) -> F
[275] eqt(tuple(H1,T1),nil) -> F
[276] eqt(tuple(H1,T1),a) -> F
[277] eqt(tuple(H1,T1),excl) -> F
[278] eqt(tuple(H1,T1),false) -> F
[279] eqt(tuple(H1,T1),lock) -> F
[280] eqt(tuple(H1,T1),locker) -> F
[281] eqt(tuple(H1,T1),mcrlrecord) -> F
[282] eqt(tuple(H1,T1),ok) -> F
[283] eqt(tuple(H1,T1),pending) -> F
[284] eqt(tuple(H1,T1),release) -> F
[285] eqt(tuple(H1,T1),request) -> F
[286] eqt(tuple(H1,T1),resource) -> F
[287] eqt(tuple(H1,T1),tag) -> F
[288] eqt(tuple(H1,T1),true) -> F
[289] eqt(tuple(H1,T1),undefined) -> F
[290] eqt(tuple(H1,T1),pid(N2)) -> F
[291] eqt(tuple(H1,T1),int(N2)) -> F
[292] eqt(tuple(H1,T1),cons(H2,T2)) -> F
[293] eqt(tuple(H1,T1),tuple(H2,T2)) -> and(eqt(H1,H2),eqt(T1,T2))
[294] eqt(tuple(H1,T1),tuplenil(H2)) -> F
[295] eqt(tuplenil(H1),nil) -> F
[296] eqt(tuplenil(H1),a) -> F
[297] eqt(tuplenil(H1),excl) -> F
[298] eqt(tuplenil(H1),false) -> F
[299] eqt(tuplenil(H1),lock) -> F
[300] eqt(tuplenil(H1),locker) -> F
[301] eqt(tuplenil(H1),mcrlrecord) -> F
[302] eqt(tuplenil(H1),ok) -> F
[303] eqt(tuplenil(H1),pending) -> F
[304] eqt(tuplenil(H1),release) -> F
[305] eqt(tuplenil(H1),request) -> F
[306] eqt(tuplenil(H1),resource) -> F
[307] eqt(tuplenil(H1),tag) -> F
[308] eqt(tuplenil(H1),true) -> F
[309] eqt(tuplenil(H1),undefined) -> F
[310] eqt(tuplenil(H1),pid(N2)) -> F
[311] eqt(tuplenil(H1),int(N2)) -> F
[312] eqt(tuplenil(H1),cons(H2,T2)) -> F
[313] eqt(tuplenil(H1),tuple(H2,T2)) -> F
[314] eqt(tuplenil(H1),tuplenil(H2)) -> eqt(H1,H2)
[315] element(int(s(0)),tuplenil(T1)) -> T1
[316] element(int(s(0)),tuple(T1,T2)) -> T1
[317] element(int(s(s(N1))),tuple(T1,T2)) -> element(int(s(N1)),T2)
[318] record_new(lock) ->
 tuple(mcrlrecord,tuple(lock,tuple(undefined,tuple(nil,tuplenil(nil)))))
[319] record_extract(tuple(mcrlrecord,
                      tuple(lock,tuple(F0,tuple(F1,tuplenil(F2))))),lock,
       resource) ->
 tuple(mcrlrecord,tuple(lock,tuple(F0,tuple(F1,tuplenil(F2)))))
[320] 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)))))
[321] record_updates(Record,Name,nil) -> Record
[322] record_updates(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields)) ->
 record_updates(record_update(Record,Name,Field,NewF),Name,Fields)
[323] locker2_map_promote_pending(nil,Pending) -> nil
[324] locker2_map_promote_pending(cons(Lock,Locks),Pending) ->
 cons(locker2_promote_pending(Lock,Pending),
  locker2_map_promote_pending(Locks,Pending))
[325] locker2_map_claim_lock(nil,Resources,Client) -> nil
[326] locker2_map_claim_lock(cons(Lock,Locks),Resources,Client) ->
 cons(locker2_claim_lock(Lock,Resources,Client),
  locker2_map_claim_lock(Locks,Resources,Client))
[327] locker2_map_add_pending(nil,Resources,Client) -> nil
[328] locker2_promote_pending(Lock,Client) ->
 case0(Client,Lock,record_extract(Lock,lock,pending))
[329] case0(Client,Lock,cons(Client,Pendings)) ->
 record_updates(Lock,lock,
  cons(tuple(excl,tuplenil(Client)),
   cons(tuple(pending,tuplenil(Pendings)),nil)))
[330] case0(Client,Lock,MCRLFree0) -> Lock
[331] locker2_remove_pending(Lock,Client) ->
 record_updates(Lock,lock,
  cons(tuple(pending,
        tuplenil(subtract(record_extract(Lock,lock,pending),cons(Client,nil)))),
   nil))
[332] locker2_add_pending(Lock,Resources,Client) ->
 case1(Client,Resources,Lock,
  member(record_extract(Lock,lock,resource),Resources))
[333] case1(Client,Resources,Lock,true) ->
 record_updates(Lock,lock,
  cons(tuple(pending,
        tuplenil(append(record_extract(Lock,lock,pending),cons(Client,nil)))),
   nil))
[334] case1(Client,Resources,Lock,false) -> Lock
[335] locker2_release_lock(Lock,Client) ->
 case2(Client,Lock,gen_modtageq(Client,record_extract(Lock,lock,excl)))
[336] case2(Client,Lock,true) ->
 record_updates(Lock,lock,cons(tuple(excllock,excl),nil))
[337] case4(Client,Lock,MCRLFree1) -> false
[338] locker2_obtainables(nil,Client) -> true
[339] locker2_obtainables(cons(Lock,Locks),Client) ->
 case5(Client,Locks,Lock,member(Client,record_extract(Lock,lock,pending)))
[340] case5(Client,Locks,Lock,true) ->
 andt(locker2_obtainable(Lock,Client),locker2_obtainables(Locks,Client))
[341] case5(Client,Locks,Lock,false) -> locker2_obtainables(Locks,Client)
[342] locker2_check_available(Resource,nil) -> false
[343] locker2_check_available(Resource,cons(Lock,Locks)) ->
 case6(Locks,Lock,Resource,equal(Resource,record_extract(Lock,lock,resource)))
[344] case6(Locks,Lock,Resource,true) ->
 andt(equal(record_extract(Lock,lock,excl),nil),
  equal(record_extract(Lock,lock,pending),nil))
[345] case6(Locks,Lock,Resource,false) ->
 locker2_check_available(Resource,Locks)
[346] locker2_check_availables(nil,Locks) -> true
[347] locker2_check_availables(cons(Resource,Resources),Locks) ->
 andt(locker2_check_available(Resource,Locks),
  locker2_check_availables(Resources,Locks))
[348] locker2_adduniq(nil,List) -> List
[349] append(cons(Head,Tail),List) -> cons(Head,append(Tail,List))
[350] subtract(List,nil) -> List
[351] subtract(List,cons(Head,Tail)) -> subtract(delete(Head,List),Tail)
[352] delete(E,nil) -> nil
[353] delete(E,cons(Head,Tail)) -> case8(Tail,Head,E,equal(E,Head))
[354] case8(Tail,Head,E,true) -> Tail
[355] case8(Tail,Head,E,false) -> cons(Head,delete(E,Tail))
[356] gen_tag(Pid) -> tuple(Pid,tuplenil(tag))
[357] gen_modtageq(Client1,Client2) -> equal(Client1,Client2)
[358] member(E,nil) -> false
[359] member(E,cons(Head,Tail)) -> case9(Tail,Head,E,equal(E,Head))
[360] case9(Tail,Head,E,true) -> true
[361] case9(Tail,Head,E,false) -> member(E,Tail)
[362] eqs(empty,empty) -> T
[363] eqs(empty,stack(E2,S2)) -> F
[364] eqs(stack(E1,S1),empty) -> F
[365] eqs(stack(E1,S1),stack(E2,S2)) -> and(eqt(E1,E2),eqs(S1,S2))
[366] pushs(E1,S1) -> stack(E1,S1)
[367] pops(stack(E1,S1)) -> S1
[368] tops(stack(E1,S1)) -> E1
[369] istops(E1,empty) -> F
[370] istops(E1,stack(E2,S1)) -> eqt(E1,E2)
[371] eqc(nocalls,nocalls) -> T
[372] eqc(nocalls,calls(E2,S2,CS2)) -> F
[373] eqc(calls(E1,S1,CS1),nocalls) -> F
[374] eqc(calls(E1,S1,CS1),calls(E2,S2,CS2)) ->
 and(eqt(E1,E2),and(eqs(S1,S2),eqc(CS1,CS2)))
[375] push(E1,E2,nocalls) -> calls(E1,stack(E2,empty),nocalls)
[376] push(E1,E2,calls(E3,S1,CS1)) -> push1(E1,E2,E3,S1,CS1,eqt(E1,E3))
[377] push1(E1,E2,E3,S1,CS1,T) -> calls(E3,pushs(E2,S1),CS1)
 ,
 CRITERION: MDP
 [ {
      
     DP termination of:
     <Marked_eqt(pid(N1),pid(N2)) , Marked_eqt(N1,N2)>
<Marked_eqt(cons(H1,T1),cons(H2,T2)) , Marked_and(eqt(H1,H2),eqt(T1,T2))>
<Marked_eqt(cons(H1,T1),cons(H2,T2)) , Marked_eqt(H1,H2)>
<Marked_eqt(cons(H1,T1),cons(H2,T2)) , Marked_eqt(T1,T2)>
<Marked_eqt(tuple(H1,T1),tuple(H2,T2)) , Marked_and(eqt(H1,H2),eqt(T1,T2))>
<Marked_eqt(tuple(H1,T1),tuple(H2,T2)) , Marked_eqt(H1,H2)>
<Marked_eqt(tuple(H1,T1),tuple(H2,T2)) , Marked_eqt(T1,T2)>
<Marked_eqt(tuplenil(H1),tuplenil(H2)) , Marked_eqt(H1,H2)>
<Marked_element(int(s(s(N1))),tuple(T1,T2)) , Marked_element(int(s(N1)),T2)>
<Marked_record_updates(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields)) , Marked_record_updates(
                                                                    record_update(
                                                                    Record,
                                                                    Name,
                                                                    Field,
                                                                    NewF),Name,
                                                                    Fields)>
<Marked_record_updates(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields)) , Marked_record_update(
                                                                    Record,
                                                                    Name,Field,
                                                                    NewF)>
<Marked_locker2_map_promote_pending(cons(Lock,Locks),Pending) , Marked_locker2_promote_pending(
                                                                 Lock,
                                                                 Pending)>
<Marked_locker2_map_promote_pending(cons(Lock,Locks),Pending) , Marked_locker2_map_promote_pending(
                                                                 Locks,
                                                                 Pending)>
<Marked_locker2_map_claim_lock(cons(Lock,Locks),Resources,Client) , Marked_locker2_map_claim_lock(
                                                                    Locks,
                                                                    Resources,
                                                                    Client)>
<Marked_locker2_promote_pending(Lock,Client) , Marked_case0(Client,Lock,
                                                record_extract(Lock,lock,
                                                 pending))>
<Marked_locker2_promote_pending(Lock,Client) , Marked_record_extract(
                                                Lock,lock,pending)>
<Marked_case0(Client,Lock,cons(Client,Pendings)) , Marked_record_updates(
                                                    Lock,lock,
                                                    cons(tuple(excl,
                                                          tuplenil(Client)),
                                                     cons(tuple(pending,
                                                           tuplenil(Pendings)),
                                                      nil)))>
<Marked_locker2_remove_pending(Lock,Client) , Marked_record_updates(Lock,
                                               lock,
                                               cons(tuple(pending,
                                                     tuplenil(subtract(
                                                               record_extract(
                                                                Lock,
                                                                lock,
                                                                pending),
                                                               cons(Client,nil)))
                                                      ),nil))>
<Marked_locker2_remove_pending(Lock,Client) , Marked_subtract(record_extract(
                                                               Lock,lock,
                                                               pending),
                                               cons(Client,nil))>
<Marked_locker2_remove_pending(Lock,Client) , Marked_record_extract(Lock,
                                               lock,pending)>
<Marked_locker2_add_pending(Lock,Resources,Client) , Marked_case1(Client,
                                                      Resources,Lock,
                                                      member(record_extract(
                                                              Lock,lock,
                                                              resource),
                                                       Resources))>
<Marked_locker2_add_pending(Lock,Resources,Client) , Marked_member(record_extract(
                                                                    Lock,
                                                                    lock,
                                                                    resource),
                                                      Resources)>
<Marked_locker2_add_pending(Lock,Resources,Client) , Marked_record_extract(
                                                      Lock,lock,resource)>
<Marked_case1(Client,Resources,Lock,true) , Marked_record_updates(Lock,
                                             lock,
                                             cons(tuple(pending,
                                                   tuplenil(append(record_extract(
                                                                    Lock,
                                                                    lock,
                                                                    pending),
                                                             cons(Client,nil)))),
                                              nil))>
<Marked_case1(Client,Resources,Lock,true) , Marked_append(record_extract(
                                                           Lock,lock,
                                                           pending),
                                             cons(Client,nil))>
<Marked_case1(Client,Resources,Lock,true) , Marked_record_extract(Lock,
                                             lock,pending)>
<Marked_locker2_release_lock(Lock,Client) , Marked_case2(Client,Lock,
                                             gen_modtageq(Client,
                                              record_extract(Lock,lock,excl)))>
<Marked_locker2_release_lock(Lock,Client) , Marked_gen_modtageq(Client,
                                             record_extract(Lock,lock,excl))>
<Marked_locker2_release_lock(Lock,Client) , Marked_record_extract(Lock,
                                             lock,excl)>
<Marked_case2(Client,Lock,true) , Marked_record_updates(Lock,lock,
                                   cons(tuple(excllock,excl),nil))>
<Marked_locker2_obtainables(cons(Lock,Locks),Client) , Marked_case5(Client,
                                                        Locks,Lock,
                                                        member(Client,
                                                         record_extract(
                                                          Lock,lock,pending)))>
<Marked_locker2_obtainables(cons(Lock,Locks),Client) , Marked_member(
                                                        Client,
                                                        record_extract(
                                                         Lock,lock,pending))>
<Marked_locker2_obtainables(cons(Lock,Locks),Client) , Marked_record_extract(
                                                        Lock,lock,pending)>
<Marked_case5(Client,Locks,Lock,true) , Marked_locker2_obtainables(Locks,
                                         Client)>
<Marked_case5(Client,Locks,Lock,false) , Marked_locker2_obtainables(Locks,
                                          Client)>
<Marked_locker2_check_available(Resource,cons(Lock,Locks)) , Marked_case6(
                                                              Locks,Lock,
                                                              Resource,
                                                              equal(Resource,
                                                               record_extract(
                                                                Lock,
                                                                lock,
                                                                resource)))>
<Marked_locker2_check_available(Resource,cons(Lock,Locks)) , Marked_record_extract(
                                                              Lock,lock,
                                                              resource)>
<Marked_case6(Locks,Lock,Resource,true) , Marked_record_extract(Lock,lock,excl)>
<Marked_case6(Locks,Lock,Resource,true) , Marked_record_extract(Lock,
                                           lock,pending)>
<Marked_case6(Locks,Lock,Resource,false) , Marked_locker2_check_available(
                                            Resource,Locks)>
<Marked_locker2_check_availables(cons(Resource,Resources),Locks) , Marked_locker2_check_available(
                                                                    Resource,
                                                                    Locks)>
<Marked_locker2_check_availables(cons(Resource,Resources),Locks) , Marked_locker2_check_availables(
                                                                    Resources,
                                                                    Locks)>
<Marked_append(cons(Head,Tail),List) , Marked_append(Tail,List)>
<Marked_subtract(List,cons(Head,Tail)) , Marked_subtract(delete(Head,List),
                                          Tail)>
<Marked_subtract(List,cons(Head,Tail)) , Marked_delete(Head,List)>
<Marked_delete(E,cons(Head,Tail)) , Marked_case8(Tail,Head,E,equal(E,Head))>
<Marked_case8(Tail,Head,E,false) , Marked_delete(E,Tail)>
<Marked_member(E,cons(Head,Tail)) , Marked_case9(Tail,Head,E,equal(E,Head))>
<Marked_case9(Tail,Head,E,false) , Marked_member(E,Tail)>
<Marked_eqs(stack(E1,S1),stack(E2,S2)) , Marked_and(eqt(E1,E2),eqs(S1,S2))>
<Marked_eqs(stack(E1,S1),stack(E2,S2)) , Marked_eqt(E1,E2)>
<Marked_eqs(stack(E1,S1),stack(E2,S2)) , Marked_eqs(S1,S2)>
<Marked_istops(E1,stack(E2,S1)) , Marked_eqt(E1,E2)>
<Marked_eqc(calls(E1,S1,CS1),calls(E2,S2,CS2)) , Marked_and(eqt(E1,E2),
                                                  and(eqs(S1,S2),eqc(CS1,CS2)))>
<Marked_eqc(calls(E1,S1,CS1),calls(E2,S2,CS2)) , Marked_eqt(E1,E2)>
<Marked_eqc(calls(E1,S1,CS1),calls(E2,S2,CS2)) , Marked_and(eqs(S1,S2),
                                                  eqc(CS1,CS2))>
<Marked_eqc(calls(E1,S1,CS1),calls(E2,S2,CS2)) , Marked_eqs(S1,S2)>
<Marked_eqc(calls(E1,S1,CS1),calls(E2,S2,CS2)) , Marked_eqc(CS1,CS2)>
<Marked_push(E1,E2,calls(E3,S1,CS1)) , Marked_push1(E1,E2,E3,S1,CS1,eqt(E1,E3))>
<Marked_push(E1,E2,calls(E3,S1,CS1)) , Marked_eqt(E1,E3)>
<Marked_push1(E1,E2,E3,S1,CS1,T) , Marked_pushs(E2,S1)>
 ,
 CRITERION: SG
 [ {
      
     DP termination of:
     <Marked_element(int(s(s(N1))),tuple(T1,T2)) , Marked_element(int(s(N1)),
                                                    T2)>
 ,
 CRITERION: ST
 [ {
      
     DP termination of:
      ,
      CRITERION: SG
      [  ]} 
      ]} 
{
 
DP termination of:
<Marked_locker2_map_promote_pending(cons(Lock,Locks),Pending) , Marked_locker2_map_promote_pending(
                                                                 Locks,
                                                                 Pending)>
 ,
 CRITERION: ST
 [ {
      
     DP termination of:
      ,
      CRITERION: SG
      [  ]} 
      ]} 
{
 
DP termination of:
<Marked_locker2_map_claim_lock(cons(Lock,Locks),Resources,Client) , Marked_locker2_map_claim_lock(
                                                                    Locks,
                                                                    Resources,
                                                                    Client)>
 ,
 CRITERION: ST
 [ {
      
     DP termination of:
      ,
      CRITERION: SG
      [  ]} 
      ]} 
{
 
DP termination of:
<Marked_record_updates(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields)) , Marked_record_updates(
                                                                    record_update(
                                                                    Record,
                                                                    Name,
                                                                    Field,
                                                                    NewF),Name,
                                                                    Fields)>
 ,
 CRITERION: ST
 [ {
      
     DP termination of:
      ,
      CRITERION: SG
      [  ]} 
      ]} 
{
 
DP termination of:
<Marked_locker2_obtainables(cons(Lock,Locks),Client) , Marked_case5(Client,
                                                        Locks,Lock,
                                                        member(Client,
                                                         record_extract(
                                                          Lock,lock,pending)))>
<Marked_case5(Client,Locks,Lock,true) , Marked_locker2_obtainables(Locks,
                                         Client)>
<Marked_case5(Client,Locks,Lock,false) , Marked_locker2_obtainables(Locks,
                                          Client)>
 ,
 CRITERION: ST
 [ {
      
     DP termination of:
     <Marked_case5(Client,Locks,Lock,false) , Marked_locker2_obtainables(
                                               Locks,Client)>
<Marked_case5(Client,Locks,Lock,true) , Marked_locker2_obtainables(Locks,
                                         Client)>
 ,
 CRITERION: SG
 [  ]} 
 ]} 
{
 
DP termination of:
<Marked_locker2_check_availables(cons(Resource,Resources),Locks) , Marked_locker2_check_availables(
                                                                    Resources,
                                                                    Locks)>
 ,
 CRITERION: ST
 [ {
      
     DP termination of:
      ,
      CRITERION: SG
      [  ]} 
      ]} 
{
 
DP termination of:
<Marked_append(cons(Head,Tail),List) , Marked_append(Tail,List)>
 ,
 CRITERION: ST
 [ {
      
     DP termination of:
      ,
      CRITERION: SG
      [  ]} 
      ]} 
{
 
DP termination of:
<Marked_subtract(List,cons(Head,Tail)) , Marked_subtract(delete(Head,List),
                                          Tail)>
 ,
 CRITERION: ST
 [ {
      
     DP termination of:
      ,
      CRITERION: SG
      [  ]} 
      ]} 
{
 
DP termination of:
<Marked_eqc(calls(E1,S1,CS1),calls(E2,S2,CS2)) , Marked_eqc(CS1,CS2)>
 ,
 CRITERION: ST
 [ {
      
     DP termination of:
      ,
      CRITERION: SG
      [  ]} 
      ]} 
{
 
DP termination of:
<Marked_eqs(stack(E1,S1),stack(E2,S2)) , Marked_eqs(S1,S2)>
 ,
 CRITERION: ST
 [ {
      
     DP termination of:
      ,
      CRITERION: SG
      [  ]} 
      ]} 
{
 
DP termination of:
<Marked_eqt(pid(N1),pid(N2)) , Marked_eqt(N1,N2)>
<Marked_eqt(cons(H1,T1),cons(H2,T2)) , Marked_eqt(H1,H2)>
<Marked_eqt(cons(H1,T1),cons(H2,T2)) , Marked_eqt(T1,T2)>
<Marked_eqt(tuple(H1,T1),tuple(H2,T2)) , Marked_eqt(H1,H2)>
<Marked_eqt(tuple(H1,T1),tuple(H2,T2)) , Marked_eqt(T1,T2)>
<Marked_eqt(tuplenil(H1),tuplenil(H2)) , Marked_eqt(H1,H2)>
 ,
 CRITERION: ST
 [ {
      
     DP termination of:
      ,
      CRITERION: SG
      [  ]} 
      ]} 
 ]} 
 ]} 

Cime worked for 0.211362 seconds (real time)
Cime Exit Status: 0