Certification Problem

Input (TPDB TRS_Standard/CiME_04/mucrl1)

The rewrite relation of the following TRS is considered.

There are 377 ruless (increase limit for explicit display).

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

eqt^#(pid(N1),pid(N2))	→	eqt^#(N1,N2)	(378)
eqt^#(cons(H1,T1),cons(H2,T2))	→	eqt^#(T1,T2)	(379)
eqt^#(cons(H1,T1),cons(H2,T2))	→	eqt^#(H1,H2)	(380)
eqt^#(cons(H1,T1),cons(H2,T2))	→	and^#(eqt(H1,H2),eqt(T1,T2))	(381)
eqt^#(tuple(H1,T1),tuple(H2,T2))	→	eqt^#(T1,T2)	(382)
eqt^#(tuple(H1,T1),tuple(H2,T2))	→	eqt^#(H1,H2)	(383)
eqt^#(tuple(H1,T1),tuple(H2,T2))	→	and^#(eqt(H1,H2),eqt(T1,T2))	(384)
eqt^#(tuplenil(H1),tuplenil(H2))	→	eqt^#(H1,H2)	(385)
element^#(int(s(s(N1))),tuple(T1,T2))	→	element^#(int(s(N1)),T2)	(386)
record_updates^#(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields))	→	record_update^#(Record,Name,Field,NewF)	(387)
record_updates^#(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields))	→	record_updates^#(record_update(Record,Name,Field,NewF),Name,Fields)	(388)
locker2_map_promote_pending^#(cons(Lock,Locks),Pending)	→	locker2_map_promote_pending^#(Locks,Pending)	(389)
locker2_map_promote_pending^#(cons(Lock,Locks),Pending)	→	locker2_promote_pending^#(Lock,Pending)	(390)
locker2_map_claim_lock^#(cons(Lock,Locks),Resources,Client)	→	locker2_map_claim_lock^#(Locks,Resources,Client)	(391)
locker2_promote_pending^#(Lock,Client)	→	record_extract^#(Lock,lock,pending)	(392)
locker2_promote_pending^#(Lock,Client)	→	case0^#(Client,Lock,record_extract(Lock,lock,pending))	(393)
case0^#(Client,Lock,cons(Client,Pendings))	→	record_updates^#(Lock,lock,cons(tuple(excl,tuplenil(Client)),cons(tuple(pending,tuplenil(Pendings)),nil)))	(394)
locker2_remove_pending^#(Lock,Client)	→	record_extract^#(Lock,lock,pending)	(395)
locker2_remove_pending^#(Lock,Client)	→	subtract^#(record_extract(Lock,lock,pending),cons(Client,nil))	(396)
locker2_remove_pending^#(Lock,Client)	→	record_updates^#(Lock,lock,cons(tuple(pending,tuplenil(subtract(record_extract(Lock,lock,pending),cons(Client,nil)))),nil))	(397)
locker2_add_pending^#(Lock,Resources,Client)	→	record_extract^#(Lock,lock,resource)	(398)
locker2_add_pending^#(Lock,Resources,Client)	→	member^#(record_extract(Lock,lock,resource),Resources)	(399)
locker2_add_pending^#(Lock,Resources,Client)	→	case1^#(Client,Resources,Lock,member(record_extract(Lock,lock,resource),Resources))	(400)
case1^#(Client,Resources,Lock,true)	→	record_extract^#(Lock,lock,pending)	(401)
case1^#(Client,Resources,Lock,true)	→	append^#(record_extract(Lock,lock,pending),cons(Client,nil))	(402)
case1^#(Client,Resources,Lock,true)	→	record_updates^#(Lock,lock,cons(tuple(pending,tuplenil(append(record_extract(Lock,lock,pending),cons(Client,nil)))),nil))	(403)
locker2_release_lock^#(Lock,Client)	→	record_extract^#(Lock,lock,excl)	(404)
locker2_release_lock^#(Lock,Client)	→	gen_modtageq^#(Client,record_extract(Lock,lock,excl))	(405)
locker2_release_lock^#(Lock,Client)	→	case2^#(Client,Lock,gen_modtageq(Client,record_extract(Lock,lock,excl)))	(406)
case2^#(Client,Lock,true)	→	record_updates^#(Lock,lock,cons(tuple(excllock,excl),nil))	(407)
locker2_obtainables^#(cons(Lock,Locks),Client)	→	record_extract^#(Lock,lock,pending)	(408)
locker2_obtainables^#(cons(Lock,Locks),Client)	→	member^#(Client,record_extract(Lock,lock,pending))	(409)
locker2_obtainables^#(cons(Lock,Locks),Client)	→	case5^#(Client,Locks,Lock,member(Client,record_extract(Lock,lock,pending)))	(410)
case5^#(Client,Locks,Lock,true)	→	locker2_obtainables^#(Locks,Client)	(411)
case5^#(Client,Locks,Lock,false)	→	locker2_obtainables^#(Locks,Client)	(412)
locker2_check_available^#(Resource,cons(Lock,Locks))	→	record_extract^#(Lock,lock,resource)	(413)
locker2_check_available^#(Resource,cons(Lock,Locks))	→	case6^#(Locks,Lock,Resource,equal(Resource,record_extract(Lock,lock,resource)))	(414)
case6^#(Locks,Lock,Resource,true)	→	record_extract^#(Lock,lock,pending)	(415)
case6^#(Locks,Lock,Resource,true)	→	record_extract^#(Lock,lock,excl)	(416)
case6^#(Locks,Lock,Resource,false)	→	locker2_check_available^#(Resource,Locks)	(417)
locker2_check_availables^#(cons(Resource,Resources),Locks)	→	locker2_check_availables^#(Resources,Locks)	(418)
locker2_check_availables^#(cons(Resource,Resources),Locks)	→	locker2_check_available^#(Resource,Locks)	(419)
append^#(cons(Head,Tail),List)	→	append^#(Tail,List)	(420)
subtract^#(List,cons(Head,Tail))	→	delete^#(Head,List)	(421)
subtract^#(List,cons(Head,Tail))	→	subtract^#(delete(Head,List),Tail)	(422)
delete^#(E,cons(Head,Tail))	→	case8^#(Tail,Head,E,equal(E,Head))	(423)
case8^#(Tail,Head,E,false)	→	delete^#(E,Tail)	(424)
member^#(E,cons(Head,Tail))	→	case9^#(Tail,Head,E,equal(E,Head))	(425)
case9^#(Tail,Head,E,false)	→	member^#(E,Tail)	(426)
eqs^#(stack(E1,S1),stack(E2,S2))	→	eqs^#(S1,S2)	(427)
eqs^#(stack(E1,S1),stack(E2,S2))	→	eqt^#(E1,E2)	(428)
eqs^#(stack(E1,S1),stack(E2,S2))	→	and^#(eqt(E1,E2),eqs(S1,S2))	(429)
istops^#(E1,stack(E2,S1))	→	eqt^#(E1,E2)	(430)
eqc^#(calls(E1,S1,CS1),calls(E2,S2,CS2))	→	eqc^#(CS1,CS2)	(431)
eqc^#(calls(E1,S1,CS1),calls(E2,S2,CS2))	→	eqs^#(S1,S2)	(432)
eqc^#(calls(E1,S1,CS1),calls(E2,S2,CS2))	→	and^#(eqs(S1,S2),eqc(CS1,CS2))	(433)
eqc^#(calls(E1,S1,CS1),calls(E2,S2,CS2))	→	eqt^#(E1,E2)	(434)
eqc^#(calls(E1,S1,CS1),calls(E2,S2,CS2))	→	and^#(eqt(E1,E2),and(eqs(S1,S2),eqc(CS1,CS2)))	(435)
push^#(E1,E2,calls(E3,S1,CS1))	→	eqt^#(E1,E3)	(436)
push^#(E1,E2,calls(E3,S1,CS1))	→	push1^#(E1,E2,E3,S1,CS1,eqt(E1,E3))	(437)
push1^#(E1,E2,E3,S1,CS1,T)	→	pushs^#(E2,S1)	(438)

1.1 Dependency Graph Processor

The dependency pairs are split into 10 components.

The 1^st component contains the pair
element^#(int(s(s(N1))),tuple(T1,T2)) → element^#(int(s(N1)),T2) (386)

1.1.1 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

element^#(int(s(s(N1))),tuple(T1,T2)) → element^#(int(s(N1)),T2) (386)

2 > 2

As there is no critical graph in the transitive closure, there are no infinite chains.
The 2^nd component contains the pair
locker2_map_promote_pending^#(cons(Lock,Locks),Pending) → locker2_map_promote_pending^#(Locks,Pending) (389)

1.1.2 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

locker2_map_promote_pending^#(cons(Lock,Locks),Pending) → locker2_map_promote_pending^#(Locks,Pending) (389)

2 ≥ 2

1 > 1

As there is no critical graph in the transitive closure, there are no infinite chains.
The 3^rd component contains the pair
locker2_map_claim_lock^#(cons(Lock,Locks),Resources,Client) → locker2_map_claim_lock^#(Locks,Resources,Client) (391)

1.1.3 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

locker2_map_claim_lock^#(cons(Lock,Locks),Resources,Client) → locker2_map_claim_lock^#(Locks,Resources,Client) (391)

3 ≥ 3

2 ≥ 2

1 > 1

As there is no critical graph in the transitive closure, there are no infinite chains.
The 4^th component contains the pair
subtract^#(List,cons(Head,Tail)) → subtract^#(delete(Head,List),Tail) (422)

1.1.4 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

subtract^#(List,cons(Head,Tail)) → subtract^#(delete(Head,List),Tail) (422)

2 > 2

As there is no critical graph in the transitive closure, there are no infinite chains.
The 5^th component contains the pair
record_updates^#(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields)) → record_updates^#(record_update(Record,Name,Field,NewF),Name,Fields) (388)

1.1.5 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

record_updates^#(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields)) → record_updates^#(record_update(Record,Name,Field,NewF),Name,Fields) (388)

3 > 3

2 ≥ 2

As there is no critical graph in the transitive closure, there are no infinite chains.
The 6^th component contains the pair
append^#(cons(Head,Tail),List) → append^#(Tail,List) (420)

1.1.6 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

append^#(cons(Head,Tail),List) → append^#(Tail,List) (420)

2 ≥ 2

1 > 1

As there is no critical graph in the transitive closure, there are no infinite chains.
The 7^th component contains the pair
locker2_check_availables^#(cons(Resource,Resources),Locks) → locker2_check_availables^#(Resources,Locks) (418)

1.1.7 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

locker2_check_availables^#(cons(Resource,Resources),Locks) → locker2_check_availables^#(Resources,Locks) (418)

2 ≥ 2

1 > 1

As there is no critical graph in the transitive closure, there are no infinite chains.
The 8^th component contains the pair
eqc^#(calls(E1,S1,CS1),calls(E2,S2,CS2)) → eqc^#(CS1,CS2) (431)

1.1.8 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

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

2 > 2

1 > 1

As there is no critical graph in the transitive closure, there are no infinite chains.
The 9^th component contains the pair
eqs^#(stack(E1,S1),stack(E2,S2)) → eqs^#(S1,S2) (427)

1.1.9 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

eqs^#(stack(E1,S1),stack(E2,S2)) → eqs^#(S1,S2) (427)

2 > 2

1 > 1

As there is no critical graph in the transitive closure, there are no infinite chains.

The 10^th component contains the pair

eqt^#(tuplenil(H1),tuplenil(H2))	→	eqt^#(H1,H2)	(385)
eqt^#(tuple(H1,T1),tuple(H2,T2))	→	eqt^#(H1,H2)	(383)
eqt^#(tuple(H1,T1),tuple(H2,T2))	→	eqt^#(T1,T2)	(382)
eqt^#(cons(H1,T1),cons(H2,T2))	→	eqt^#(H1,H2)	(380)
eqt^#(cons(H1,T1),cons(H2,T2))	→	eqt^#(T1,T2)	(379)
eqt^#(pid(N1),pid(N2))	→	eqt^#(N1,N2)	(378)

1.1.10 Subterm Criterion Processor

We use the projection

π(eqt^#)

and remove the pairs:

eqt^#(tuplenil(H1),tuplenil(H2))	→	eqt^#(H1,H2)	(385)
eqt^#(tuple(H1,T1),tuple(H2,T2))	→	eqt^#(H1,H2)	(383)
eqt^#(tuple(H1,T1),tuple(H2,T2))	→	eqt^#(T1,T2)	(382)
eqt^#(cons(H1,T1),cons(H2,T2))	→	eqt^#(H1,H2)	(380)
eqt^#(cons(H1,T1),cons(H2,T2))	→	eqt^#(T1,T2)	(379)
eqt^#(pid(N1),pid(N2))	→	eqt^#(N1,N2)	(378)

1.1.10.1 P is empty

There are no pairs anymore.

Certification Problem

Input (TPDB TRS_Standard/CiME_04/mucrl1)

Property / Task

Answer / Result

Proof (by ttt2 @ termCOMP 2023)

1 Dependency Pair Transformation

1.1 Dependency Graph Processor

1.1.1 Size-Change Termination

1.1.2 Size-Change Termination

1.1.3 Size-Change Termination

1.1.4 Size-Change Termination

1.1.5 Size-Change Termination

1.1.6 Size-Change Termination

1.1.7 Size-Change Termination

1.1.8 Size-Change Termination

1.1.9 Size-Change Termination

1.1.10 Subterm Criterion Processor

1.1.10.1 P is empty