(STRATEGY
    INNERMOST)

(VAR
    B B1 B2 CS1 CS2 Client Client1
    Client2 E E1 E2 E3 F0 F1 F2
    Field Fields H1 H2 Head List
    Lock Locks MCRLFree0 MCRLFree1
    N1 N2 Name NewF Pending Pendings
    Pid Record Resource Resources S1
    S2 T1 T2 Tail)
(DATATYPES
    A = µX.< T, F, nil, undefined, pid(X), int(X), cons(X, X), tuple(X, X), tuplenil(X), a, excl, false, lock, locker, mcrlrecord, ok, pending, release, request, resource, tag, true, s(X), 0, locker2_claim_lock(X, X, X), excllock, andt(X, X), locker2_obtainable(X, X), equal(X, X), empty, stack(X, X), nocalls, calls(X, X, X) >)
(SIGNATURES
    or :: [A x A] -> A
    and :: [A x A] -> A
    imp :: [A x A] -> A
    not :: [A] -> A
    if :: [A x A x A] -> A
    eq :: [A x A] -> A
    eqt :: [A x A] -> A
    element :: [A x A] -> A
    record_new :: [A] -> A
    record_extract :: [A x A x A] -> A
    record_update :: [A x A x A x A] -> A
    record_updates :: [A x A x A] -> A
    locker2_map_promote_pending :: [A x A] -> A
    locker2_map_claim_lock :: [A x A x A] -> A
    locker2_map_add_pending :: [A x A x A] -> A
    locker2_promote_pending :: [A x A] -> A
    case0 :: [A x A x A] -> A
    locker2_remove_pending :: [A x A] -> A
    locker2_add_pending :: [A x A x A] -> A
    case1 :: [A x A x A x A] -> A
    locker2_release_lock :: [A x A] -> A
    case2 :: [A x A x A] -> A
    case4 :: [A x A x A] -> A
    locker2_obtainables :: [A x A] -> A
    case5 :: [A x A x A x A] -> A
    locker2_check_available :: [A x A] -> A
    case6 :: [A x A x A x A] -> A
    locker2_check_availables :: [A x A] -> A
    locker2_adduniq :: [A x A] -> A
    append :: [A x A] -> A
    subtract :: [A x A] -> A
    delete :: [A x A] -> A
    case8 :: [A x A x A x A] -> A
    gen_tag :: [A] -> A
    gen_modtageq :: [A x A] -> A
    member :: [A x A] -> A
    case9 :: [A x A x A x A] -> A
    eqs :: [A x A] -> A
    pushs :: [A x A] -> A
    pops :: [A] -> A
    tops :: [A] -> A
    istops :: [A x A] -> A
    eqc :: [A x A] -> A
    push :: [A x A x A] -> A
    push1 :: [A x A x A x A x A x A] -> A)
(RULES
    or(T(),T()) -> T()
    or(F(),T()) -> T()
    or(T(),F()) -> T()
    or(F(),F()) -> F()
    and(T(),B) -> B
    and(B,T()) -> B
    and(F(),B) -> F()
    and(B,F()) -> F()
    imp(T(),B) -> B
    imp(F(),B) -> T()
    not(T()) -> F()
    not(F()) -> T()
    if(T(),B1,B2) -> B1
    if(F(),B1,B2) -> B2
    eq(T(),T()) -> T()
    eq(F(),F()) -> T()
    eq(T(),F()) -> F()
    eq(F(),T()) -> F()
    eqt(nil(),undefined()) -> F()
    eqt(nil(),pid(N2)) -> F()
    eqt(nil(),int(N2)) -> F()
    eqt(nil(),cons(H2,T2)) -> F()
    eqt(nil(),tuple(H2,T2)) -> F()
    eqt(nil(),tuplenil(H2)) -> F()
    eqt(a(),nil()) -> F()
    eqt(a(),a()) -> T()
    eqt(a(),excl()) -> F()
    eqt(a(),false()) -> F()
    eqt(a(),lock()) -> F()
    eqt(a(),locker()) -> F()
    eqt(a(),mcrlrecord()) -> F()
    eqt(a(),ok()) -> F()
    eqt(a(),pending()) -> F()
    eqt(a(),release()) -> F()
    eqt(a(),request()) -> F()
    eqt(a(),resource()) -> F()
    eqt(a(),tag()) -> F()
    eqt(a(),true()) -> F()
    eqt(a(),undefined()) -> F()
    eqt(a(),pid(N2)) -> F()
    eqt(a(),int(N2)) -> F()
    eqt(a(),cons(H2,T2)) -> F()
    eqt(a(),tuple(H2,T2)) -> F()
    eqt(a(),tuplenil(H2)) -> F()
    eqt(excl(),nil()) -> F()
    eqt(excl(),a()) -> F()
    eqt(excl(),excl()) -> T()
    eqt(excl(),false()) -> F()
    eqt(excl(),lock()) -> F()
    eqt(excl(),locker()) -> F()
    eqt(excl(),mcrlrecord()) -> F()
    eqt(excl(),ok()) -> F()
    eqt(excl(),pending()) -> F()
    eqt(excl(),release()) -> F()
    eqt(excl(),request()) -> F()
    eqt(excl(),resource()) -> F()
    eqt(excl(),tag()) -> F()
    eqt(excl(),true()) -> F()
    eqt(excl(),undefined()) -> F()
    eqt(excl(),pid(N2)) -> F()
    eqt(excl()
       ,eqt(false(),int(N2))) -> F()
    eqt(false(),cons(H2,T2)) -> F()
    eqt(false(),tuple(H2,T2)) -> F()
    eqt(false(),tuplenil(H2)) -> F()
    eqt(lock(),nil()) -> F()
    eqt(lock(),a()) -> F()
    eqt(lock(),excl()) -> F()
    eqt(lock(),false()) -> F()
    eqt(lock(),lock()) -> T()
    eqt(lock(),locker()) -> F()
    eqt(lock(),mcrlrecord()) -> F()
    eqt(lock(),ok()) -> F()
    eqt(lock(),pending()) -> F()
    eqt(lock(),release()) -> F()
    eqt(lock(),request()) -> F()
    eqt(lock(),resource()) -> F()
    eqt(lock(),tag()) -> F()
    eqt(lock(),true()) -> F()
    eqt(lock(),undefined()) -> F()
    eqt(lock(),pid(N2)) -> F()
    eqt(lock(),int(N2)) -> F()
    eqt(lock(),cons(H2,T2)) -> F()
    eqt(lock(),tuple(H2,T2)) -> F()
    eqt(lock(),tuplenil(H2)) -> F()
    eqt(locker(),nil()) -> F()
    eqt(locker(),a()) -> F()
    eqt(locker(),excl()) -> F()
    eqt(locker(),false()) -> F()
    eqt(locker(),lock()) -> F()
    eqt(locker(),locker()) -> T()
    eqt(locker(),mcrlrecord()) ->
      F()
    eqt(locker(),ok()) -> F()
    eqt(locker(),pending()) -> F()
    eqt(locker(),release()) -> F()
    eqt(locker(),request()) -> F()
    eqt(locker(),resource()) -> F()
    eqt(locker(),tag()) -> F()
    eqt(locker(),true()) -> F()
    eqt(locker(),undefined()) -> F()
    eqt(locker(),pid(N2)) -> F()
    eqt(locker(),int(N2)) -> F()
    eqt(locker(),cons(H2,T2)) -> F()
    eqt(locker(),tuple(H2,T2)) ->
      F()
    eqt(locker(),tuplenil(H2)) ->
      F()
    eqt(mcrlrecord(),nil()) -> F()
    eqt(mcrlrecord(),a()) -> F()
    eqt(mcrlrecord(),excl()) -> F()
    eqt(mcrlrecord(),false()) -> F()
    eqt(mcrlrecord(),lock()) -> F()
    eqt(mcrlrecord(),locker()) ->
      F()
    eqt(mcrlrecord()
       ,mcrlrecord()) -> T()
    eqt(mcrlrecord(),ok()) -> F()
    eqt(mcrlrecord(),pending()) ->
      F()
    eqt(mcrlrecord(),release()) ->
      F()
    eqt(mcrlrecord(),request()) ->
      F()
    eqt(mcrlrecord(),resource()) ->
      F()
    eqt(ok(),resource()) -> F()
    eqt(ok(),tag()) -> F()
    eqt(ok(),true()) -> F()
    eqt(ok(),undefined()) -> F()
    eqt(ok(),pid(N2)) -> F()
    eqt(ok(),int(N2)) -> F()
    eqt(ok(),cons(H2,T2)) -> F()
    eqt(ok(),tuple(H2,T2)) -> F()
    eqt(ok(),tuplenil(H2)) -> F()
    eqt(pending(),nil()) -> F()
    eqt(pending(),a()) -> F()
    eqt(pending(),excl()) -> F()
    eqt(pending(),false()) -> F()
    eqt(pending(),lock()) -> F()
    eqt(pending(),locker()) -> F()
    eqt(pending(),mcrlrecord()) ->
      F()
    eqt(pending(),ok()) -> F()
    eqt(pending(),pending()) -> T()
    eqt(pending(),release()) -> F()
    eqt(pending(),request()) -> F()
    eqt(pending(),resource()) -> F()
    eqt(pending(),tag()) -> F()
    eqt(pending(),true()) -> F()
    eqt(pending(),undefined()) ->
      F()
    eqt(pending(),pid(N2)) -> F()
    eqt(pending(),int(N2)) -> F()
    eqt(pending(),cons(H2,T2)) ->
      F()
    eqt(pending(),tuple(H2,T2)) ->
      F()
    eqt(pending(),tuplenil(H2)) ->
      F()
    eqt(release(),nil()) -> F()
    eqt(release(),a()) -> F()
    eqt(release(),excl()) -> F()
    eqt(release(),false()) -> F()
    eqt(release(),lock()) -> F()
    eqt(release(),locker()) -> F()
    eqt(release(),mcrlrecord()) ->
      F()
    eqt(release(),ok()) -> F()
    eqt(request(),mcrlrecord()) ->
      F()
    eqt(request(),ok()) -> F()
    eqt(request(),pending()) -> F()
    eqt(request(),release()) -> F()
    eqt(request(),request()) -> T()
    eqt(request(),resource()) -> F()
    eqt(request(),tag()) -> F()
    eqt(request(),true()) -> F()
    eqt(request(),undefined()) ->
      F()
    eqt(request(),pid(N2)) -> F()
    eqt(request(),int(N2)) -> F()
    eqt(request(),cons(H2,T2)) ->
      F()
    eqt(request(),tuple(H2,T2)) ->
      F()
    eqt(request(),tuplenil(H2)) ->
      F()
    eqt(resource(),nil()) -> F()
    eqt(resource(),a()) -> F()
    eqt(resource(),excl()) -> F()
    eqt(resource(),false()) -> F()
    eqt(resource(),lock()) -> F()
    eqt(resource(),locker()) -> F()
    eqt(resource(),mcrlrecord()) ->
      F()
    eqt(resource(),ok()) -> F()
    eqt(resource(),pending()) -> F()
    eqt(resource(),release()) -> F()
    eqt(resource(),request()) -> F()
    eqt(resource(),resource()) ->
      T()
    eqt(resource(),tag()) -> F()
    eqt(resource(),true()) -> F()
    eqt(resource(),undefined()) ->
      F()
    eqt(resource(),pid(N2)) -> F()
    eqt(resource(),int(N2)) -> F()
    eqt(resource(),cons(H2,T2)) ->
      F()
    eqt(resource(),tuple(H2,T2)) ->
      F()
    eqt(resource(),tuplenil(H2)) ->
      F()
    eqt(tag(),nil()) -> F()
    eqt(tag(),a()) -> F()
    eqt(tag(),excl()) -> F()
    eqt(tag(),false()) -> F()
    eqt(tag(),lock()) -> F()
    eqt(tag(),locker()) -> F()
    eqt(tag(),mcrlrecord()) -> F()
    eqt(tag(),ok()) -> F()
    eqt(tag(),pending()) -> F()
    eqt(tag(),release()) -> F()
    eqt(tag(),request()) -> F()
    eqt(tag(),resource()) -> F()
    eqt(tag(),tag()) -> T()
    eqt(tag(),true()) -> F()
    eqt(tag(),undefined()) -> F()
    eqt(tag(),pid(N2)) -> F()
    eqt(tag(),int(N2)) -> F()
    eqt(tag(),cons(H2,T2)) -> F()
    eqt(tag(),tuple(H2,T2)) -> F()
    eqt(tag(),tuplenil(H2)) -> F()
    eqt(true(),nil()) -> F()
    eqt(true(),a()) -> F()
    eqt(true(),excl()) -> F()
    eqt(true(),false()) -> F()
    eqt(true(),lock()) -> F()
    eqt(true(),locker()) -> F()
    eqt(true(),mcrlrecord()) -> F()
    eqt(true(),ok()) -> F()
    eqt(true(),pending()) -> F()
    eqt(true(),release()) -> F()
    eqt(true(),request()) -> F()
    eqt(true(),resource()) -> F()
    eqt(true(),tag()) -> F()
    eqt(true(),true()) -> T()
    eqt(true(),undefined()) -> F()
    eqt(true(),pid(N2)) -> F()
    eqt(true(),int(N2)) -> F()
    eqt(true(),cons(H2,T2)) -> F()
    eqt(true(),tuple(H2,T2)) -> F()
    eqt(true(),tuplenil(H2)) -> F()
    eqt(undefined(),nil()) -> F()
    eqt(undefined(),a()) -> F()
    eqt(undefined(),tuplenil(H2)) ->
      F()
    eqt(pid(N1),nil()) -> F()
    eqt(pid(N1),a()) -> F()
    eqt(pid(N1),excl()) -> F()
    eqt(pid(N1),false()) -> F()
    eqt(pid(N1),lock()) -> F()
    eqt(pid(N1),locker()) -> F()
    eqt(pid(N1),mcrlrecord()) -> F()
    eqt(pid(N1),ok()) -> F()
    eqt(pid(N1),pending()) -> F()
    eqt(pid(N1),release()) -> F()
    eqt(pid(N1),request()) -> F()
    eqt(pid(N1),resource()) -> F()
    eqt(pid(N1),tag()) -> F()
    eqt(pid(N1),true()) -> F()
    eqt(pid(N1),undefined()) -> F()
    eqt(pid(N1),pid(N2)) -> eqt(N1
                               ,N2)
    eqt(pid(N1),int(N2)) -> F()
    eqt(pid(N1),cons(H2,T2)) -> F()
    eqt(pid(N1),tuple(H2,T2)) -> F()
    eqt(pid(N1),tuplenil(H2)) -> F()
    eqt(int(N1),nil()) -> F()
    eqt(int(N1),a()) -> F()
    eqt(int(N1),excl()) -> F()
    eqt(int(N1),false()) -> F()
    eqt(int(N1),lock()) -> F()
    eqt(int(N1),locker()) -> F()
    eqt(int(N1),mcrlrecord()) -> F()
    eqt(int(N1),ok()) -> F()
    eqt(int(N1),pending()) -> F()
    eqt(int(N1),release()) -> F()
    eqt(int(N1),request()) -> F()
    eqt(int(N1),resource()) -> F()
    eqt(int(N1),tag()) -> F()
    eqt(int(N1),true()) -> F()
    eqt(int(N1),undefined()) -> F()
    eqt(cons(H1,T1),resource()) ->
      F()
    eqt(cons(H1,T1),tag()) -> F()
    eqt(cons(H1,T1),true()) -> F()
    eqt(cons(H1,T1),undefined()) ->
      F()
    eqt(cons(H1,T1),pid(N2)) -> F()
    eqt(cons(H1,T1),int(N2)) -> F()
    eqt(cons(H1,T1),cons(H2,T2)) ->
      and(eqt(H1,H2),eqt(T1,T2))
    eqt(cons(H1,T1),tuple(H2,T2)) ->
      F()
    eqt(cons(H1,T1),tuplenil(H2)) ->
      F()
    eqt(tuple(H1,T1),nil()) -> F()
    eqt(tuple(H1,T1),a()) -> F()
    eqt(tuple(H1,T1),excl()) -> F()
    eqt(tuple(H1,T1),false()) -> F()
    eqt(tuple(H1,T1),lock()) -> F()
    eqt(tuple(H1,T1),locker()) ->
      F()
    eqt(tuple(H1,T1)
       ,mcrlrecord()) -> F()
    eqt(tuple(H1,T1),ok()) -> F()
    eqt(tuple(H1,T1),pending()) ->
      F()
    eqt(tuple(H1,T1),release()) ->
      F()
    eqt(tuple(H1,T1),request()) ->
      F()
    eqt(tuple(H1,T1),resource()) ->
      F()
    eqt(tuple(H1,T1),tag()) -> F()
    eqt(tuple(H1,T1),true()) -> F()
    eqt(tuple(H1,T1),undefined()) ->
      F()
    eqt(tuple(H1,T1),pid(N2)) -> F()
    eqt(tuple(H1,T1),int(N2)) -> F()
    eqt(tuple(H1,T1),cons(H2,T2)) ->
      F()
    eqt(tuple(H1,T1)
       ,tuple(H2,T2)) -> and(eqt(H1,H2)
                            ,eqt(T1,T2))
    eqt(tuple(H1,T1)
       ,tuplenil(H2)) -> F()
    eqt(tuplenil(H1),nil()) -> F()
    eqt(tuplenil(H1),a()) -> F()
    eqt(tuplenil(H1),excl()) -> F()
    eqt(tuplenil(H1),false()) -> F()
    eqt(tuplenil(H1),lock()) -> F()
    eqt(tuplenil(H1),locker()) ->
      F()
    eqt(tuplenil(H1)
       ,mcrlrecord()) -> F()
    eqt(tuplenil(H1),ok()) -> F()
    eqt(tuplenil(H1),pending()) ->
      F()
    eqt(tuplenil(H1),release()) ->
      F()
    eqt(tuplenil(H1),request()) ->
      F()
    eqt(tuplenil(H1),resource()) ->
      F()
    eqt(tuplenil(H1),tag()) -> F()
    eqt(tuplenil(H1),true()) -> F()
    eqt(tuplenil(H1),undefined()) ->
      F()
    eqt(tuplenil(H1),pid(N2)) -> F()
    eqt(tuplenil(H1),int(N2)) -> F()
    eqt(tuplenil(H1),cons(H2,T2)) ->
      F()
    eqt(tuplenil(H1)
       ,tuple(H2,T2)) -> F()
    eqt(tuplenil(H1)
       ,tuplenil(H2)) -> eqt(H1,H2)
    element(int(s(0()))
           ,tuplenil(T1)) -> T1
    element(int(s(0()))
           ,tuple(T1,T2)) -> T1
    element(int(s(s(N1)))
           ,tuple(T1,T2)) ->
      element(int(s(N1)),T2)
    record_new(lock()) ->
      tuple(mcrlrecord()
           ,tuple(lock()
                 ,tuple(undefined()
                       ,tuple(nil(),tuplenil(nil())))))
    record_extract(tuple(mcrlrecord()
                        ,tuple(lock()
                              ,tuple(F0
                                    ,tuple(F1,tuplenil(F2)))))
                  ,lock()
                  ,resource()) ->
      tuple(mcrlrecord()
           ,tuple(lock()
                 ,tuple(F0
                       ,tuple(F1,tuplenil(F2)))))
    record_update(tuple(mcrlrecord()
                       ,tuple(lock()
                             ,tuple(F0
                                   ,tuple(F1,tuplenil(F2)))))
                 ,lock()
                 ,pending()
                 ,NewF) -> tuple(mcrlrecord()
                                ,tuple(lock()
                                      ,tuple(F0
                                            ,tuple(F1,tuplenil(NewF)))))
    record_updates(Record
                  ,Name
                  ,nil()) -> Record
    record_updates(Record
                  ,Name
                  ,cons(tuple(Field
                             ,tuplenil(NewF))
                       ,Fields)) ->
      record_updates(record_update(Record
                                  ,Name
                                  ,Field
                                  ,NewF)
                    ,Name
                    ,Fields)
    locker2_map_promote_pending(nil()
                               ,Pending) -> nil()
    locker2_map_promote_pending(cons(Lock
                                    ,Locks)
                               ,Pending) ->
      cons(locker2_promote_pending(Lock
                                  ,Pending)
          ,locker2_map_promote_pending(Locks
                                      ,Pending))
    locker2_map_claim_lock(nil()
                          ,Resources
                          ,Client) -> nil()
    locker2_map_claim_lock(cons(Lock
                               ,Locks)
                          ,Resources
                          ,Client) ->
      cons(locker2_claim_lock(Lock
                             ,Resources
                             ,Client)
          ,locker2_map_claim_lock(Locks
                                 ,Resources
                                 ,Client))
    locker2_map_add_pending(nil()
                           ,Resources
                           ,Client) -> nil()
    locker2_promote_pending(Lock
                           ,Client) -> case0(Client
                                            ,Lock
                                            ,record_extract(Lock
                                                           ,lock()
                                                           ,pending()))
    case0(Client
         ,Lock
         ,cons(Client,Pendings)) ->
      record_updates(Lock
                    ,lock()
                    ,cons(tuple(excl()
                               ,tuplenil(Client))
                         ,cons(tuple(pending()
                                    ,tuplenil(Pendings))
                              ,nil())))
    case0(Client,Lock,MCRLFree0) ->
      Lock
    locker2_remove_pending(Lock
                          ,Client) -> record_updates(Lock
                                                    ,lock()
                                                    ,cons(tuple(pending()
                                                               ,tuplenil(subtract(record_extract(Lock
                                                                                                ,lock()
                                                                                                ,pending())
                                                                                 ,cons(Client
                                                                                      ,nil()))))
                                                         ,nil()))
    locker2_add_pending(Lock
                       ,Resources
                       ,Client) -> case1(Client
                                        ,Resources
                                        ,Lock
                                        ,member(record_extract(Lock
                                                              ,lock()
                                                              ,resource())
                                               ,Resources))
    case1(Client
         ,Resources
         ,Lock
         ,true()) -> record_updates(Lock
                                   ,lock()
                                   ,cons(tuple(pending()
                                              ,tuplenil(append(record_extract(Lock
                                                                             ,lock()
                                                                             ,pending())
                                                              ,cons(Client
                                                                   ,nil()))))
                                        ,nil()))
    case1(Client
         ,Resources
         ,Lock
         ,false()) -> Lock
    locker2_release_lock(Lock
                        ,Client) -> case2(Client
                                         ,Lock
                                         ,gen_modtageq(Client
                                                      ,record_extract(Lock
                                                                     ,lock()
                                                                     ,excl())))
    case2(Client,Lock,true()) ->
      record_updates(Lock
                    ,lock()
                    ,cons(tuple(excllock(),excl())
                         ,nil()))
    case4(Client,Lock,MCRLFree1) ->
      false()
    locker2_obtainables(nil()
                       ,Client) -> true()
    locker2_obtainables(cons(Lock
                            ,Locks)
                       ,Client) -> case5(Client
                                        ,Locks
                                        ,Lock
                                        ,member(Client
                                               ,record_extract(Lock
                                                              ,lock()
                                                              ,pending())))
    case5(Client
         ,Locks
         ,Lock
         ,true()) ->
      andt(locker2_obtainable(Lock
                             ,Client)
          ,locker2_obtainables(Locks
                              ,Client))
    case5(Client
         ,Locks
         ,Lock
         ,false()) ->
      locker2_obtainables(Locks
                         ,Client)
    locker2_check_available(Resource
                           ,nil()) -> false()
    locker2_check_available(Resource
                           ,cons(Lock,Locks)) ->
      case6(Locks
           ,Lock
           ,Resource
           ,equal(Resource
                 ,record_extract(Lock
                                ,lock()
                                ,resource())))
    case6(Locks
         ,Lock
         ,Resource
         ,true()) ->
      andt(equal(record_extract(Lock
                               ,lock()
                               ,excl())
                ,nil())
          ,equal(record_extract(Lock
                               ,lock()
                               ,pending())
                ,nil()))
    case6(Locks
         ,Lock
         ,Resource
         ,false()) ->
      locker2_check_available(Resource
                             ,Locks)
    locker2_check_availables(nil()
                            ,Locks) -> true()
    locker2_check_availables(cons(Resource
                                 ,Resources)
                            ,Locks) ->
      andt(locker2_check_available(Resource
                                  ,Locks)
          ,locker2_check_availables(Resources
                                   ,Locks))
    locker2_adduniq(nil(),List) ->
      List
    append(cons(Head,Tail),List) ->
      cons(Head,append(Tail,List))
    subtract(List,nil()) -> List
    subtract(List
            ,cons(Head,Tail)) ->
      subtract(delete(Head,List),Tail)
    delete(E,nil()) -> nil()
    delete(E,cons(Head,Tail)) ->
      case8(Tail,Head,E,equal(E,Head))
    case8(Tail,Head,E,true()) ->
      Tail
    case8(Tail,Head,E,false()) ->
      cons(Head,delete(E,Tail))
    gen_tag(Pid) -> tuple(Pid
                         ,tuplenil(tag()))
    gen_modtageq(Client1,Client2) ->
      equal(Client1,Client2)
    member(E,nil()) -> false()
    member(E,cons(Head,Tail)) ->
      case9(Tail,Head,E,equal(E,Head))
    case9(Tail,Head,E,true()) ->
      true()
    case9(Tail,Head,E,false()) ->
      member(E,Tail)
    eqs(empty(),empty()) -> T()
    eqs(empty(),stack(E2,S2)) -> F()
    eqs(stack(E1,S1),empty()) -> F()
    eqs(stack(E1,S1)
       ,stack(E2,S2)) -> and(eqt(E1,E2)
                            ,eqs(S1,S2))
    pushs(E1,S1) -> stack(E1,S1)
    pops(stack(E1,S1)) -> S1
    tops(stack(E1,S1)) -> E1
    istops(E1,empty()) -> F()
    istops(E1,stack(E2,S1)) ->
      eqt(E1,E2)
    eqc(nocalls(),nocalls()) -> T()
    eqc(nocalls()
       ,calls(E2,S2,CS2)) -> F()
    eqc(calls(E1,S1,CS1)
       ,nocalls()) -> F()
    eqc(calls(E1,S1,CS1)
       ,calls(E2,S2,CS2)) -> and(eqt(E1
                                    ,E2)
                                ,and(eqs(S1,S2),eqc(CS1,CS2)))
    push(E1,E2,nocalls()) ->
      calls(E1
           ,stack(E2,empty())
           ,nocalls())
    push(E1,E2,calls(E3,S1,CS1)) ->
      push1(E1
           ,E2
           ,E3
           ,S1
           ,CS1
           ,eqt(E1,E3))
    push1(E1,E2,E3,S1,CS1,T()) ->
      calls(E3,pushs(E2,S1),CS1))