Termination proof

1: switching to dependency pairs

eqt#( pid( N1 ) , pid( N2 ) )	→	eqt#( N1 , N2 )
eqt#( cons( H1 , T1 ) , cons( H2 , T2 ) )	→	and#( eqt( H1 , H2 ) , eqt( T1 , T2 ) )
eqt#( cons( H1 , T1 ) , cons( H2 , T2 ) )	→	eqt#( H1 , H2 )
eqt#( cons( H1 , T1 ) , cons( H2 , T2 ) )	→	eqt#( T1 , T2 )
eqt#( tuple( H1 , T1 ) , tuple( H2 , T2 ) )	→	and#( eqt( H1 , H2 ) , eqt( T1 , T2 ) )
eqt#( tuple( H1 , T1 ) , tuple( H2 , T2 ) )	→	eqt#( H1 , H2 )
eqt#( tuple( H1 , T1 ) , tuple( H2 , T2 ) )	→	eqt#( T1 , T2 )
eqt#( tuplenil( H1 ) , tuplenil( H2 ) )	→	eqt#( H1 , H2 )
element#( int( s( s( N1 ) ) ) , tuple( T1 , T2 ) )	→	element#( int( s( N1 ) ) , T2 )
record_updates#( Record , Name , cons( tuple( Field , tuplenil( NewF ) ) , Fields ) )	→	record_updates#( record_update( Record , Name , Field , NewF ) , Name , Fields )
record_updates#( Record , Name , cons( tuple( Field , tuplenil( NewF ) ) , Fields ) )	→	record_update#( Record , Name , Field , NewF )
locker2_map_promote_pending#( cons( Lock , Locks ) , Pending )	→	locker2_promote_pending#( Lock , Pending )
locker2_map_promote_pending#( cons( Lock , Locks ) , Pending )	→	locker2_map_promote_pending#( Locks , Pending )
locker2_map_claim_lock#( cons( Lock , Locks ) , Resources , Client )	→	locker2_map_claim_lock#( Locks , Resources , Client )
locker2_promote_pending#( Lock , Client )	→	case0#( Client , Lock , record_extract( Lock , lock , pending ) )
locker2_promote_pending#( Lock , Client )	→	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 ) ) )
locker2_remove_pending#( Lock , Client )	→	record_updates#( Lock , lock , cons( tuple( pending , tuplenil( subtract( record_extract( Lock , lock , pending ) , cons( Client , nil ) ) ) ) , nil ) )
locker2_remove_pending#( Lock , Client )	→	subtract#( record_extract( Lock , lock , pending ) , cons( Client , nil ) )
locker2_remove_pending#( Lock , Client )	→	record_extract#( Lock , lock , pending )
locker2_add_pending#( Lock , Resources , Client )	→	case1#( Client , Resources , Lock , member( record_extract( Lock , lock , resource ) , Resources ) )
locker2_add_pending#( Lock , Resources , Client )	→	member#( record_extract( Lock , lock , resource ) , Resources )
locker2_add_pending#( Lock , Resources , Client )	→	record_extract#( Lock , lock , resource )
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 , true )	→	append#( record_extract( Lock , lock , pending ) , cons( Client , nil ) )
case1#( Client , Resources , Lock , true )	→	record_extract#( Lock , lock , pending )
locker2_release_lock#( Lock , Client )	→	case2#( Client , Lock , gen_modtageq( Client , record_extract( Lock , lock , excl ) ) )
locker2_release_lock#( Lock , Client )	→	gen_modtageq#( Client , record_extract( Lock , lock , excl ) )
locker2_release_lock#( Lock , Client )	→	record_extract#( Lock , lock , excl )
case2#( Client , Lock , true )	→	record_updates#( Lock , lock , cons( tuple( excllock , excl ) , nil ) )
locker2_obtainables#( cons( Lock , Locks ) , Client )	→	case5#( Client , Locks , Lock , member( Client , record_extract( Lock , lock , pending ) ) )
locker2_obtainables#( cons( Lock , Locks ) , Client )	→	member#( Client , record_extract( Lock , lock , pending ) )
locker2_obtainables#( cons( Lock , Locks ) , Client )	→	record_extract#( Lock , lock , pending )
case5#( Client , Locks , Lock , true )	→	locker2_obtainables#( Locks , Client )
case5#( Client , Locks , Lock , false )	→	locker2_obtainables#( Locks , Client )
locker2_check_available#( Resource , cons( Lock , Locks ) )	→	case6#( Locks , Lock , Resource , equal( Resource , record_extract( Lock , lock , resource ) ) )
locker2_check_available#( Resource , cons( Lock , Locks ) )	→	record_extract#( Lock , lock , resource )
case6#( Locks , Lock , Resource , true )	→	record_extract#( Lock , lock , excl )
case6#( Locks , Lock , Resource , true )	→	record_extract#( Lock , lock , pending )
case6#( Locks , Lock , Resource , false )	→	locker2_check_available#( Resource , Locks )
locker2_check_availables#( cons( Resource , Resources ) , Locks )	→	locker2_check_available#( Resource , Locks )
locker2_check_availables#( cons( Resource , Resources ) , Locks )	→	locker2_check_availables#( Resources , Locks )
append#( cons( Head , Tail ) , List )	→	append#( Tail , List )
subtract#( List , cons( Head , Tail ) )	→	subtract#( delete( Head , List ) , Tail )
subtract#( List , cons( Head , Tail ) )	→	delete#( Head , List )
delete#( E , cons( Head , Tail ) )	→	case8#( Tail , Head , E , equal( E , Head ) )
case8#( Tail , Head , E , false )	→	delete#( E , Tail )
member#( E , cons( Head , Tail ) )	→	case9#( Tail , Head , E , equal( E , Head ) )
case9#( Tail , Head , E , false )	→	member#( E , Tail )
eqs#( stack( E1 , S1 ) , stack( E2 , S2 ) )	→	and#( eqt( E1 , E2 ) , eqs( S1 , S2 ) )
eqs#( stack( E1 , S1 ) , stack( E2 , S2 ) )	→	eqt#( E1 , E2 )
eqs#( stack( E1 , S1 ) , stack( E2 , S2 ) )	→	eqs#( S1 , S2 )
istops#( E1 , stack( E2 , S1 ) )	→	eqt#( E1 , E2 )
eqc#( calls( E1 , S1 , CS1 ) , calls( E2 , S2 , CS2 ) )	→	and#( eqt( E1 , E2 ) , and( eqs( S1 , S2 ) , eqc( CS1 , CS2 ) ) )
eqc#( calls( E1 , S1 , CS1 ) , calls( E2 , S2 , CS2 ) )	→	eqt#( E1 , E2 )
eqc#( calls( E1 , S1 , CS1 ) , calls( E2 , S2 , CS2 ) )	→	and#( eqs( S1 , S2 ) , eqc( CS1 , CS2 ) )
eqc#( calls( E1 , S1 , CS1 ) , calls( E2 , S2 , CS2 ) )	→	eqs#( S1 , S2 )
eqc#( calls( E1 , S1 , CS1 ) , calls( E2 , S2 , CS2 ) )	→	eqc#( CS1 , CS2 )
push#( E1 , E2 , calls( E3 , S1 , CS1 ) )	→	push1#( E1 , E2 , E3 , S1 , CS1 , eqt( E1 , E3 ) )
push#( E1 , E2 , calls( E3 , S1 , CS1 ) )	→	eqt#( E1 , E3 )
push1#( E1 , E2 , E3 , S1 , CS1 , T )	→	pushs#( E2 , S1 )

1.1: dependency graph processor

The dependency pairs are split into 11 component(s).

• The 1st component contains the pair(s)

  eqc#( calls( E1 , S1 , CS1 ) , calls( E2 , S2 , CS2 ) )

  →

  eqc#( CS1 , CS2 )

  1.1.1: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [locker2_add_pending (x1, x2, x3) ]	=	3 x1 + 2 x2 + 3 x3 + 1
  [locker]	=	0
  [a]	=	0
  [stack (x1, x2) ]	=	x1 + x2
  [locker2_remove_pending (x1, x2) ]	=	3 x1 + x2 + 1
  [lock]	=	0
  [or (x1, x2) ]	=	0
  [case6 (x1, ..., x4) ]	=	3 x1 + 3 x2
  [0]	=	0
  [locker2_check_availables (x1, x2) ]	=	3
  [F]	=	0
  [cons (x1, x2) ]	=	2 x1 + 2 x2
  [locker2_release_lock (x1, x2) ]	=	2 x1 + 2 x2 + 1
  [element (x1, x2) ]	=	x1
  [true]	=	0
  [case9 (x1, ..., x4) ]	=	2 x1 + 2 x2
  [resource]	=	0
  [and (x1, x2) ]	=	2 x1 + 2 x2
  [locker2_adduniq (x1, x2) ]	=	x1
  [tops (x1) ]	=	x1
  [record_new (x1) ]	=	1
  [istops (x1, x2) ]	=	3 x1 + 2 x2 + 2
  [locker2_check_available (x1, x2) ]	=	2 x1
  [eqs (x1, x2) ]	=	0
  [request]	=	0
  [gen_tag (x1) ]	=	3 x1 + 2
  [mcrlrecord]	=	0
  [locker2_map_add_pending (x1, x2, x3) ]	=	3
  [push (x1, x2, x3) ]	=	2 x1 + 2 x2 + 2 x3 + 2
  [empty]	=	0
  [record_update (x1, ..., x4) ]	=	x1 + 3 x2 + x3
  [case1 (x1, ..., x4) ]	=	3 x1 + x2 + 3 x3 + 1
  [locker2_map_claim_lock (x1, x2, x3) ]	=	0
  [eqc (x1, x2) ]	=	0
  [tuple (x1, x2) ]	=	2 x1 + x2
  [append (x1, x2) ]	=	x1
  [false]	=	0
  [locker2_promote_pending (x1, x2) ]	=	3 x1
  [pushs (x1, x2) ]	=	x1 + 2 x2
  [eqt (x1, x2) ]	=	0
  [subtract (x1, x2) ]	=	x1
  [locker2_map_promote_pending (x1, x2) ]	=	3 x1
  [record_updates (x1, x2, x3) ]	=	x1 + x2
  [nocalls]	=	0
  [record_extract (x1, x2, x3) ]	=	x1
  [andt (x1, x2) ]	=	0
  [case8 (x1, ..., x4) ]	=	2 x1 + 2 x2
  [s (x1) ]	=	0
  [undefined]	=	0
  [pending]	=	0
  [push1 (x1, ..., x6) ]	=	2 x1 + 2 x2 + 2 x3 + 2
  [not (x1) ]	=	2
  [calls (x1, x2, x3) ]	=	2 x1 + 1
  [if (x1, x2, x3) ]	=	x1 + x2
  [excl]	=	0
  [case5 (x1, ..., x4) ]	=	0
  [tuplenil (x1) ]	=	x1
  [imp (x1, x2) ]	=	x1
  [locker2_obtainables (x1, x2) ]	=	0
  [eq (x1, x2) ]	=	0
  [ok]	=	0
  [tag]	=	0
  [case0 (x1, x2, x3) ]	=	x1 + 2 x2
  [T]	=	0
  [eqc# (x1, x2) ]	=	x1 + x2
  [nil]	=	0
  [int (x1) ]	=	0
  [pid (x1) ]	=	0
  [equal (x1, x2) ]	=	0
  [pops (x1) ]	=	x1
  [case2 (x1, x2, x3) ]	=	x1 + x2
  [excllock]	=	0
  [locker2_obtainable (x1, x2) ]	=	0
  [delete (x1, x2) ]	=	x1
  [member (x1, x2) ]	=	x1
  [gen_modtageq (x1, x2) ]	=	x1
  [locker2_claim_lock (x1, x2, x3) ]	=	0
  [release]	=	0
  [case4 (x1, x2, x3) ]	=	3
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  none

  1.1.1.1: P is empty

  All dependency pairs have been removed.

• The 2nd component contains the pair(s)

  eqs#( stack( E1 , S1 ) , stack( E2 , S2 ) )

  →

  eqs#( S1 , S2 )

  1.1.2: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [locker2_add_pending (x1, x2, x3) ]	=	3 x1 + 2 x2 + 3 x3 + 3
  [locker]	=	0
  [a]	=	0
  [stack (x1, x2) ]	=	2 x1 + 2 x2 + 2
  [locker2_remove_pending (x1, x2) ]	=	3 x1 + x2 + 3
  [lock]	=	0
  [or (x1, x2) ]	=	0
  [case6 (x1, ..., x4) ]	=	3 x1 + x2
  [0]	=	0
  [locker2_check_availables (x1, x2) ]	=	3 x1 + 2
  [F]	=	0
  [cons (x1, x2) ]	=	x1 + x2 + 1
  [locker2_release_lock (x1, x2) ]	=	2 x1 + 2 x2 + 2
  [element (x1, x2) ]	=	2 x1
  [true]	=	0
  [case9 (x1, ..., x4) ]	=	0
  [resource]	=	0
  [and (x1, x2) ]	=	x1 + 2 x2
  [locker2_adduniq (x1, x2) ]	=	x1
  [tops (x1) ]	=	x1
  [record_new (x1) ]	=	0
  [istops (x1, x2) ]	=	3 x1
  [locker2_check_available (x1, x2) ]	=	3 x1
  [eqs (x1, x2) ]	=	0
  [request]	=	0
  [gen_tag (x1) ]	=	2 x1
  [mcrlrecord]	=	0
  [locker2_map_add_pending (x1, x2, x3) ]	=	3
  [push (x1, x2, x3) ]	=	3 x1 + 2 x2
  [empty]	=	0
  [record_update (x1, ..., x4) ]	=	x1 + 3 x2 + 2 x3
  [case1 (x1, ..., x4) ]	=	3 x1 + x2 + 3 x3 + 3
  [locker2_map_claim_lock (x1, x2, x3) ]	=	2 x1
  [eqc (x1, x2) ]	=	0
  [tuple (x1, x2) ]	=	2 x1 + x2
  [append (x1, x2) ]	=	x1
  [eqs# (x1, x2) ]	=	x1
  [false]	=	0
  [locker2_promote_pending (x1, x2) ]	=	3 x1 + 2
  [pushs (x1, x2) ]	=	3 x1 + 2 x2 + 3
  [eqt (x1, x2) ]	=	0
  [subtract (x1, x2) ]	=	x1
  [locker2_map_promote_pending (x1, x2) ]	=	3 x1 + 2
  [record_updates (x1, x2, x3) ]	=	x1 + 2 x2
  [nocalls]	=	0
  [record_extract (x1, x2, x3) ]	=	x1
  [andt (x1, x2) ]	=	0
  [case8 (x1, ..., x4) ]	=	x1 + x2 + 1
  [s (x1) ]	=	0
  [undefined]	=	0
  [pending]	=	0
  [push1 (x1, ..., x6) ]	=	3 x1 + 2 x2
  [not (x1) ]	=	0
  [calls (x1, x2, x3) ]	=	0
  [if (x1, x2, x3) ]	=	x1 + x2
  [excl]	=	0
  [case5 (x1, ..., x4) ]	=	2 x1
  [tuplenil (x1) ]	=	x1
  [imp (x1, x2) ]	=	x1
  [locker2_obtainables (x1, x2) ]	=	2 x1
  [eq (x1, x2) ]	=	0
  [ok]	=	0
  [tag]	=	0
  [case0 (x1, x2, x3) ]	=	x1 + 2 x2 + 2
  [T]	=	0
  [nil]	=	0
  [int (x1) ]	=	0
  [pid (x1) ]	=	0
  [equal (x1, x2) ]	=	2 x1
  [pops (x1) ]	=	x1
  [case2 (x1, x2, x3) ]	=	x1 + 2 x2 + 2
  [excllock]	=	0
  [locker2_obtainable (x1, x2) ]	=	0
  [delete (x1, x2) ]	=	x1
  [member (x1, x2) ]	=	0
  [gen_modtageq (x1, x2) ]	=	2 x1 + 3 x2
  [locker2_claim_lock (x1, x2, x3) ]	=	1
  [release]	=	0
  [case4 (x1, x2, x3) ]	=	3
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  none

  1.1.2.1: P is empty

  All dependency pairs have been removed.

• The 3rd component contains the pair(s)

  eqt#( cons( H1 , T1 ) , cons( H2 , T2 ) )	→	eqt#( H1 , H2 )
  eqt#( pid( N1 ) , pid( N2 ) )	→	eqt#( N1 , N2 )
  eqt#( cons( H1 , T1 ) , cons( H2 , T2 ) )	→	eqt#( T1 , T2 )
  eqt#( tuple( H1 , T1 ) , tuple( H2 , T2 ) )	→	eqt#( H1 , H2 )
  eqt#( tuple( H1 , T1 ) , tuple( H2 , T2 ) )	→	eqt#( T1 , T2 )
  eqt#( tuplenil( H1 ) , tuplenil( H2 ) )	→	eqt#( H1 , H2 )

  1.1.3: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [locker2_add_pending (x1, x2, x3) ]	=	3 x1 + 2 x2 + 3 x3
  [locker]	=	0
  [a]	=	0
  [stack (x1, x2) ]	=	2 x1 + 2 x2
  [locker2_remove_pending (x1, x2) ]	=	3 x1 + x2
  [lock]	=	0
  [or (x1, x2) ]	=	1
  [case6 (x1, ..., x4) ]	=	3 x1 + 2
  [0]	=	0
  [locker2_check_availables (x1, x2) ]	=	3 x1 + 1
  [F]	=	0
  [cons (x1, x2) ]	=	x1 + 2 x2
  [locker2_release_lock (x1, x2) ]	=	2 x1 + 2 x2
  [element (x1, x2) ]	=	x1
  [true]	=	0
  [case9 (x1, ..., x4) ]	=	0
  [resource]	=	0
  [and (x1, x2) ]	=	x1 + 2 x2
  [locker2_adduniq (x1, x2) ]	=	x1
  [tops (x1) ]	=	x1
  [record_new (x1) ]	=	1
  [istops (x1, x2) ]	=	2 x1 + x2 + 1
  [locker2_check_available (x1, x2) ]	=	2 x1 + 2
  [eqs (x1, x2) ]	=	0
  [request]	=	0
  [gen_tag (x1) ]	=	3 x1
  [mcrlrecord]	=	0
  [locker2_map_add_pending (x1, x2, x3) ]	=	3
  [push (x1, x2, x3) ]	=	2 x1 + x2 + 3 x3 + 3
  [empty]	=	0
  [record_update (x1, ..., x4) ]	=	x1 + x2 + 2 x3
  [case1 (x1, ..., x4) ]	=	3 x1 + x2 + 3 x3
  [locker2_map_claim_lock (x1, x2, x3) ]	=	2 x1
  [eqc (x1, x2) ]	=	0
  [tuple (x1, x2) ]	=	2 x1 + x2
  [append (x1, x2) ]	=	x1
  [false]	=	0
  [locker2_promote_pending (x1, x2) ]	=	3 x1
  [pushs (x1, x2) ]	=	2 x1 + 2 x2
  [eqt (x1, x2) ]	=	0
  [subtract (x1, x2) ]	=	x1
  [locker2_map_promote_pending (x1, x2) ]	=	3 x1
  [eqt# (x1, x2) ]	=	x1 + 2 x2
  [record_updates (x1, x2, x3) ]	=	x1 + x2
  [nocalls]	=	2
  [record_extract (x1, x2, x3) ]	=	x1
  [andt (x1, x2) ]	=	1
  [case8 (x1, ..., x4) ]	=	2 x1 + x2
  [s (x1) ]	=	0
  [undefined]	=	0
  [pending]	=	0
  [push1 (x1, ..., x6) ]	=	0
  [not (x1) ]	=	1
  [calls (x1, x2, x3) ]	=	0
  [if (x1, x2, x3) ]	=	x1 + x2
  [excl]	=	0
  [case5 (x1, ..., x4) ]	=	x1 + 2
  [tuplenil (x1) ]	=	2 x1
  [imp (x1, x2) ]	=	x1
  [locker2_obtainables (x1, x2) ]	=	x1 + 2
  [eq (x1, x2) ]	=	2
  [ok]	=	0
  [tag]	=	0
  [case0 (x1, x2, x3) ]	=	x1 + 2 x2
  [T]	=	0
  [nil]	=	0
  [int (x1) ]	=	0
  [pid (x1) ]	=	2 x1 + 3
  [equal (x1, x2) ]	=	0
  [pops (x1) ]	=	x1
  [case2 (x1, x2, x3) ]	=	x1 + x2
  [excllock]	=	0
  [locker2_obtainable (x1, x2) ]	=	0
  [delete (x1, x2) ]	=	x1
  [member (x1, x2) ]	=	0
  [gen_modtageq (x1, x2) ]	=	3 x1 + 2
  [locker2_claim_lock (x1, x2, x3) ]	=	x1
  [release]	=	0
  [case4 (x1, x2, x3) ]	=	1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  eqt#( cons( H1 , T1 ) , cons( H2 , T2 ) )	→	eqt#( H1 , H2 )
  eqt#( cons( H1 , T1 ) , cons( H2 , T2 ) )	→	eqt#( T1 , T2 )
  eqt#( tuple( H1 , T1 ) , tuple( H2 , T2 ) )	→	eqt#( H1 , H2 )
  eqt#( tuple( H1 , T1 ) , tuple( H2 , T2 ) )	→	eqt#( T1 , T2 )
  eqt#( tuplenil( H1 ) , tuplenil( H2 ) )	→	eqt#( H1 , H2 )

  1.1.3.1: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [locker2_add_pending (x1, x2, x3) ]	=	3 x1 + 2 x2 + 3 x3 + 3
  [locker]	=	0
  [a]	=	0
  [stack (x1, x2) ]	=	x1 + x2
  [locker2_remove_pending (x1, x2) ]	=	3 x1 + 3 x2 + 2
  [lock]	=	0
  [or (x1, x2) ]	=	0
  [case6 (x1, ..., x4) ]	=	2 x1
  [0]	=	0
  [locker2_check_availables (x1, x2) ]	=	2 x1 + 2
  [F]	=	0
  [cons (x1, x2) ]	=	x1 + x2 + 1
  [locker2_release_lock (x1, x2) ]	=	3 x1 + x2 + 3
  [element (x1, x2) ]	=	x1 + 2 x2
  [true]	=	0
  [case9 (x1, ..., x4) ]	=	x1 + 1
  [resource]	=	0
  [and (x1, x2) ]	=	2 x1 + 2 x2
  [locker2_adduniq (x1, x2) ]	=	x1
  [tops (x1) ]	=	x1
  [record_new (x1) ]	=	1
  [istops (x1, x2) ]	=	x1 + 2
  [locker2_check_available (x1, x2) ]	=	2
  [eqs (x1, x2) ]	=	0
  [request]	=	0
  [gen_tag (x1) ]	=	x1
  [mcrlrecord]	=	0
  [locker2_map_add_pending (x1, x2, x3) ]	=	0
  [push (x1, x2, x3) ]	=	3 x1 + 3 x2 + 1
  [empty]	=	0
  [record_update (x1, ..., x4) ]	=	x1 + 2 x2 + 1
  [case1 (x1, ..., x4) ]	=	3 x1 + x2 + 3 x3 + 2
  [locker2_map_claim_lock (x1, x2, x3) ]	=	x1
  [eqc (x1, x2) ]	=	0
  [tuple (x1, x2) ]	=	x1 + x2
  [append (x1, x2) ]	=	x1
  [false]	=	2
  [locker2_promote_pending (x1, x2) ]	=	3 x1 + 2
  [pushs (x1, x2) ]	=	2 x1 + x2 + 2
  [eqt (x1, x2) ]	=	0
  [subtract (x1, x2) ]	=	x1
  [locker2_map_promote_pending (x1, x2) ]	=	3 x1 + 3
  [eqt# (x1, x2) ]	=	3 x1 + 3 x2
  [record_updates (x1, x2, x3) ]	=	x1 + x2
  [nocalls]	=	0
  [record_extract (x1, x2, x3) ]	=	x1
  [andt (x1, x2) ]	=	x1
  [case8 (x1, ..., x4) ]	=	x1 + x2 + 1
  [s (x1) ]	=	2 x1
  [undefined]	=	0
  [pending]	=	0
  [push1 (x1, ..., x6) ]	=	3 x1 + 1
  [not (x1) ]	=	0
  [calls (x1, x2, x3) ]	=	0
  [if (x1, x2, x3) ]	=	x1 + x2
  [excl]	=	0
  [case5 (x1, ..., x4) ]	=	0
  [tuplenil (x1) ]	=	2 x1
  [imp (x1, x2) ]	=	x1 + 1
  [locker2_obtainables (x1, x2) ]	=	0
  [eq (x1, x2) ]	=	0
  [ok]	=	0
  [tag]	=	0
  [case0 (x1, x2, x3) ]	=	x1 + 2 x2
  [T]	=	0
  [nil]	=	0
  [int (x1) ]	=	x1
  [pid (x1) ]	=	0
  [equal (x1, x2) ]	=	0
  [pops (x1) ]	=	x1
  [case2 (x1, x2, x3) ]	=	x1 + 2 x2 + 2
  [excllock]	=	0
  [locker2_obtainable (x1, x2) ]	=	0
  [delete (x1, x2) ]	=	x1
  [member (x1, x2) ]	=	2
  [gen_modtageq (x1, x2) ]	=	3 x1
  [locker2_claim_lock (x1, x2, x3) ]	=	0
  [release]	=	0
  [case4 (x1, x2, x3) ]	=	3
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  eqt#( tuple( H1 , T1 ) , tuple( H2 , T2 ) )	→	eqt#( H1 , H2 )
  eqt#( tuple( H1 , T1 ) , tuple( H2 , T2 ) )	→	eqt#( T1 , T2 )
  eqt#( tuplenil( H1 ) , tuplenil( H2 ) )	→	eqt#( H1 , H2 )

  1.1.3.1.1: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [locker2_add_pending (x1, x2, x3) ]	=	3 x1 + 2 x2 + x3 + 3
  [locker]	=	0
  [a]	=	0
  [stack (x1, x2) ]	=	2 x1 + x2
  [locker2_remove_pending (x1, x2) ]	=	3 x1 + 3
  [lock]	=	0
  [or (x1, x2) ]	=	1
  [case6 (x1, ..., x4) ]	=	2 x1 + 1
  [0]	=	0
  [locker2_check_availables (x1, x2) ]	=	3 x1 + 2
  [F]	=	0
  [cons (x1, x2) ]	=	x1 + x2 + 2
  [locker2_release_lock (x1, x2) ]	=	3 x1 + 2 x2 + 2
  [element (x1, x2) ]	=	2 x1
  [true]	=	0
  [case9 (x1, ..., x4) ]	=	2 x1
  [resource]	=	0
  [and (x1, x2) ]	=	2 x1 + 2 x2
  [locker2_adduniq (x1, x2) ]	=	x1
  [tops (x1) ]	=	x1
  [record_new (x1) ]	=	1
  [istops (x1, x2) ]	=	0
  [locker2_check_available (x1, x2) ]	=	2
  [eqs (x1, x2) ]	=	0
  [request]	=	0
  [gen_tag (x1) ]	=	2 x1 + 2
  [mcrlrecord]	=	0
  [locker2_map_add_pending (x1, x2, x3) ]	=	3
  [push (x1, x2, x3) ]	=	2 x1 + 2 x2 + 1
  [empty]	=	0
  [record_update (x1, ..., x4) ]	=	x1 + x2 + 2 x3 + 3
  [case1 (x1, ..., x4) ]	=	x1 + 3 x2 + 3
  [locker2_map_claim_lock (x1, x2, x3) ]	=	2 x1
  [eqc (x1, x2) ]	=	0
  [tuple (x1, x2) ]	=	2 x1 + x2
  [append (x1, x2) ]	=	x1
  [false]	=	2
  [locker2_promote_pending (x1, x2) ]	=	3 x1 + 2
  [pushs (x1, x2) ]	=	2 x1 + x2 + 1
  [eqt (x1, x2) ]	=	0
  [subtract (x1, x2) ]	=	x1
  [locker2_map_promote_pending (x1, x2) ]	=	3 x1
  [eqt# (x1, x2) ]	=	x1 + x2
  [record_updates (x1, x2, x3) ]	=	x1 + x2
  [nocalls]	=	0
  [record_extract (x1, x2, x3) ]	=	x1
  [andt (x1, x2) ]	=	1
  [case8 (x1, ..., x4) ]	=	x1 + x2 + 3 x3 + 2
  [s (x1) ]	=	0
  [undefined]	=	0
  [pending]	=	0
  [push1 (x1, ..., x6) ]	=	0
  [not (x1) ]	=	2
  [calls (x1, x2, x3) ]	=	0
  [if (x1, x2, x3) ]	=	x1 + x2
  [excl]	=	0
  [case5 (x1, ..., x4) ]	=	x1 + 3
  [tuplenil (x1) ]	=	2 x1 + 1
  [imp (x1, x2) ]	=	x1
  [locker2_obtainables (x1, x2) ]	=	x1 + 3
  [eq (x1, x2) ]	=	0
  [ok]	=	0
  [tag]	=	0
  [case0 (x1, x2, x3) ]	=	x1 + 2 x2 + 2
  [T]	=	0
  [nil]	=	0
  [int (x1) ]	=	0
  [pid (x1) ]	=	0
  [equal (x1, x2) ]	=	0
  [pops (x1) ]	=	x1
  [case2 (x1, x2, x3) ]	=	x1 + 2 x2 + 2
  [excllock]	=	0
  [locker2_obtainable (x1, x2) ]	=	0
  [delete (x1, x2) ]	=	x1
  [member (x1, x2) ]	=	2
  [gen_modtageq (x1, x2) ]	=	3 x1 + 3 x2
  [locker2_claim_lock (x1, x2, x3) ]	=	x1 + 2
  [release]	=	0
  [case4 (x1, x2, x3) ]	=	3
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  eqt#( tuple( H1 , T1 ) , tuple( H2 , T2 ) )	→	eqt#( H1 , H2 )
  eqt#( tuple( H1 , T1 ) , tuple( H2 , T2 ) )	→	eqt#( T1 , T2 )

  1.1.3.1.1.1: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [locker2_add_pending (x1, x2, x3) ]	=	3 x1 + 2 x2 + 3 x3 + 3
  [locker]	=	0
  [a]	=	0
  [stack (x1, x2) ]	=	x1 + x2
  [locker2_remove_pending (x1, x2) ]	=	3 x1 + 3
  [lock]	=	2
  [or (x1, x2) ]	=	0
  [case6 (x1, ..., x4) ]	=	2
  [0]	=	0
  [locker2_check_availables (x1, x2) ]	=	2 x1
  [F]	=	0
  [cons (x1, x2) ]	=	x1 + x2 + 2
  [locker2_release_lock (x1, x2) ]	=	3 x1 + 2 x2 + 3
  [element (x1, x2) ]	=	2 x1
  [true]	=	0
  [case9 (x1, ..., x4) ]	=	2 x1 + 2 x2 + 2 x3
  [resource]	=	0
  [and (x1, x2) ]	=	2 x1 + 2 x2
  [locker2_adduniq (x1, x2) ]	=	x1
  [tops (x1) ]	=	x1
  [record_new (x1) ]	=	3 x1 + 3
  [istops (x1, x2) ]	=	0
  [locker2_check_available (x1, x2) ]	=	2
  [eqs (x1, x2) ]	=	0
  [request]	=	0
  [gen_tag (x1) ]	=	3 x1 + 1
  [mcrlrecord]	=	0
  [locker2_map_add_pending (x1, x2, x3) ]	=	3
  [push (x1, x2, x3) ]	=	x1 + 2 x2 + 2 x3
  [empty]	=	0
  [record_update (x1, ..., x4) ]	=	x1 + x2 + 2 x3 + 3
  [case1 (x1, ..., x4) ]	=	3 x1 + x2 + 3 x3 + 3
  [locker2_map_claim_lock (x1, x2, x3) ]	=	2 x1
  [eqc (x1, x2) ]	=	0
  [tuple (x1, x2) ]	=	2 x1 + x2 + 1
  [append (x1, x2) ]	=	x1
  [false]	=	0
  [locker2_promote_pending (x1, x2) ]	=	3 x1 + 2
  [pushs (x1, x2) ]	=	x1 + x2
  [eqt (x1, x2) ]	=	0
  [subtract (x1, x2) ]	=	x1
  [locker2_map_promote_pending (x1, x2) ]	=	3 x1
  [eqt# (x1, x2) ]	=	x1
  [record_updates (x1, x2, x3) ]	=	x1 + x2
  [nocalls]	=	0
  [record_extract (x1, x2, x3) ]	=	x1
  [andt (x1, x2) ]	=	1
  [case8 (x1, ..., x4) ]	=	x1 + x2 + 2
  [s (x1) ]	=	0
  [undefined]	=	0
  [pending]	=	0
  [push1 (x1, ..., x6) ]	=	x1 + 2 x2 + 2 x3 + 2 x4
  [not (x1) ]	=	3
  [calls (x1, x2, x3) ]	=	2 x1 + x2
  [if (x1, x2, x3) ]	=	x1 + x2
  [excl]	=	0
  [case5 (x1, ..., x4) ]	=	1
  [tuplenil (x1) ]	=	2 x1
  [imp (x1, x2) ]	=	x1
  [locker2_obtainables (x1, x2) ]	=	1
  [eq (x1, x2) ]	=	0
  [ok]	=	0
  [tag]	=	0
  [case0 (x1, x2, x3) ]	=	x1 + 2 x2 + 2
  [T]	=	0
  [nil]	=	0
  [int (x1) ]	=	0
  [pid (x1) ]	=	0
  [equal (x1, x2) ]	=	1
  [pops (x1) ]	=	x1
  [case2 (x1, x2, x3) ]	=	x1 + 2 x2 + 3
  [excllock]	=	0
  [locker2_obtainable (x1, x2) ]	=	0
  [delete (x1, x2) ]	=	x1
  [member (x1, x2) ]	=	2 x1
  [gen_modtageq (x1, x2) ]	=	3 x1 + 2 x2 + 2
  [locker2_claim_lock (x1, x2, x3) ]	=	x1
  [release]	=	0
  [case4 (x1, x2, x3) ]	=	2
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  none

  1.1.3.1.1.1.1: P is empty

  All dependency pairs have been removed.

• The 4th component contains the pair(s)

  element#( int( s( s( N1 ) ) ) , tuple( T1 , T2 ) )

  →

  element#( int( s( N1 ) ) , T2 )

  1.1.4: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [locker2_add_pending (x1, x2, x3) ]	=	3 x1 + x2 + x3
  [locker]	=	2
  [a]	=	2
  [stack (x1, x2) ]	=	2 x1 + x2
  [locker2_remove_pending (x1, x2) ]	=	3 x1 + x2
  [lock]	=	0
  [or (x1, x2) ]	=	0
  [case6 (x1, ..., x4) ]	=	0
  [0]	=	0
  [locker2_check_availables (x1, x2) ]	=	3 x1
  [F]	=	0
  [cons (x1, x2) ]	=	2 x1 + x2
  [locker2_release_lock (x1, x2) ]	=	2 x1 + 2 x2
  [element (x1, x2) ]	=	x1
  [true]	=	0
  [case9 (x1, ..., x4) ]	=	0
  [resource]	=	1
  [and (x1, x2) ]	=	x1 + x2
  [locker2_adduniq (x1, x2) ]	=	x1
  [tops (x1) ]	=	x1
  [record_new (x1) ]	=	0
  [istops (x1, x2) ]	=	2 x1
  [locker2_check_available (x1, x2) ]	=	0
  [eqs (x1, x2) ]	=	2 x1
  [request]	=	0
  [gen_tag (x1) ]	=	3 x1 + 3
  [mcrlrecord]	=	0
  [locker2_map_add_pending (x1, x2, x3) ]	=	0
  [push (x1, x2, x3) ]	=	2 x1 + 3 x2 + 2 x3
  [empty]	=	0
  [record_update (x1, ..., x4) ]	=	x1 + 3 x2 + 2 x3
  [case1 (x1, ..., x4) ]	=	x1 + 3 x2
  [locker2_map_claim_lock (x1, x2, x3) ]	=	0
  [eqc (x1, x2) ]	=	2 x1 + 1
  [tuple (x1, x2) ]	=	2 x1 + x2
  [append (x1, x2) ]	=	x1
  [false]	=	0
  [element# (x1, x2) ]	=	2 x1
  [locker2_promote_pending (x1, x2) ]	=	3 x1
  [pushs (x1, x2) ]	=	2 x1 + x2
  [eqt (x1, x2) ]	=	x1
  [subtract (x1, x2) ]	=	x1
  [locker2_map_promote_pending (x1, x2) ]	=	3 x1
  [record_updates (x1, x2, x3) ]	=	x1 + x2
  [nocalls]	=	0
  [record_extract (x1, x2, x3) ]	=	x1
  [andt (x1, x2) ]	=	0
  [case8 (x1, ..., x4) ]	=	x1 + 2 x2
  [s (x1) ]	=	2 x1 + 1
  [undefined]	=	0
  [pending]	=	0
  [push1 (x1, ..., x6) ]	=	x1 + 2 x2 + 3 x3 + 2 x4 + x5
  [not (x1) ]	=	1
  [calls (x1, x2, x3) ]	=	2 x1 + x2 + x3
  [if (x1, x2, x3) ]	=	x1 + x2
  [excl]	=	0
  [case5 (x1, ..., x4) ]	=	0
  [tuplenil (x1) ]	=	x1
  [imp (x1, x2) ]	=	x1 + 2
  [locker2_obtainables (x1, x2) ]	=	0
  [eq (x1, x2) ]	=	0
  [ok]	=	0
  [tag]	=	2
  [case0 (x1, x2, x3) ]	=	x1 + 2 x2
  [T]	=	0
  [nil]	=	0
  [int (x1) ]	=	2 x1 + 1
  [pid (x1) ]	=	x1 + 1
  [equal (x1, x2) ]	=	0
  [pops (x1) ]	=	x1
  [case2 (x1, x2, x3) ]	=	x1 + 2 x2
  [excllock]	=	0
  [locker2_obtainable (x1, x2) ]	=	0
  [delete (x1, x2) ]	=	x1
  [member (x1, x2) ]	=	0
  [gen_modtageq (x1, x2) ]	=	2
  [locker2_claim_lock (x1, x2, x3) ]	=	0
  [release]	=	0
  [case4 (x1, x2, x3) ]	=	3
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  none

  1.1.4.1: P is empty

  All dependency pairs have been removed.

• The 5th component contains the pair(s)

  locker2_map_promote_pending#( cons( Lock , Locks ) , Pending )

  →

  locker2_map_promote_pending#( Locks , Pending )

  1.1.5: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [locker2_add_pending (x1, x2, x3) ]	=	2 x1 + 2 x2 + 3 x3 + 1
  [locker]	=	0
  [a]	=	0
  [stack (x1, x2) ]	=	2 x1 + x2
  [locker2_remove_pending (x1, x2) ]	=	3 x1 + 1
  [lock]	=	1
  [or (x1, x2) ]	=	0
  [case6 (x1, ..., x4) ]	=	0
  [0]	=	0
  [locker2_check_availables (x1, x2) ]	=	2 x1 + 2
  [F]	=	0
  [cons (x1, x2) ]	=	x1 + x2 + 1
  [locker2_release_lock (x1, x2) ]	=	x1 + 3 x2 + 3
  [element (x1, x2) ]	=	x1
  [true]	=	0
  [case9 (x1, ..., x4) ]	=	3 x1 + 3 x2
  [resource]	=	1
  [and (x1, x2) ]	=	x1 + 2 x2
  [locker2_map_promote_pending# (x1, x2) ]	=	x1
  [locker2_adduniq (x1, x2) ]	=	x1
  [tops (x1) ]	=	x1
  [record_new (x1) ]	=	x1 + 3
  [istops (x1, x2) ]	=	x1
  [locker2_check_available (x1, x2) ]	=	0
  [eqs (x1, x2) ]	=	0
  [request]	=	0
  [gen_tag (x1) ]	=	2 x1
  [mcrlrecord]	=	0
  [locker2_map_add_pending (x1, x2, x3) ]	=	3
  [push (x1, x2, x3) ]	=	x1 + 2 x2
  [empty]	=	0
  [record_update (x1, ..., x4) ]	=	x1 + x2 + 1
  [case1 (x1, ..., x4) ]	=	3 x1 + x2 + 2 x3 + 1
  [locker2_map_claim_lock (x1, x2, x3) ]	=	2 x1 + 2
  [eqc (x1, x2) ]	=	0
  [tuple (x1, x2) ]	=	x1 + x2
  [append (x1, x2) ]	=	x1
  [false]	=	0
  [locker2_promote_pending (x1, x2) ]	=	3 x1 + 2
  [pushs (x1, x2) ]	=	2 x1 + x2 + 2
  [eqt (x1, x2) ]	=	0
  [subtract (x1, x2) ]	=	x1
  [locker2_map_promote_pending (x1, x2) ]	=	3 x1
  [record_updates (x1, x2, x3) ]	=	x1 + x2
  [nocalls]	=	0
  [record_extract (x1, x2, x3) ]	=	x1 + x2
  [andt (x1, x2) ]	=	0
  [case8 (x1, ..., x4) ]	=	x1 + x2 + 1
  [s (x1) ]	=	0
  [undefined]	=	0
  [pending]	=	0
  [push1 (x1, ..., x6) ]	=	x1
  [not (x1) ]	=	1
  [calls (x1, x2, x3) ]	=	0
  [if (x1, x2, x3) ]	=	x1 + x2
  [excl]	=	0
  [case5 (x1, ..., x4) ]	=	x1 + 1
  [tuplenil (x1) ]	=	x1
  [imp (x1, x2) ]	=	x1
  [locker2_obtainables (x1, x2) ]	=	x1
  [eq (x1, x2) ]	=	0
  [ok]	=	0
  [tag]	=	0
  [case0 (x1, x2, x3) ]	=	2 x1 + x2 + 2
  [T]	=	0
  [nil]	=	0
  [int (x1) ]	=	0
  [pid (x1) ]	=	0
  [equal (x1, x2) ]	=	0
  [pops (x1) ]	=	x1
  [case2 (x1, x2, x3) ]	=	x1 + 2
  [excllock]	=	0
  [locker2_obtainable (x1, x2) ]	=	0
  [delete (x1, x2) ]	=	x1
  [member (x1, x2) ]	=	3 x1
  [gen_modtageq (x1, x2) ]	=	3 x1 + 1
  [locker2_claim_lock (x1, x2, x3) ]	=	x1
  [release]	=	0
  [case4 (x1, x2, x3) ]	=	3
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  none

  1.1.5.1: P is empty

  All dependency pairs have been removed.

• The 6th component contains the pair(s)

  record_updates#( Record , Name , cons( tuple( Field , tuplenil( NewF ) ) , Fields ) )

  →

  record_updates#( record_update( Record , Name , Field , NewF ) , Name , Fields )

  1.1.6: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [locker2_add_pending (x1, x2, x3) ]	=	3 x1 + 2 x2 + 3 x3 + 2
  [locker]	=	0
  [a]	=	0
  [stack (x1, x2) ]	=	x1 + 2 x2 + 1
  [locker2_remove_pending (x1, x2) ]	=	3 x1 + 3 x2 + 3
  [lock]	=	0
  [or (x1, x2) ]	=	1
  [case6 (x1, ..., x4) ]	=	3 x1 + x2 + x3 + 3
  [0]	=	0
  [locker2_check_availables (x1, x2) ]	=	3 x1 + x2 + 2
  [F]	=	0
  [cons (x1, x2) ]	=	2 x1 + 2 x2 + 2
  [locker2_release_lock (x1, x2) ]	=	3 x1 + 2 x2 + 2
  [element (x1, x2) ]	=	x1 + 2 x2
  [true]	=	0
  [case9 (x1, ..., x4) ]	=	3 x1 + 2 x2 + 3 x3 + 2
  [resource]	=	0
  [and (x1, x2) ]	=	2 x1 + 2 x2
  [locker2_adduniq (x1, x2) ]	=	x1
  [tops (x1) ]	=	x1
  [record_new (x1) ]	=	0
  [istops (x1, x2) ]	=	3 x1 + 2 x2
  [locker2_check_available (x1, x2) ]	=	3 x1 + 2
  [eqs (x1, x2) ]	=	0
  [request]	=	0
  [gen_tag (x1) ]	=	2 x1
  [mcrlrecord]	=	0
  [locker2_map_add_pending (x1, x2, x3) ]	=	3
  [push (x1, x2, x3) ]	=	0
  [empty]	=	0
  [record_update (x1, ..., x4) ]	=	x1 + 2 x2 + 2 x3
  [case1 (x1, ..., x4) ]	=	3 x1 + x2 + 3 x3 + 2
  [locker2_map_claim_lock (x1, x2, x3) ]	=	3 x1 + 2
  [eqc (x1, x2) ]	=	0
  [tuple (x1, x2) ]	=	2 x1 + x2
  [append (x1, x2) ]	=	x1
  [false]	=	1
  [locker2_promote_pending (x1, x2) ]	=	3 x1 + 2
  [record_updates# (x1, x2, x3) ]	=	x1 + x2
  [pushs (x1, x2) ]	=	2 x1 + 3 x2 + 1
  [eqt (x1, x2) ]	=	0
  [subtract (x1, x2) ]	=	x1
  [locker2_map_promote_pending (x1, x2) ]	=	3 x1
  [record_updates (x1, x2, x3) ]	=	x1 + x2
  [nocalls]	=	0
  [record_extract (x1, x2, x3) ]	=	x1
  [andt (x1, x2) ]	=	0
  [case8 (x1, ..., x4) ]	=	2 x1 + 2 x2 + 2
  [s (x1) ]	=	3 x1
  [undefined]	=	0
  [pending]	=	0
  [push1 (x1, ..., x6) ]	=	0
  [not (x1) ]	=	3
  [calls (x1, x2, x3) ]	=	0
  [if (x1, x2, x3) ]	=	x1 + x2
  [excl]	=	0
  [case5 (x1, ..., x4) ]	=	0
  [tuplenil (x1) ]	=	x1
  [imp (x1, x2) ]	=	x1 + 2
  [locker2_obtainables (x1, x2) ]	=	0
  [eq (x1, x2) ]	=	0
  [ok]	=	0
  [tag]	=	0
  [case0 (x1, x2, x3) ]	=	x1 + 2 x2 + 2
  [T]	=	0
  [nil]	=	0
  [int (x1) ]	=	x1
  [pid (x1) ]	=	0
  [equal (x1, x2) ]	=	2
  [pops (x1) ]	=	x1
  [case2 (x1, x2, x3) ]	=	x1 + 2 x2 + 2
  [excllock]	=	0
  [locker2_obtainable (x1, x2) ]	=	0
  [delete (x1, x2) ]	=	x1
  [member (x1, x2) ]	=	3 x1 + 2
  [gen_modtageq (x1, x2) ]	=	x1 + 3
  [locker2_claim_lock (x1, x2, x3) ]	=	x1
  [release]	=	0
  [case4 (x1, x2, x3) ]	=	1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  none

  1.1.6.1: P is empty

  All dependency pairs have been removed.

• The 7th component contains the pair(s)

  locker2_map_claim_lock#( cons( Lock , Locks ) , Resources , Client )

  →

  locker2_map_claim_lock#( Locks , Resources , Client )

  1.1.7: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [locker2_add_pending (x1, x2, x3) ]	=	3 x1 + x2 + x3
  [locker]	=	0
  [a]	=	0
  [stack (x1, x2) ]	=	x1 + 2 x2
  [locker2_remove_pending (x1, x2) ]	=	3 x1 + 3 x2 + 2
  [lock]	=	0
  [or (x1, x2) ]	=	2
  [case6 (x1, ..., x4) ]	=	2 x1 + 2 x2 + 2
  [0]	=	0
  [locker2_check_availables (x1, x2) ]	=	x1 + 2
  [F]	=	0
  [cons (x1, x2) ]	=	2 x1 + 2 x2 + 1
  [locker2_release_lock (x1, x2) ]	=	2 x1 + 3 x2 + 2
  [element (x1, x2) ]	=	x1
  [true]	=	2
  [case9 (x1, ..., x4) ]	=	2 x1
  [resource]	=	2
  [and (x1, x2) ]	=	2 x1 + 2 x2
  [locker2_adduniq (x1, x2) ]	=	x1
  [tops (x1) ]	=	x1
  [record_new (x1) ]	=	0
  [istops (x1, x2) ]	=	2 x1
  [locker2_check_available (x1, x2) ]	=	x1 + 1
  [eqs (x1, x2) ]	=	0
  [request]	=	0
  [gen_tag (x1) ]	=	2 x1
  [mcrlrecord]	=	0
  [locker2_map_add_pending (x1, x2, x3) ]	=	3
  [push (x1, x2, x3) ]	=	3 x1 + 2 x2 + 2 x3
  [empty]	=	0
  [record_update (x1, ..., x4) ]	=	x1 + x2 + 2 x3 + 1
  [case1 (x1, ..., x4) ]	=	3 x1 + 2 x2
  [locker2_map_claim_lock (x1, x2, x3) ]	=	3 x1 + 2
  [eqc (x1, x2) ]	=	0
  [tuple (x1, x2) ]	=	x1 + x2
  [append (x1, x2) ]	=	x1
  [false]	=	0
  [locker2_promote_pending (x1, x2) ]	=	3 x1 + 1
  [pushs (x1, x2) ]	=	x1 + 2 x2 + 1
  [eqt (x1, x2) ]	=	0
  [locker2_map_claim_lock# (x1, x2, x3) ]	=	x1
  [subtract (x1, x2) ]	=	x1
  [locker2_map_promote_pending (x1, x2) ]	=	3 x1
  [record_updates (x1, x2, x3) ]	=	x1 + x2
  [nocalls]	=	0
  [record_extract (x1, x2, x3) ]	=	x1 + 2 x2
  [andt (x1, x2) ]	=	0
  [case8 (x1, ..., x4) ]	=	2 x1 + 2 x2 + 1
  [s (x1) ]	=	0
  [undefined]	=	0
  [pending]	=	0
  [push1 (x1, ..., x6) ]	=	x1 + 2 x2 + x3
  [not (x1) ]	=	1
  [calls (x1, x2, x3) ]	=	x1 + x2
  [if (x1, x2, x3) ]	=	x1 + x2
  [excl]	=	0
  [case5 (x1, ..., x4) ]	=	2 x1 + 3 x2 + 2
  [tuplenil (x1) ]	=	x1
  [imp (x1, x2) ]	=	x1
  [locker2_obtainables (x1, x2) ]	=	2 x1 + 2
  [eq (x1, x2) ]	=	1
  [ok]	=	0
  [tag]	=	0
  [case0 (x1, x2, x3) ]	=	x1 + 2 x2 + 1
  [T]	=	0
  [nil]	=	0
  [int (x1) ]	=	0
  [pid (x1) ]	=	0
  [equal (x1, x2) ]	=	0
  [pops (x1) ]	=	x1
  [case2 (x1, x2, x3) ]	=	x1 + 1
  [excllock]	=	0
  [locker2_obtainable (x1, x2) ]	=	0
  [delete (x1, x2) ]	=	x1
  [member (x1, x2) ]	=	0
  [gen_modtageq (x1, x2) ]	=	x1 + 2 x2
  [locker2_claim_lock (x1, x2, x3) ]	=	x1
  [release]	=	0
  [case4 (x1, x2, x3) ]	=	2
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  none

  1.1.7.1: P is empty

  All dependency pairs have been removed.

• The 8th component contains the pair(s)

  case5#( Client , Locks , Lock , true )	→	locker2_obtainables#( Locks , Client )
  locker2_obtainables#( cons( Lock , Locks ) , Client )	→	case5#( Client , Locks , Lock , member( Client , record_extract( Lock , lock , pending ) ) )
  case5#( Client , Locks , Lock , false )	→	locker2_obtainables#( Locks , Client )

  1.1.8: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [locker2_add_pending (x1, x2, x3) ]	=	3 x1 + 2 x2 + 3 x3
  [a]	=	0
  [locker]	=	0
  [stack (x1, x2) ]	=	x1 + x2
  [locker2_remove_pending (x1, x2) ]	=	3 x1
  [lock]	=	0
  [or (x1, x2) ]	=	0
  [case6 (x1, ..., x4) ]	=	0
  [locker2_obtainables# (x1, x2) ]	=	0
  [0]	=	0
  [locker2_check_availables (x1, x2) ]	=	3 x1 + 3 x2 + 2
  [F]	=	0
  [cons (x1, x2) ]	=	x1 + 2 x2
  [locker2_release_lock (x1, x2) ]	=	3 x1 + x2
  [element (x1, x2) ]	=	2 x1
  [true]	=	1
  [case9 (x1, ..., x4) ]	=	2 x1
  [resource]	=	0
  [and (x1, x2) ]	=	2 x1 + 2 x2
  [locker2_adduniq (x1, x2) ]	=	x1
  [tops (x1) ]	=	x1
  [record_new (x1) ]	=	1
  [istops (x1, x2) ]	=	x1 + x2 + 1
  [locker2_check_available (x1, x2) ]	=	0
  [eqs (x1, x2) ]	=	0
  [request]	=	0
  [gen_tag (x1) ]	=	2 x1 + 3
  [mcrlrecord]	=	0
  [locker2_map_add_pending (x1, x2, x3) ]	=	3
  [push (x1, x2, x3) ]	=	x1 + x2 + 2 x3 + 3
  [empty]	=	0
  [record_update (x1, ..., x4) ]	=	x1 + x2 + 2 x3
  [case1 (x1, ..., x4) ]	=	3 x1 + x2 + 3 x3 + x4
  [locker2_map_claim_lock (x1, x2, x3) ]	=	2 x1
  [eqc (x1, x2) ]	=	0
  [tuple (x1, x2) ]	=	x1 + x2
  [append (x1, x2) ]	=	x1
  [case5# (x1, ..., x4) ]	=	2 x1
  [false]	=	0
  [locker2_promote_pending (x1, x2) ]	=	3 x1
  [pushs (x1, x2) ]	=	x1 + 2 x2 + 1
  [eqt (x1, x2) ]	=	0
  [subtract (x1, x2) ]	=	x1
  [locker2_map_promote_pending (x1, x2) ]	=	3 x1
  [record_updates (x1, x2, x3) ]	=	x1 + 2 x2
  [nocalls]	=	1
  [record_extract (x1, x2, x3) ]	=	x1
  [andt (x1, x2) ]	=	0
  [case8 (x1, ..., x4) ]	=	2 x1 + x2
  [s (x1) ]	=	0
  [undefined]	=	0
  [pending]	=	0
  [push1 (x1, ..., x6) ]	=	x1 + 3
  [not (x1) ]	=	3
  [calls (x1, x2, x3) ]	=	2
  [excl]	=	0
  [if (x1, x2, x3) ]	=	x1 + x2
  [case5 (x1, ..., x4) ]	=	2
  [tuplenil (x1) ]	=	x1
  [imp (x1, x2) ]	=	x1 + 2
  [locker2_obtainables (x1, x2) ]	=	2
  [ok]	=	0
  [eq (x1, x2) ]	=	0
  [tag]	=	0
  [case0 (x1, x2, x3) ]	=	x1 + 2 x2
  [T]	=	0
  [nil]	=	0
  [int (x1) ]	=	0
  [pid (x1) ]	=	0
  [equal (x1, x2) ]	=	0
  [pops (x1) ]	=	x1
  [case2 (x1, x2, x3) ]	=	2 x1
  [excllock]	=	0
  [locker2_obtainable (x1, x2) ]	=	0
  [delete (x1, x2) ]	=	x1
  [member (x1, x2) ]	=	0
  [gen_modtageq (x1, x2) ]	=	0
  [locker2_claim_lock (x1, x2, x3) ]	=	x1
  [release]	=	0
  [case4 (x1, x2, x3) ]	=	1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  locker2_obtainables#( cons( Lock , Locks ) , Client )	→	case5#( Client , Locks , Lock , member( Client , record_extract( Lock , lock , pending ) ) )
  case5#( Client , Locks , Lock , false )	→	locker2_obtainables#( Locks , Client )

  1.1.8.1: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [locker2_add_pending (x1, x2, x3) ]	=	3 x1 + 2 x2 + 3 x3 + 3
  [a]	=	0
  [locker]	=	0
  [stack (x1, x2) ]	=	x1 + x2
  [locker2_remove_pending (x1, x2) ]	=	3 x1 + x2 + 2
  [lock]	=	0
  [or (x1, x2) ]	=	2
  [case6 (x1, ..., x4) ]	=	1
  [locker2_obtainables# (x1, x2) ]	=	2 x1
  [0]	=	0
  [locker2_check_availables (x1, x2) ]	=	2 x1
  [F]	=	0
  [cons (x1, x2) ]	=	x1 + x2 + 2
  [locker2_release_lock (x1, x2) ]	=	3 x1 + 2 x2 + 3
  [element (x1, x2) ]	=	x1 + x2
  [true]	=	0
  [case9 (x1, ..., x4) ]	=	0
  [resource]	=	0
  [and (x1, x2) ]	=	2 x1 + 2 x2
  [locker2_adduniq (x1, x2) ]	=	x1
  [tops (x1) ]	=	x1
  [record_new (x1) ]	=	1
  [istops (x1, x2) ]	=	3
  [locker2_check_available (x1, x2) ]	=	1
  [eqs (x1, x2) ]	=	0
  [request]	=	0
  [gen_tag (x1) ]	=	2 x1 + 1
  [mcrlrecord]	=	0
  [locker2_map_add_pending (x1, x2, x3) ]	=	3
  [push (x1, x2, x3) ]	=	0
  [empty]	=	0
  [record_update (x1, ..., x4) ]	=	x1 + x2 + 1
  [case1 (x1, ..., x4) ]	=	3 x1 + x2 + 3 x3 + 2
  [locker2_map_claim_lock (x1, x2, x3) ]	=	2 x1
  [eqc (x1, x2) ]	=	0
  [tuple (x1, x2) ]	=	x1 + x2
  [append (x1, x2) ]	=	x1
  [case5# (x1, ..., x4) ]	=	2 x1
  [false]	=	0
  [locker2_promote_pending (x1, x2) ]	=	3 x1 + 3
  [pushs (x1, x2) ]	=	2 x1 + x2
  [eqt (x1, x2) ]	=	0
  [subtract (x1, x2) ]	=	x1
  [locker2_map_promote_pending (x1, x2) ]	=	3 x1
  [record_updates (x1, x2, x3) ]	=	x1 + x2
  [nocalls]	=	0
  [record_extract (x1, x2, x3) ]	=	2 x1
  [andt (x1, x2) ]	=	0
  [case8 (x1, ..., x4) ]	=	x1 + x2 + 2
  [s (x1) ]	=	3 x1
  [undefined]	=	0
  [pending]	=	0
  [push1 (x1, ..., x6) ]	=	0
  [not (x1) ]	=	0
  [calls (x1, x2, x3) ]	=	0
  [if (x1, x2, x3) ]	=	x1 + x2
  [excl]	=	0
  [case5 (x1, ..., x4) ]	=	2 x1 + x2 + 1
  [tuplenil (x1) ]	=	x1
  [imp (x1, x2) ]	=	x1
  [locker2_obtainables (x1, x2) ]	=	2 x1
  [ok]	=	0
  [eq (x1, x2) ]	=	2
  [tag]	=	1
  [case0 (x1, x2, x3) ]	=	x1 + x2 + 3
  [T]	=	0
  [nil]	=	0
  [int (x1) ]	=	x1
  [pid (x1) ]	=	0
  [equal (x1, x2) ]	=	0
  [pops (x1) ]	=	x1
  [case2 (x1, x2, x3) ]	=	x1 + 2 x2 + 3
  [excllock]	=	0
  [locker2_obtainable (x1, x2) ]	=	0
  [delete (x1, x2) ]	=	x1
  [member (x1, x2) ]	=	0
  [gen_modtageq (x1, x2) ]	=	3 x1 + 3 x2 + 3
  [locker2_claim_lock (x1, x2, x3) ]	=	x1 + 1
  [release]	=	0
  [case4 (x1, x2, x3) ]	=	1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  case5#( Client , Locks , Lock , false )

  →

  locker2_obtainables#( Locks , Client )

  1.1.8.1.1: dependency graph processor

  The dependency pairs are split into 0 component(s).

• The 9th component contains the pair(s)

  locker2_check_availables#( cons( Resource , Resources ) , Locks )

  →

  locker2_check_availables#( Resources , Locks )

  1.1.9: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [locker2_add_pending (x1, x2, x3) ]	=	2 x1 + 2 x2 + 3 x3 + 1
  [locker]	=	0
  [a]	=	0
  [stack (x1, x2) ]	=	2 x1 + x2
  [locker2_remove_pending (x1, x2) ]	=	3 x1 + 1
  [lock]	=	1
  [or (x1, x2) ]	=	0
  [case6 (x1, ..., x4) ]	=	0
  [0]	=	0
  [locker2_check_availables (x1, x2) ]	=	2 x1 + 2
  [F]	=	0
  [cons (x1, x2) ]	=	x1 + x2 + 1
  [locker2_release_lock (x1, x2) ]	=	x1 + 3 x2 + 3
  [element (x1, x2) ]	=	x1
  [true]	=	0
  [case9 (x1, ..., x4) ]	=	3 x1 + 3 x2
  [resource]	=	1
  [and (x1, x2) ]	=	x1 + 2 x2
  [locker2_adduniq (x1, x2) ]	=	x1
  [tops (x1) ]	=	x1
  [record_new (x1) ]	=	x1 + 3
  [istops (x1, x2) ]	=	x1
  [locker2_check_available (x1, x2) ]	=	0
  [eqs (x1, x2) ]	=	0
  [request]	=	0
  [gen_tag (x1) ]	=	2 x1
  [mcrlrecord]	=	0
  [locker2_map_add_pending (x1, x2, x3) ]	=	3
  [push (x1, x2, x3) ]	=	x1 + 2 x2
  [empty]	=	0
  [record_update (x1, ..., x4) ]	=	x1 + x2 + 1
  [case1 (x1, ..., x4) ]	=	3 x1 + x2 + 2 x3 + 1
  [locker2_map_claim_lock (x1, x2, x3) ]	=	2 x1 + 2
  [eqc (x1, x2) ]	=	0
  [tuple (x1, x2) ]	=	x1 + x2
  [append (x1, x2) ]	=	x1
  [false]	=	0
  [locker2_promote_pending (x1, x2) ]	=	3 x1 + 2
  [pushs (x1, x2) ]	=	2 x1 + x2 + 2
  [eqt (x1, x2) ]	=	0
  [subtract (x1, x2) ]	=	x1
  [locker2_map_promote_pending (x1, x2) ]	=	3 x1
  [record_updates (x1, x2, x3) ]	=	x1 + x2
  [nocalls]	=	0
  [record_extract (x1, x2, x3) ]	=	x1 + x2
  [andt (x1, x2) ]	=	0
  [case8 (x1, ..., x4) ]	=	x1 + x2 + 1
  [s (x1) ]	=	0
  [undefined]	=	0
  [pending]	=	0
  [push1 (x1, ..., x6) ]	=	x1
  [not (x1) ]	=	1
  [calls (x1, x2, x3) ]	=	0
  [if (x1, x2, x3) ]	=	x1 + x2
  [excl]	=	0
  [case5 (x1, ..., x4) ]	=	x1 + 1
  [tuplenil (x1) ]	=	x1
  [imp (x1, x2) ]	=	x1
  [locker2_check_availables# (x1, x2) ]	=	x1
  [locker2_obtainables (x1, x2) ]	=	x1
  [eq (x1, x2) ]	=	0
  [ok]	=	0
  [tag]	=	0
  [case0 (x1, x2, x3) ]	=	2 x1 + x2 + 2
  [T]	=	0
  [nil]	=	0
  [int (x1) ]	=	0
  [pid (x1) ]	=	0
  [equal (x1, x2) ]	=	0
  [pops (x1) ]	=	x1
  [case2 (x1, x2, x3) ]	=	x1 + 2
  [excllock]	=	0
  [locker2_obtainable (x1, x2) ]	=	0
  [delete (x1, x2) ]	=	x1
  [member (x1, x2) ]	=	3 x1
  [gen_modtageq (x1, x2) ]	=	3 x1 + 1
  [locker2_claim_lock (x1, x2, x3) ]	=	x1
  [release]	=	0
  [case4 (x1, x2, x3) ]	=	3
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  none

  1.1.9.1: P is empty

  All dependency pairs have been removed.

• The 10th component contains the pair(s)

  append#( cons( Head , Tail ) , List )

  →

  append#( Tail , List )

  1.1.10: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [locker2_add_pending (x1, x2, x3) ]	=	2 x1 + 2 x2 + 3 x3 + 1
  [locker]	=	0
  [a]	=	0
  [stack (x1, x2) ]	=	2 x1 + x2
  [locker2_remove_pending (x1, x2) ]	=	3 x1 + 1
  [lock]	=	1
  [or (x1, x2) ]	=	0
  [case6 (x1, ..., x4) ]	=	0
  [0]	=	0
  [locker2_check_availables (x1, x2) ]	=	2 x1 + 2
  [F]	=	0
  [cons (x1, x2) ]	=	x1 + x2 + 1
  [locker2_release_lock (x1, x2) ]	=	x1 + 3 x2 + 3
  [element (x1, x2) ]	=	x1
  [true]	=	0
  [case9 (x1, ..., x4) ]	=	3 x1 + 3 x2
  [resource]	=	1
  [and (x1, x2) ]	=	x1 + 2 x2
  [locker2_adduniq (x1, x2) ]	=	x1
  [tops (x1) ]	=	x1
  [record_new (x1) ]	=	x1 + 3
  [istops (x1, x2) ]	=	x1
  [locker2_check_available (x1, x2) ]	=	0
  [eqs (x1, x2) ]	=	0
  [request]	=	0
  [gen_tag (x1) ]	=	2 x1
  [mcrlrecord]	=	0
  [locker2_map_add_pending (x1, x2, x3) ]	=	3
  [push (x1, x2, x3) ]	=	x1 + 2 x2
  [empty]	=	0
  [record_update (x1, ..., x4) ]	=	x1 + x2 + 1
  [case1 (x1, ..., x4) ]	=	3 x1 + x2 + 2 x3 + 1
  [locker2_map_claim_lock (x1, x2, x3) ]	=	2 x1 + 2
  [eqc (x1, x2) ]	=	0
  [tuple (x1, x2) ]	=	x1 + x2
  [append (x1, x2) ]	=	x1
  [false]	=	0
  [locker2_promote_pending (x1, x2) ]	=	3 x1 + 2
  [pushs (x1, x2) ]	=	2 x1 + x2 + 2
  [eqt (x1, x2) ]	=	0
  [subtract (x1, x2) ]	=	x1
  [locker2_map_promote_pending (x1, x2) ]	=	3 x1
  [record_updates (x1, x2, x3) ]	=	x1 + x2
  [nocalls]	=	0
  [record_extract (x1, x2, x3) ]	=	x1 + x2
  [andt (x1, x2) ]	=	0
  [case8 (x1, ..., x4) ]	=	x1 + x2 + 1
  [s (x1) ]	=	0
  [undefined]	=	0
  [pending]	=	0
  [push1 (x1, ..., x6) ]	=	x1
  [not (x1) ]	=	1
  [calls (x1, x2, x3) ]	=	0
  [if (x1, x2, x3) ]	=	x1 + x2
  [excl]	=	0
  [case5 (x1, ..., x4) ]	=	x1 + 1
  [tuplenil (x1) ]	=	x1
  [imp (x1, x2) ]	=	x1
  [locker2_obtainables (x1, x2) ]	=	x1
  [eq (x1, x2) ]	=	0
  [ok]	=	0
  [tag]	=	0
  [case0 (x1, x2, x3) ]	=	2 x1 + x2 + 2
  [T]	=	0
  [nil]	=	0
  [int (x1) ]	=	0
  [pid (x1) ]	=	0
  [equal (x1, x2) ]	=	0
  [pops (x1) ]	=	x1
  [case2 (x1, x2, x3) ]	=	x1 + 2
  [append# (x1, x2) ]	=	x1
  [excllock]	=	0
  [locker2_obtainable (x1, x2) ]	=	0
  [delete (x1, x2) ]	=	x1
  [member (x1, x2) ]	=	3 x1
  [gen_modtageq (x1, x2) ]	=	3 x1 + 1
  [locker2_claim_lock (x1, x2, x3) ]	=	x1
  [release]	=	0
  [case4 (x1, x2, x3) ]	=	3
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  none

  1.1.10.1: P is empty

  All dependency pairs have been removed.

• The 11th component contains the pair(s)

  subtract#( List , cons( Head , Tail ) )

  →

  subtract#( delete( Head , List ) , Tail )

  1.1.11: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [locker2_add_pending (x1, x2, x3) ]	=	3 x1 + 2 x2 + 3 x3 + 1
  [locker]	=	0
  [a]	=	0
  [stack (x1, x2) ]	=	x1 + x2
  [locker2_remove_pending (x1, x2) ]	=	3 x1 + 2
  [lock]	=	0
  [or (x1, x2) ]	=	1
  [case6 (x1, ..., x4) ]	=	3 x1 + 2 x2 + 2
  [0]	=	0
  [locker2_check_availables (x1, x2) ]	=	x1
  [F]	=	0
  [cons (x1, x2) ]	=	x1 + 2 x2 + 1
  [locker2_release_lock (x1, x2) ]	=	2 x1 + 2 x2 + 1
  [element (x1, x2) ]	=	x1
  [true]	=	0
  [case9 (x1, ..., x4) ]	=	0
  [resource]	=	0
  [and (x1, x2) ]	=	2 x1 + 2 x2
  [locker2_adduniq (x1, x2) ]	=	x1
  [tops (x1) ]	=	x1
  [record_new (x1) ]	=	0
  [istops (x1, x2) ]	=	2 x1
  [locker2_check_available (x1, x2) ]	=	2 x1
  [eqs (x1, x2) ]	=	0
  [request]	=	0
  [gen_tag (x1) ]	=	2 x1
  [mcrlrecord]	=	0
  [locker2_map_add_pending (x1, x2, x3) ]	=	3
  [push (x1, x2, x3) ]	=	x1 + 2 x2 + 3 x3
  [empty]	=	0
  [record_update (x1, ..., x4) ]	=	x1 + 2 x2 + 1
  [case1 (x1, ..., x4) ]	=	3 x1 + x2 + 3 x3 + 1
  [locker2_map_claim_lock (x1, x2, x3) ]	=	x1
  [eqc (x1, x2) ]	=	0
  [tuple (x1, x2) ]	=	x1 + x2
  [append (x1, x2) ]	=	x1
  [false]	=	0
  [locker2_promote_pending (x1, x2) ]	=	3 x1 + 2
  [pushs (x1, x2) ]	=	x1 + 2 x2
  [eqt (x1, x2) ]	=	0
  [subtract (x1, x2) ]	=	x1
  [locker2_map_promote_pending (x1, x2) ]	=	3 x1
  [record_updates (x1, x2, x3) ]	=	x1 + x2
  [nocalls]	=	0
  [record_extract (x1, x2, x3) ]	=	x1
  [andt (x1, x2) ]	=	0
  [case8 (x1, ..., x4) ]	=	2 x1 + x2 + 1
  [s (x1) ]	=	0
  [undefined]	=	0
  [pending]	=	0
  [push1 (x1, ..., x6) ]	=	x1 + x2 + 2 x3
  [not (x1) ]	=	1
  [calls (x1, x2, x3) ]	=	x1
  [if (x1, x2, x3) ]	=	x1 + x2
  [excl]	=	0
  [case5 (x1, ..., x4) ]	=	2 x1 + 2 x2
  [tuplenil (x1) ]	=	2 x1
  [imp (x1, x2) ]	=	x1 + 3
  [locker2_obtainables (x1, x2) ]	=	2 x1
  [eq (x1, x2) ]	=	0
  [ok]	=	0
  [tag]	=	0
  [case0 (x1, x2, x3) ]	=	x1 + 2 x2 + 2
  [T]	=	0
  [nil]	=	0
  [int (x1) ]	=	0
  [pid (x1) ]	=	0
  [equal (x1, x2) ]	=	0
  [pops (x1) ]	=	x1
  [case2 (x1, x2, x3) ]	=	x1 + x2 + 1
  [delete (x1, x2) ]	=	x1
  [excllock]	=	0
  [locker2_obtainable (x1, x2) ]	=	0
  [member (x1, x2) ]	=	0
  [gen_modtageq (x1, x2) ]	=	2 x1 + 2 x2 + 2
  [locker2_claim_lock (x1, x2, x3) ]	=	0
  [release]	=	0
  [subtract# (x1, x2) ]	=	x1
  [case4 (x1, x2, x3) ]	=	2
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  none

  1.1.11.1: P is empty

  All dependency pairs have been removed.