MAYBE 1110.19/297.17 MAYBE 1110.19/297.17 1110.19/297.17 We are left with following problem, upon which TcT provides the 1110.19/297.17 certificate MAYBE. 1110.19/297.17 1110.19/297.17 Strict Trs: 1110.19/297.17 { or(T(), T()) -> T() 1110.19/297.17 , or(T(), F()) -> T() 1110.19/297.17 , or(F(), T()) -> T() 1110.19/297.17 , or(F(), F()) -> F() 1110.19/297.17 , and(B, T()) -> B 1110.19/297.17 , and(B, F()) -> F() 1110.19/297.17 , and(T(), B) -> B 1110.19/297.17 , and(F(), B) -> F() 1110.19/297.17 , imp(T(), B) -> B 1110.19/297.17 , imp(F(), B) -> T() 1110.19/297.17 , not(T()) -> F() 1110.19/297.17 , not(F()) -> T() 1110.19/297.17 , if(T(), B1, B2) -> B1 1110.19/297.17 , if(F(), B1, B2) -> B2 1110.19/297.17 , eq(T(), T()) -> T() 1110.19/297.17 , eq(T(), F()) -> F() 1110.19/297.17 , eq(F(), T()) -> F() 1110.19/297.17 , eq(F(), F()) -> T() 1110.19/297.17 , eqt(nil(), undefined()) -> F() 1110.19/297.17 , eqt(nil(), pid(N2)) -> F() 1110.19/297.17 , eqt(nil(), int(N2)) -> F() 1110.19/297.17 , eqt(nil(), cons(H2, T2)) -> F() 1110.19/297.17 , eqt(nil(), tuple(H2, T2)) -> F() 1110.19/297.17 , eqt(nil(), tuplenil(H2)) -> F() 1110.19/297.17 , eqt(undefined(), nil()) -> F() 1110.19/297.17 , eqt(undefined(), tuplenil(H2)) -> F() 1110.19/297.17 , eqt(undefined(), a()) -> F() 1110.19/297.17 , eqt(pid(N1), nil()) -> F() 1110.19/297.17 , eqt(pid(N1), undefined()) -> F() 1110.19/297.17 , eqt(pid(N1), pid(N2)) -> eqt(N1, N2) 1110.19/297.17 , eqt(pid(N1), int(N2)) -> F() 1110.19/297.17 , eqt(pid(N1), cons(H2, T2)) -> F() 1110.19/297.17 , eqt(pid(N1), tuple(H2, T2)) -> F() 1110.19/297.17 , eqt(pid(N1), tuplenil(H2)) -> F() 1110.19/297.17 , eqt(pid(N1), a()) -> F() 1110.19/297.17 , eqt(pid(N1), excl()) -> F() 1110.19/297.17 , eqt(pid(N1), false()) -> F() 1110.19/297.17 , eqt(pid(N1), lock()) -> F() 1110.19/297.17 , eqt(pid(N1), locker()) -> F() 1110.19/297.17 , eqt(pid(N1), mcrlrecord()) -> F() 1110.19/297.17 , eqt(pid(N1), ok()) -> F() 1110.19/297.17 , eqt(pid(N1), pending()) -> F() 1110.19/297.17 , eqt(pid(N1), release()) -> F() 1110.19/297.17 , eqt(pid(N1), request()) -> F() 1110.19/297.17 , eqt(pid(N1), resource()) -> F() 1110.19/297.17 , eqt(pid(N1), tag()) -> F() 1110.19/297.17 , eqt(pid(N1), true()) -> F() 1110.19/297.17 , eqt(int(N1), nil()) -> F() 1110.19/297.17 , eqt(int(N1), undefined()) -> F() 1110.19/297.17 , eqt(int(N1), a()) -> F() 1110.19/297.17 , eqt(int(N1), excl()) -> F() 1110.19/297.17 , eqt(int(N1), false()) -> F() 1110.19/297.17 , eqt(int(N1), lock()) -> F() 1110.19/297.17 , eqt(int(N1), locker()) -> F() 1110.19/297.17 , eqt(int(N1), mcrlrecord()) -> F() 1110.19/297.17 , eqt(int(N1), ok()) -> F() 1110.19/297.17 , eqt(int(N1), pending()) -> F() 1110.19/297.17 , eqt(int(N1), release()) -> F() 1110.19/297.17 , eqt(int(N1), request()) -> F() 1110.19/297.17 , eqt(int(N1), resource()) -> F() 1110.19/297.17 , eqt(int(N1), tag()) -> F() 1110.19/297.17 , eqt(int(N1), true()) -> F() 1110.19/297.17 , eqt(cons(H1, T1), undefined()) -> F() 1110.19/297.17 , eqt(cons(H1, T1), pid(N2)) -> F() 1110.19/297.17 , eqt(cons(H1, T1), int(N2)) -> F() 1110.19/297.17 , eqt(cons(H1, T1), cons(H2, T2)) -> and(eqt(H1, H2), eqt(T1, T2)) 1110.19/297.17 , eqt(cons(H1, T1), tuple(H2, T2)) -> F() 1110.19/297.17 , eqt(cons(H1, T1), tuplenil(H2)) -> F() 1110.19/297.17 , eqt(cons(H1, T1), resource()) -> F() 1110.19/297.17 , eqt(cons(H1, T1), tag()) -> F() 1110.19/297.17 , eqt(cons(H1, T1), true()) -> F() 1110.19/297.17 , eqt(tuple(H1, T1), nil()) -> F() 1110.19/297.17 , eqt(tuple(H1, T1), undefined()) -> F() 1110.19/297.17 , eqt(tuple(H1, T1), pid(N2)) -> F() 1110.19/297.17 , eqt(tuple(H1, T1), int(N2)) -> F() 1110.19/297.17 , eqt(tuple(H1, T1), cons(H2, T2)) -> F() 1110.19/297.17 , eqt(tuple(H1, T1), tuple(H2, T2)) -> 1110.19/297.17 and(eqt(H1, H2), eqt(T1, T2)) 1110.19/297.17 , eqt(tuple(H1, T1), tuplenil(H2)) -> F() 1110.19/297.17 , eqt(tuple(H1, T1), a()) -> F() 1110.19/297.17 , eqt(tuple(H1, T1), excl()) -> F() 1110.19/297.17 , eqt(tuple(H1, T1), false()) -> F() 1110.19/297.17 , eqt(tuple(H1, T1), lock()) -> F() 1110.19/297.17 , eqt(tuple(H1, T1), locker()) -> F() 1110.19/297.17 , eqt(tuple(H1, T1), mcrlrecord()) -> F() 1110.19/297.17 , eqt(tuple(H1, T1), ok()) -> F() 1110.19/297.17 , eqt(tuple(H1, T1), pending()) -> F() 1110.19/297.17 , eqt(tuple(H1, T1), release()) -> F() 1110.19/297.17 , eqt(tuple(H1, T1), request()) -> F() 1110.19/297.17 , eqt(tuple(H1, T1), resource()) -> F() 1110.19/297.17 , eqt(tuple(H1, T1), tag()) -> F() 1110.19/297.17 , eqt(tuple(H1, T1), true()) -> F() 1110.19/297.17 , eqt(tuplenil(H1), nil()) -> F() 1110.19/297.17 , eqt(tuplenil(H1), undefined()) -> F() 1110.19/297.17 , eqt(tuplenil(H1), pid(N2)) -> F() 1110.19/297.17 , eqt(tuplenil(H1), int(N2)) -> F() 1110.19/297.17 , eqt(tuplenil(H1), cons(H2, T2)) -> F() 1110.19/297.17 , eqt(tuplenil(H1), tuple(H2, T2)) -> F() 1110.19/297.17 , eqt(tuplenil(H1), tuplenil(H2)) -> eqt(H1, H2) 1110.19/297.17 , eqt(tuplenil(H1), a()) -> F() 1110.19/297.17 , eqt(tuplenil(H1), excl()) -> F() 1110.19/297.17 , eqt(tuplenil(H1), false()) -> F() 1110.19/297.17 , eqt(tuplenil(H1), lock()) -> F() 1110.19/297.17 , eqt(tuplenil(H1), locker()) -> F() 1110.19/297.17 , eqt(tuplenil(H1), mcrlrecord()) -> F() 1110.19/297.17 , eqt(tuplenil(H1), ok()) -> F() 1110.19/297.17 , eqt(tuplenil(H1), pending()) -> F() 1110.19/297.17 , eqt(tuplenil(H1), release()) -> F() 1110.19/297.17 , eqt(tuplenil(H1), request()) -> F() 1110.19/297.17 , eqt(tuplenil(H1), resource()) -> F() 1110.19/297.17 , eqt(tuplenil(H1), tag()) -> F() 1110.19/297.17 , eqt(tuplenil(H1), true()) -> F() 1110.19/297.17 , eqt(a(), nil()) -> F() 1110.19/297.17 , eqt(a(), undefined()) -> F() 1110.19/297.17 , eqt(a(), pid(N2)) -> F() 1110.19/297.17 , eqt(a(), int(N2)) -> F() 1110.19/297.17 , eqt(a(), cons(H2, T2)) -> F() 1110.19/297.17 , eqt(a(), tuple(H2, T2)) -> F() 1110.19/297.17 , eqt(a(), tuplenil(H2)) -> F() 1110.19/297.17 , eqt(a(), a()) -> T() 1110.19/297.17 , eqt(a(), excl()) -> F() 1110.19/297.17 , eqt(a(), false()) -> F() 1110.19/297.17 , eqt(a(), lock()) -> F() 1110.19/297.17 , eqt(a(), locker()) -> F() 1110.19/297.17 , eqt(a(), mcrlrecord()) -> F() 1110.19/297.17 , eqt(a(), ok()) -> F() 1110.19/297.17 , eqt(a(), pending()) -> F() 1110.19/297.17 , eqt(a(), release()) -> F() 1110.19/297.17 , eqt(a(), request()) -> F() 1110.19/297.17 , eqt(a(), resource()) -> F() 1110.19/297.17 , eqt(a(), tag()) -> F() 1110.19/297.17 , eqt(a(), true()) -> F() 1110.19/297.17 , eqt(excl(), eqt(false(), int(N2))) -> F() 1110.19/297.17 , eqt(excl(), nil()) -> F() 1110.19/297.17 , eqt(excl(), undefined()) -> F() 1110.19/297.17 , eqt(excl(), pid(N2)) -> F() 1110.19/297.17 , eqt(excl(), a()) -> F() 1110.19/297.17 , eqt(excl(), excl()) -> T() 1110.19/297.17 , eqt(excl(), false()) -> F() 1110.19/297.17 , eqt(excl(), lock()) -> F() 1110.19/297.17 , eqt(excl(), locker()) -> F() 1110.19/297.17 , eqt(excl(), mcrlrecord()) -> F() 1110.19/297.17 , eqt(excl(), ok()) -> F() 1110.19/297.17 , eqt(excl(), pending()) -> F() 1110.19/297.17 , eqt(excl(), release()) -> F() 1110.19/297.17 , eqt(excl(), request()) -> F() 1110.19/297.17 , eqt(excl(), resource()) -> F() 1110.19/297.17 , eqt(excl(), tag()) -> F() 1110.19/297.17 , eqt(excl(), true()) -> F() 1110.19/297.17 , eqt(false(), cons(H2, T2)) -> F() 1110.19/297.17 , eqt(false(), tuple(H2, T2)) -> F() 1110.19/297.17 , eqt(false(), tuplenil(H2)) -> F() 1110.19/297.17 , eqt(lock(), nil()) -> F() 1110.19/297.17 , eqt(lock(), undefined()) -> F() 1110.19/297.17 , eqt(lock(), pid(N2)) -> F() 1110.19/297.17 , eqt(lock(), int(N2)) -> F() 1110.19/297.17 , eqt(lock(), cons(H2, T2)) -> F() 1110.19/297.17 , eqt(lock(), tuple(H2, T2)) -> F() 1110.19/297.17 , eqt(lock(), tuplenil(H2)) -> F() 1110.19/297.17 , eqt(lock(), a()) -> F() 1110.19/297.17 , eqt(lock(), excl()) -> F() 1110.19/297.17 , eqt(lock(), false()) -> F() 1110.19/297.17 , eqt(lock(), lock()) -> T() 1110.19/297.17 , eqt(lock(), locker()) -> F() 1110.19/297.17 , eqt(lock(), mcrlrecord()) -> F() 1110.19/297.17 , eqt(lock(), ok()) -> F() 1110.19/297.17 , eqt(lock(), pending()) -> F() 1110.19/297.17 , eqt(lock(), release()) -> F() 1110.19/297.17 , eqt(lock(), request()) -> F() 1110.19/297.17 , eqt(lock(), resource()) -> F() 1110.19/297.17 , eqt(lock(), tag()) -> F() 1110.19/297.17 , eqt(lock(), true()) -> F() 1110.19/297.17 , eqt(locker(), nil()) -> F() 1110.19/297.17 , eqt(locker(), undefined()) -> F() 1110.19/297.17 , eqt(locker(), pid(N2)) -> F() 1110.19/297.17 , eqt(locker(), int(N2)) -> F() 1110.19/297.17 , eqt(locker(), cons(H2, T2)) -> F() 1110.19/297.17 , eqt(locker(), tuple(H2, T2)) -> F() 1110.19/297.17 , eqt(locker(), tuplenil(H2)) -> F() 1110.19/297.17 , eqt(locker(), a()) -> F() 1110.19/297.17 , eqt(locker(), excl()) -> F() 1110.19/297.17 , eqt(locker(), false()) -> F() 1110.19/297.17 , eqt(locker(), lock()) -> F() 1110.19/297.17 , eqt(locker(), locker()) -> T() 1110.19/297.17 , eqt(locker(), mcrlrecord()) -> F() 1110.19/297.17 , eqt(locker(), ok()) -> F() 1110.19/297.17 , eqt(locker(), pending()) -> F() 1110.19/297.17 , eqt(locker(), release()) -> F() 1110.19/297.17 , eqt(locker(), request()) -> F() 1110.19/297.17 , eqt(locker(), resource()) -> F() 1110.19/297.17 , eqt(locker(), tag()) -> F() 1110.19/297.17 , eqt(locker(), true()) -> F() 1110.19/297.17 , eqt(mcrlrecord(), nil()) -> F() 1110.19/297.17 , eqt(mcrlrecord(), a()) -> F() 1110.19/297.17 , eqt(mcrlrecord(), excl()) -> F() 1110.19/297.17 , eqt(mcrlrecord(), false()) -> F() 1110.19/297.17 , eqt(mcrlrecord(), lock()) -> F() 1110.19/297.17 , eqt(mcrlrecord(), locker()) -> F() 1110.19/297.17 , eqt(mcrlrecord(), mcrlrecord()) -> T() 1110.19/297.17 , eqt(mcrlrecord(), ok()) -> F() 1110.19/297.17 , eqt(mcrlrecord(), pending()) -> F() 1110.19/297.17 , eqt(mcrlrecord(), release()) -> F() 1110.19/297.17 , eqt(mcrlrecord(), request()) -> F() 1110.19/297.17 , eqt(mcrlrecord(), resource()) -> F() 1110.19/297.17 , eqt(ok(), undefined()) -> F() 1110.19/297.17 , eqt(ok(), pid(N2)) -> F() 1110.19/297.17 , eqt(ok(), int(N2)) -> F() 1110.19/297.17 , eqt(ok(), cons(H2, T2)) -> F() 1110.19/297.17 , eqt(ok(), tuple(H2, T2)) -> F() 1110.19/297.17 , eqt(ok(), tuplenil(H2)) -> F() 1110.19/297.17 , eqt(ok(), resource()) -> F() 1110.19/297.17 , eqt(ok(), tag()) -> F() 1110.19/297.17 , eqt(ok(), true()) -> F() 1110.19/297.17 , eqt(pending(), nil()) -> F() 1110.19/297.17 , eqt(pending(), undefined()) -> F() 1110.19/297.17 , eqt(pending(), pid(N2)) -> F() 1110.19/297.17 , eqt(pending(), int(N2)) -> F() 1110.19/297.17 , eqt(pending(), cons(H2, T2)) -> F() 1110.19/297.17 , eqt(pending(), tuple(H2, T2)) -> F() 1110.19/297.17 , eqt(pending(), tuplenil(H2)) -> F() 1110.19/297.17 , eqt(pending(), a()) -> F() 1110.19/297.17 , eqt(pending(), excl()) -> F() 1110.19/297.17 , eqt(pending(), false()) -> F() 1110.19/297.17 , eqt(pending(), lock()) -> F() 1110.19/297.17 , eqt(pending(), locker()) -> F() 1110.19/297.17 , eqt(pending(), mcrlrecord()) -> F() 1110.19/297.17 , eqt(pending(), ok()) -> F() 1110.19/297.17 , eqt(pending(), pending()) -> T() 1110.19/297.17 , eqt(pending(), release()) -> F() 1110.19/297.17 , eqt(pending(), request()) -> F() 1110.19/297.17 , eqt(pending(), resource()) -> F() 1110.19/297.17 , eqt(pending(), tag()) -> F() 1110.19/297.17 , eqt(pending(), true()) -> F() 1110.19/297.17 , eqt(release(), nil()) -> F() 1110.19/297.17 , eqt(release(), a()) -> F() 1110.19/297.17 , eqt(release(), excl()) -> F() 1110.19/297.17 , eqt(release(), false()) -> F() 1110.19/297.17 , eqt(release(), lock()) -> F() 1110.19/297.17 , eqt(release(), locker()) -> F() 1110.19/297.17 , eqt(release(), mcrlrecord()) -> F() 1110.19/297.17 , eqt(release(), ok()) -> F() 1110.19/297.17 , eqt(request(), undefined()) -> F() 1110.19/297.17 , eqt(request(), pid(N2)) -> F() 1110.19/297.17 , eqt(request(), int(N2)) -> F() 1110.19/297.17 , eqt(request(), cons(H2, T2)) -> F() 1110.19/297.17 , eqt(request(), tuple(H2, T2)) -> F() 1110.19/297.17 , eqt(request(), tuplenil(H2)) -> F() 1110.19/297.17 , eqt(request(), mcrlrecord()) -> F() 1110.19/297.17 , eqt(request(), ok()) -> F() 1110.19/297.17 , eqt(request(), pending()) -> F() 1110.19/297.17 , eqt(request(), release()) -> F() 1110.19/297.17 , eqt(request(), request()) -> T() 1110.19/297.17 , eqt(request(), resource()) -> F() 1110.19/297.17 , eqt(request(), tag()) -> F() 1110.19/297.17 , eqt(request(), true()) -> F() 1110.19/297.17 , eqt(resource(), nil()) -> F() 1110.19/297.17 , eqt(resource(), undefined()) -> F() 1110.19/297.17 , eqt(resource(), pid(N2)) -> F() 1110.19/297.17 , eqt(resource(), int(N2)) -> F() 1110.19/297.17 , eqt(resource(), cons(H2, T2)) -> F() 1110.19/297.17 , eqt(resource(), tuple(H2, T2)) -> F() 1110.19/297.17 , eqt(resource(), tuplenil(H2)) -> F() 1110.19/297.17 , eqt(resource(), a()) -> F() 1110.19/297.17 , eqt(resource(), excl()) -> F() 1110.19/297.17 , eqt(resource(), false()) -> F() 1110.19/297.17 , eqt(resource(), lock()) -> F() 1110.19/297.17 , eqt(resource(), locker()) -> F() 1110.19/297.17 , eqt(resource(), mcrlrecord()) -> F() 1110.19/297.17 , eqt(resource(), ok()) -> F() 1110.19/297.17 , eqt(resource(), pending()) -> F() 1110.19/297.17 , eqt(resource(), release()) -> F() 1110.19/297.17 , eqt(resource(), request()) -> F() 1110.19/297.17 , eqt(resource(), resource()) -> T() 1110.19/297.17 , eqt(resource(), tag()) -> F() 1110.19/297.17 , eqt(resource(), true()) -> F() 1110.19/297.17 , eqt(tag(), nil()) -> F() 1110.19/297.17 , eqt(tag(), undefined()) -> F() 1110.19/297.17 , eqt(tag(), pid(N2)) -> F() 1110.19/297.17 , eqt(tag(), int(N2)) -> F() 1110.19/297.17 , eqt(tag(), cons(H2, T2)) -> F() 1110.19/297.17 , eqt(tag(), tuple(H2, T2)) -> F() 1110.19/297.17 , eqt(tag(), tuplenil(H2)) -> F() 1110.19/297.17 , eqt(tag(), a()) -> F() 1110.19/297.17 , eqt(tag(), excl()) -> F() 1110.19/297.17 , eqt(tag(), false()) -> F() 1110.19/297.17 , eqt(tag(), lock()) -> F() 1110.19/297.17 , eqt(tag(), locker()) -> F() 1110.19/297.17 , eqt(tag(), mcrlrecord()) -> F() 1110.19/297.17 , eqt(tag(), ok()) -> F() 1110.19/297.17 , eqt(tag(), pending()) -> F() 1110.19/297.17 , eqt(tag(), release()) -> F() 1110.19/297.17 , eqt(tag(), request()) -> F() 1110.19/297.17 , eqt(tag(), resource()) -> F() 1110.19/297.17 , eqt(tag(), tag()) -> T() 1110.19/297.17 , eqt(tag(), true()) -> F() 1110.19/297.17 , eqt(true(), nil()) -> F() 1110.19/297.17 , eqt(true(), undefined()) -> F() 1110.19/297.17 , eqt(true(), pid(N2)) -> F() 1110.19/297.17 , eqt(true(), int(N2)) -> F() 1110.19/297.17 , eqt(true(), cons(H2, T2)) -> F() 1110.19/297.17 , eqt(true(), tuple(H2, T2)) -> F() 1110.19/297.17 , eqt(true(), tuplenil(H2)) -> F() 1110.19/297.17 , eqt(true(), a()) -> F() 1110.19/297.17 , eqt(true(), excl()) -> F() 1110.19/297.17 , eqt(true(), false()) -> F() 1110.19/297.17 , eqt(true(), lock()) -> F() 1110.19/297.17 , eqt(true(), locker()) -> F() 1110.19/297.17 , eqt(true(), mcrlrecord()) -> F() 1110.19/297.17 , eqt(true(), ok()) -> F() 1110.19/297.17 , eqt(true(), pending()) -> F() 1110.19/297.17 , eqt(true(), release()) -> F() 1110.19/297.17 , eqt(true(), request()) -> F() 1110.19/297.17 , eqt(true(), resource()) -> F() 1110.19/297.17 , eqt(true(), tag()) -> F() 1110.19/297.17 , eqt(true(), true()) -> T() 1110.19/297.17 , element(int(s(s(N1))), tuple(T1, T2)) -> element(int(s(N1)), T2) 1110.19/297.17 , element(int(s(0())), tuple(T1, T2)) -> T1 1110.19/297.17 , element(int(s(0())), tuplenil(T1)) -> T1 1110.19/297.17 , record_new(lock()) -> 1110.19/297.17 tuple(mcrlrecord(), 1110.19/297.17 tuple(lock(), tuple(undefined(), tuple(nil(), tuplenil(nil()))))) 1110.19/297.17 , record_extract(tuple(mcrlrecord(), 1110.19/297.17 tuple(lock(), tuple(F0, tuple(F1, tuplenil(F2))))), 1110.19/297.17 lock(), 1110.19/297.17 resource()) 1110.19/297.17 -> 1110.19/297.17 tuple(mcrlrecord(), 1110.19/297.17 tuple(lock(), tuple(F0, tuple(F1, tuplenil(F2))))) 1110.19/297.17 , record_update(tuple(mcrlrecord(), 1110.19/297.17 tuple(lock(), tuple(F0, tuple(F1, tuplenil(F2))))), 1110.19/297.17 lock(), 1110.19/297.17 pending(), 1110.19/297.17 NewF) 1110.19/297.17 -> 1110.19/297.17 tuple(mcrlrecord(), 1110.19/297.17 tuple(lock(), tuple(F0, tuple(F1, tuplenil(NewF))))) 1110.19/297.17 , record_updates(Record, Name, nil()) -> Record 1110.19/297.17 , record_updates(Record, 1110.19/297.17 Name, 1110.19/297.17 cons(tuple(Field, tuplenil(NewF)), Fields)) 1110.19/297.17 -> 1110.19/297.17 record_updates(record_update(Record, Name, Field, NewF), 1110.19/297.17 Name, 1110.19/297.17 Fields) 1110.19/297.17 , locker2_map_promote_pending(nil(), Pending) -> nil() 1110.19/297.17 , locker2_map_promote_pending(cons(Lock, Locks), Pending) -> 1110.19/297.17 cons(locker2_promote_pending(Lock, Pending), 1110.19/297.17 locker2_map_promote_pending(Locks, Pending)) 1110.19/297.17 , locker2_promote_pending(Lock, Client) -> 1110.19/297.17 case0(Client, Lock, record_extract(Lock, lock(), pending())) 1110.19/297.17 , locker2_map_claim_lock(nil(), Resources, Client) -> nil() 1110.19/297.17 , locker2_map_claim_lock(cons(Lock, Locks), Resources, Client) -> 1110.19/297.17 cons(locker2_claim_lock(Lock, Resources, Client), 1110.19/297.17 locker2_map_claim_lock(Locks, Resources, Client)) 1110.19/297.17 , locker2_map_add_pending(nil(), Resources, Client) -> nil() 1110.19/297.17 , case0(Client, Lock, MCRLFree0) -> Lock 1110.19/297.17 , case0(Client, Lock, cons(Client, Pendings)) -> 1110.19/297.17 record_updates(Lock, 1110.19/297.17 lock(), 1110.19/297.17 cons(tuple(excl(), tuplenil(Client)), 1110.19/297.17 cons(tuple(pending(), tuplenil(Pendings)), nil()))) 1110.19/297.17 , locker2_remove_pending(Lock, Client) -> 1110.19/297.17 record_updates(Lock, 1110.19/297.17 lock(), 1110.19/297.17 cons(tuple(pending(), 1110.19/297.17 tuplenil(subtract(record_extract(Lock, lock(), pending()), 1110.19/297.17 cons(Client, nil())))), 1110.19/297.17 nil())) 1110.19/297.17 , subtract(List, nil()) -> List 1110.19/297.17 , subtract(List, cons(Head, Tail)) -> 1110.19/297.17 subtract(delete(Head, List), Tail) 1110.19/297.17 , locker2_add_pending(Lock, Resources, Client) -> 1110.19/297.17 case1(Client, 1110.19/297.17 Resources, 1110.19/297.17 Lock, 1110.19/297.17 member(record_extract(Lock, lock(), resource()), Resources)) 1110.19/297.17 , case1(Client, Resources, Lock, false()) -> Lock 1110.19/297.17 , case1(Client, Resources, Lock, true()) -> 1110.19/297.17 record_updates(Lock, 1110.19/297.17 lock(), 1110.19/297.17 cons(tuple(pending(), 1110.19/297.17 tuplenil(append(record_extract(Lock, lock(), pending()), 1110.19/297.17 cons(Client, nil())))), 1110.19/297.17 nil())) 1110.19/297.17 , member(E, nil()) -> false() 1110.19/297.17 , member(E, cons(Head, Tail)) -> 1110.19/297.17 case9(Tail, Head, E, equal(E, Head)) 1110.19/297.17 , append(cons(Head, Tail), List) -> cons(Head, append(Tail, List)) 1110.19/297.17 , locker2_release_lock(Lock, Client) -> 1110.19/297.17 case2(Client, 1110.19/297.17 Lock, 1110.19/297.17 gen_modtageq(Client, record_extract(Lock, lock(), excl()))) 1110.19/297.17 , case2(Client, Lock, true()) -> 1110.19/297.17 record_updates(Lock, 1110.19/297.17 lock(), 1110.19/297.17 cons(tuple(excllock(), excl()), nil())) 1110.19/297.17 , gen_modtageq(Client1, Client2) -> equal(Client1, Client2) 1110.19/297.17 , case4(Client, Lock, MCRLFree1) -> false() 1110.19/297.17 , locker2_obtainables(nil(), Client) -> true() 1110.19/297.17 , locker2_obtainables(cons(Lock, Locks), Client) -> 1110.19/297.17 case5(Client, 1110.19/297.17 Locks, 1110.19/297.17 Lock, 1110.19/297.17 member(Client, record_extract(Lock, lock(), pending()))) 1110.19/297.17 , case5(Client, Locks, Lock, false()) -> 1110.19/297.17 locker2_obtainables(Locks, Client) 1110.19/297.17 , case5(Client, Locks, Lock, true()) -> 1110.19/297.17 andt(locker2_obtainable(Lock, Client), 1110.19/297.17 locker2_obtainables(Locks, Client)) 1110.19/297.17 , locker2_check_available(Resource, nil()) -> false() 1110.19/297.17 , locker2_check_available(Resource, cons(Lock, Locks)) -> 1110.19/297.17 case6(Locks, 1110.19/297.17 Lock, 1110.19/297.17 Resource, 1110.19/297.17 equal(Resource, record_extract(Lock, lock(), resource()))) 1110.19/297.17 , case6(Locks, Lock, Resource, false()) -> 1110.19/297.17 locker2_check_available(Resource, Locks) 1110.19/297.17 , case6(Locks, Lock, Resource, true()) -> 1110.19/297.17 andt(equal(record_extract(Lock, lock(), excl()), nil()), 1110.19/297.17 equal(record_extract(Lock, lock(), pending()), nil())) 1110.19/297.17 , locker2_check_availables(nil(), Locks) -> true() 1110.19/297.17 , locker2_check_availables(cons(Resource, Resources), Locks) -> 1110.19/297.17 andt(locker2_check_available(Resource, Locks), 1110.19/297.17 locker2_check_availables(Resources, Locks)) 1110.19/297.17 , locker2_adduniq(nil(), List) -> List 1110.19/297.17 , delete(E, nil()) -> nil() 1110.19/297.17 , delete(E, cons(Head, Tail)) -> 1110.19/297.17 case8(Tail, Head, E, equal(E, Head)) 1110.19/297.17 , case8(Tail, Head, E, false()) -> cons(Head, delete(E, Tail)) 1110.19/297.17 , case8(Tail, Head, E, true()) -> Tail 1110.19/297.17 , gen_tag(Pid) -> tuple(Pid, tuplenil(tag())) 1110.19/297.17 , case9(Tail, Head, E, false()) -> member(E, Tail) 1110.19/297.17 , case9(Tail, Head, E, true()) -> true() 1110.19/297.17 , eqs(empty(), empty()) -> T() 1110.19/297.17 , eqs(empty(), stack(E2, S2)) -> F() 1110.19/297.17 , eqs(stack(E1, S1), empty()) -> F() 1110.19/297.17 , eqs(stack(E1, S1), stack(E2, S2)) -> 1110.19/297.17 and(eqt(E1, E2), eqs(S1, S2)) 1110.19/297.17 , pushs(E1, S1) -> stack(E1, S1) 1110.19/297.17 , pops(stack(E1, S1)) -> S1 1110.19/297.17 , tops(stack(E1, S1)) -> E1 1110.19/297.17 , istops(E1, empty()) -> F() 1110.19/297.17 , istops(E1, stack(E2, S1)) -> eqt(E1, E2) 1110.19/297.17 , eqc(nocalls(), nocalls()) -> T() 1110.19/297.17 , eqc(nocalls(), calls(E2, S2, CS2)) -> F() 1110.19/297.17 , eqc(calls(E1, S1, CS1), nocalls()) -> F() 1110.19/297.17 , eqc(calls(E1, S1, CS1), calls(E2, S2, CS2)) -> 1110.19/297.17 and(eqt(E1, E2), and(eqs(S1, S2), eqc(CS1, CS2))) 1110.19/297.17 , push(E1, E2, nocalls()) -> 1110.19/297.17 calls(E1, stack(E2, empty()), nocalls()) 1110.19/297.17 , push(E1, E2, calls(E3, S1, CS1)) -> 1110.19/297.17 push1(E1, E2, E3, S1, CS1, eqt(E1, E3)) 1110.19/297.17 , push1(E1, E2, E3, S1, CS1, T()) -> 1110.19/297.17 calls(E3, pushs(E2, S1), CS1) } 1110.19/297.17 Obligation: 1110.19/297.17 runtime complexity 1110.19/297.17 Answer: 1110.19/297.17 MAYBE 1110.19/297.17 1110.19/297.17 None of the processors succeeded. 1110.19/297.17 1110.19/297.17 Details of failed attempt(s): 1110.19/297.17 ----------------------------- 1110.19/297.17 1) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 1110.19/297.17 the following reason: 1110.19/297.17 1110.19/297.17 Computation stopped due to timeout after 297.0 seconds. 1110.19/297.17 1110.19/297.17 2) 'With Problem ... (timeout of 297 seconds)' failed due to the 1110.19/297.17 following reason: 1110.19/297.17 1110.19/297.17 Computation stopped due to timeout after 297.0 seconds. 1110.19/297.17 1110.19/297.17 3) 'Best' failed due to the following reason: 1110.19/297.17 1110.19/297.17 None of the processors succeeded. 1110.19/297.17 1110.19/297.17 Details of failed attempt(s): 1110.19/297.17 ----------------------------- 1110.19/297.17 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1110.19/297.17 seconds)' failed due to the following reason: 1110.19/297.17 1110.19/297.17 Computation stopped due to timeout after 148.0 seconds. 1110.19/297.17 1110.19/297.17 2) 'Best' failed due to the following reason: 1110.19/297.17 1110.19/297.17 None of the processors succeeded. 1110.19/297.17 1110.19/297.17 Details of failed attempt(s): 1110.19/297.17 ----------------------------- 1110.19/297.17 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1110.19/297.17 following reason: 1110.19/297.17 1110.19/297.17 The processor is inapplicable, reason: 1110.19/297.17 Processor only applicable for innermost runtime complexity analysis 1110.19/297.17 1110.19/297.17 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1110.19/297.17 to the following reason: 1110.19/297.17 1110.19/297.17 The processor is inapplicable, reason: 1110.19/297.17 Processor only applicable for innermost runtime complexity analysis 1110.19/297.17 1110.19/297.17 1110.19/297.17 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1110.19/297.17 failed due to the following reason: 1110.19/297.17 1110.19/297.17 None of the processors succeeded. 1110.19/297.17 1110.19/297.17 Details of failed attempt(s): 1110.19/297.17 ----------------------------- 1110.19/297.17 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 1110.19/297.17 failed due to the following reason: 1110.19/297.17 1110.19/297.17 match-boundness of the problem could not be verified. 1110.19/297.17 1110.19/297.17 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1110.19/297.17 failed due to the following reason: 1110.19/297.17 1110.19/297.17 match-boundness of the problem could not be verified. 1110.19/297.17 1110.19/297.17 1110.19/297.17 1110.19/297.17 1110.19/297.17 Arrrr.. 1110.66/297.41 EOF