Certification Problem

Input (TPDB TRS_Standard/Kaliszyk_19/arith)

The rewrite relation of the following TRS is considered.

There are 108 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.

SUC^#(NUMERAL(n))	→	SUC^#(n)	(109)
SUC^#(NUMERAL(n))	→	NUMERAL^#(SUC(n))	(110)
SUC^#(BIT1(n))	→	SUC^#(n)	(111)
SUC^#(BIT1(n))	→	BIT0^#(SUC(n))	(112)
PRE^#(NUMERAL(n))	→	PRE^#(n)	(113)
PRE^#(NUMERAL(n))	→	NUMERAL^#(PRE(n))	(114)
PRE^#(BIT0(n))	→	PRE^#(n)	(115)
PRE^#(BIT0(n))	→	eq^#(n,0)	(116)
PRE^#(BIT1(n))	→	BIT0^#(n)	(117)
plus^#(NUMERAL(m),NUMERAL(n))	→	plus^#(m,n)	(118)
plus^#(NUMERAL(m),NUMERAL(n))	→	NUMERAL^#(plus(m,n))	(119)
plus^#(BIT0(m),BIT0(n))	→	plus^#(m,n)	(120)
plus^#(BIT0(m),BIT0(n))	→	BIT0^#(plus(m,n))	(121)
plus^#(BIT0(m),BIT1(n))	→	plus^#(m,n)	(122)
plus^#(BIT1(m),BIT0(n))	→	plus^#(m,n)	(123)
plus^#(BIT1(m),BIT1(n))	→	plus^#(m,n)	(124)
plus^#(BIT1(m),BIT1(n))	→	SUC^#(plus(m,n))	(125)
plus^#(BIT1(m),BIT1(n))	→	BIT0^#(SUC(plus(m,n)))	(126)
mult^#(NUMERAL(m),NUMERAL(n))	→	mult^#(m,n)	(127)
mult^#(NUMERAL(m),NUMERAL(n))	→	NUMERAL^#(mult(m,n))	(128)
mult^#(BIT0(m),BIT0(n))	→	mult^#(m,n)	(129)
mult^#(BIT0(m),BIT0(n))	→	BIT0^#(mult(m,n))	(130)
mult^#(BIT0(m),BIT0(n))	→	BIT0^#(BIT0(mult(m,n)))	(131)
mult^#(BIT0(m),BIT1(n))	→	mult^#(m,n)	(132)
mult^#(BIT0(m),BIT1(n))	→	BIT0^#(mult(m,n))	(133)
mult^#(BIT0(m),BIT1(n))	→	BIT0^#(BIT0(mult(m,n)))	(134)
mult^#(BIT0(m),BIT1(n))	→	plus^#(BIT0(m),BIT0(BIT0(mult(m,n))))	(135)
mult^#(BIT1(m),BIT0(n))	→	mult^#(m,n)	(136)
mult^#(BIT1(m),BIT0(n))	→	BIT0^#(mult(m,n))	(137)
mult^#(BIT1(m),BIT0(n))	→	BIT0^#(BIT0(mult(m,n)))	(138)
mult^#(BIT1(m),BIT0(n))	→	plus^#(BIT0(n),BIT0(BIT0(mult(m,n))))	(139)
mult^#(BIT1(m),BIT1(n))	→	mult^#(m,n)	(140)
mult^#(BIT1(m),BIT1(n))	→	BIT0^#(mult(m,n))	(141)
mult^#(BIT1(m),BIT1(n))	→	BIT0^#(BIT0(mult(m,n)))	(142)
mult^#(BIT1(m),BIT1(n))	→	BIT0^#(n)	(143)
mult^#(BIT1(m),BIT1(n))	→	plus^#(BIT1(m),BIT0(n))	(144)
mult^#(BIT1(m),BIT1(n))	→	plus^#(plus(BIT1(m),BIT0(n)),BIT0(BIT0(mult(m,n))))	(145)
exp^#(NUMERAL(m),NUMERAL(n))	→	exp^#(m,n)	(146)
exp^#(NUMERAL(m),NUMERAL(n))	→	NUMERAL^#(exp(m,n))	(147)
exp^#(0,BIT0(n))	→	exp^#(0,n)	(148)
exp^#(0,BIT0(n))	→	mult^#(exp(0,n),exp(0,n))	(149)
exp^#(BIT0(m),BIT0(n))	→	exp^#(BIT0(m),n)	(150)
exp^#(BIT0(m),BIT0(n))	→	mult^#(exp(BIT0(m),n),exp(BIT0(m),n))	(151)
exp^#(BIT1(m),BIT0(n))	→	exp^#(BIT1(m),n)	(152)
exp^#(BIT1(m),BIT0(n))	→	mult^#(exp(BIT1(m),n),exp(BIT1(m),n))	(153)
exp^#(BIT0(m),BIT1(n))	→	exp^#(BIT0(m),n)	(154)
exp^#(BIT0(m),BIT1(n))	→	mult^#(BIT0(m),exp(BIT0(m),n))	(155)
exp^#(BIT0(m),BIT1(n))	→	mult^#(mult(BIT0(m),exp(BIT0(m),n)),exp(BIT0(m),n))	(156)
exp^#(BIT1(m),BIT1(n))	→	exp^#(BIT1(m),n)	(157)
exp^#(BIT1(m),BIT1(n))	→	mult^#(BIT1(m),exp(BIT1(m),n))	(158)
exp^#(BIT1(m),BIT1(n))	→	mult^#(mult(BIT1(m),exp(BIT1(m),n)),exp(BIT1(m),n))	(159)
EVEN^#(NUMERAL(n))	→	EVEN^#(n)	(160)
ODD^#(NUMERAL(n))	→	ODD^#(n)	(161)
eq^#(NUMERAL(m),NUMERAL(n))	→	eq^#(m,n)	(162)
eq^#(BIT0(n),0)	→	eq^#(n,0)	(163)
eq^#(0,BIT0(n))	→	eq^#(0,n)	(164)
eq^#(BIT0(m),BIT0(n))	→	eq^#(m,n)	(165)
eq^#(BIT1(m),BIT1(n))	→	eq^#(m,n)	(166)
le^#(NUMERAL(m),NUMERAL(n))	→	le^#(m,n)	(167)
le^#(BIT0(n),0)	→	le^#(n,0)	(168)
le^#(BIT0(m),BIT0(n))	→	le^#(m,n)	(169)
le^#(BIT0(m),BIT1(n))	→	le^#(m,n)	(170)
le^#(BIT1(m),BIT0(n))	→	lt^#(m,n)	(171)
le^#(BIT1(m),BIT1(n))	→	le^#(m,n)	(172)
lt^#(NUMERAL(m),NUMERAL(n))	→	lt^#(m,n)	(173)
lt^#(0,BIT0(n))	→	lt^#(0,n)	(174)
lt^#(BIT0(m),BIT0(n))	→	lt^#(m,n)	(175)
lt^#(BIT0(m),BIT1(n))	→	le^#(m,n)	(176)
lt^#(BIT1(m),BIT0(n))	→	lt^#(m,n)	(177)
lt^#(BIT1(m),BIT1(n))	→	lt^#(m,n)	(178)
ge^#(NUMERAL(n),NUMERAL(m))	→	ge^#(n,m)	(179)
ge^#(0,BIT0(n))	→	ge^#(0,n)	(180)
ge^#(BIT0(n),BIT0(m))	→	ge^#(n,m)	(181)
ge^#(BIT1(n),BIT0(m))	→	ge^#(n,m)	(182)
ge^#(BIT0(n),BIT1(m))	→	gt^#(n,m)	(183)
ge^#(BIT1(n),BIT1(m))	→	ge^#(n,m)	(184)
gt^#(NUMERAL(n),NUMERAL(m))	→	gt^#(n,m)	(185)
gt^#(BIT0(n),0)	→	gt^#(n,0)	(186)
gt^#(BIT0(n),BIT0(m))	→	gt^#(n,m)	(187)
gt^#(BIT1(n),BIT0(m))	→	ge^#(n,m)	(188)
gt^#(BIT0(n),BIT1(m))	→	gt^#(n,m)	(189)
gt^#(BIT1(n),BIT1(m))	→	gt^#(n,m)	(190)
minus^#(NUMERAL(m),NUMERAL(n))	→	minus^#(m,n)	(191)
minus^#(NUMERAL(m),NUMERAL(n))	→	NUMERAL^#(minus(m,n))	(192)
minus^#(BIT0(m),BIT0(n))	→	minus^#(m,n)	(193)
minus^#(BIT0(m),BIT0(n))	→	BIT0^#(minus(m,n))	(194)
minus^#(BIT0(m),BIT1(n))	→	minus^#(m,n)	(195)
minus^#(BIT0(m),BIT1(n))	→	BIT0^#(minus(m,n))	(196)
minus^#(BIT0(m),BIT1(n))	→	PRE^#(BIT0(minus(m,n)))	(197)
minus^#(BIT1(m),BIT0(n))	→	minus^#(m,n)	(198)
minus^#(BIT1(m),BIT0(n))	→	le^#(n,m)	(199)
minus^#(BIT1(m),BIT1(n))	→	minus^#(m,n)	(200)
minus^#(BIT1(m),BIT1(n))	→	BIT0^#(minus(m,n))	(201)

1.1 Dependency Graph Processor

The dependency pairs are split into 20 components.

The 1^st component contains the pair

eq^#(BIT1(m),BIT1(n)) → eq^#(m,n) (166)

eq^#(BIT0(m),BIT0(n)) → eq^#(m,n) (165)

eq^#(NUMERAL(m),NUMERAL(n)) → eq^#(m,n) (162)

1.1.1 Size-Change Termination

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

eq^#(BIT1(m),BIT1(n)) → eq^#(m,n) (166)

2 > 2

1 > 1

eq^#(BIT0(m),BIT0(n)) → eq^#(m,n) (165)

2 > 2

1 > 1

eq^#(NUMERAL(m),NUMERAL(n)) → eq^#(m,n) (162)

2 > 2

1 > 1

As there is no critical graph in the transitive closure, there are no infinite chains.
The 2^nd component contains the pair
eq^#(0,BIT0(n)) → eq^#(0,n) (164)

1.1.2 Size-Change Termination

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

eq^#(0,BIT0(n)) → eq^#(0,n) (164)

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
exp^#(NUMERAL(m),NUMERAL(n)) → exp^#(m,n) (146)

1.1.3 Size-Change Termination

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

exp^#(NUMERAL(m),NUMERAL(n)) → exp^#(m,n) (146)

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

exp^#(BIT0(m),BIT1(n)) → exp^#(BIT0(m),n) (154)

exp^#(BIT0(m),BIT0(n)) → exp^#(BIT0(m),n) (150)

1.1.4 Size-Change Termination

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

exp^#(BIT0(m),BIT1(n)) → exp^#(BIT0(m),n) (154)

2 > 2

1 ≥ 1

exp^#(BIT0(m),BIT0(n)) → exp^#(BIT0(m),n) (150)

2 > 2

1 ≥ 1

As there is no critical graph in the transitive closure, there are no infinite chains.
The 5^th component contains the pair
exp^#(0,BIT0(n)) → exp^#(0,n) (148)

1.1.5 Size-Change Termination

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

exp^#(0,BIT0(n)) → exp^#(0,n) (148)

2 > 2

1 ≥ 1

As there is no critical graph in the transitive closure, there are no infinite chains.
The 6^th component contains the pair

exp^#(BIT1(m),BIT1(n)) → exp^#(BIT1(m),n) (157)

exp^#(BIT1(m),BIT0(n)) → exp^#(BIT1(m),n) (152)

1.1.6 Size-Change Termination

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

exp^#(BIT1(m),BIT1(n)) → exp^#(BIT1(m),n) (157)

2 > 2

1 ≥ 1

exp^#(BIT1(m),BIT0(n)) → exp^#(BIT1(m),n) (152)

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

mult^#(BIT1(m),BIT1(n))	→	mult^#(m,n)	(140)
mult^#(BIT1(m),BIT0(n))	→	mult^#(m,n)	(136)
mult^#(BIT0(m),BIT1(n))	→	mult^#(m,n)	(132)
mult^#(BIT0(m),BIT0(n))	→	mult^#(m,n)	(129)
mult^#(NUMERAL(m),NUMERAL(n))	→	mult^#(m,n)	(127)

1.1.7 Size-Change Termination

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

mult^#(BIT1(m),BIT1(n))	→	mult^#(m,n)	(140)

2	>	2
1	>	1
mult^#(BIT1(m),BIT0(n))	→	mult^#(m,n)	(136)

2	>	2
1	>	1
mult^#(BIT0(m),BIT1(n))	→	mult^#(m,n)	(132)

2	>	2
1	>	1
mult^#(BIT0(m),BIT0(n))	→	mult^#(m,n)	(129)

2	>	2
1	>	1
mult^#(NUMERAL(m),NUMERAL(n))	→	mult^#(m,n)	(127)

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

plus^#(BIT1(m),BIT0(n))	→	plus^#(m,n)	(123)
plus^#(BIT1(m),BIT1(n))	→	plus^#(m,n)	(124)
plus^#(BIT0(m),BIT1(n))	→	plus^#(m,n)	(122)
plus^#(BIT0(m),BIT0(n))	→	plus^#(m,n)	(120)
plus^#(NUMERAL(m),NUMERAL(n))	→	plus^#(m,n)	(118)

1.1.8 Size-Change Termination

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

plus^#(BIT1(m),BIT0(n))	→	plus^#(m,n)	(123)

2	>	2
1	>	1
plus^#(BIT1(m),BIT1(n))	→	plus^#(m,n)	(124)

2	>	2
1	>	1
plus^#(BIT0(m),BIT1(n))	→	plus^#(m,n)	(122)

2	>	2
1	>	1
plus^#(BIT0(m),BIT0(n))	→	plus^#(m,n)	(120)

2	>	2
1	>	1
plus^#(NUMERAL(m),NUMERAL(n))	→	plus^#(m,n)	(118)

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

SUC^#(BIT1(n)) → SUC^#(n) (111)

SUC^#(NUMERAL(n)) → SUC^#(n) (109)

1.1.9 Size-Change Termination

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

SUC^#(BIT1(n)) → SUC^#(n) (111)

1 > 1

SUC^#(NUMERAL(n)) → SUC^#(n) (109)

1 > 1

As there is no critical graph in the transitive closure, there are no infinite chains.
The 10^th component contains the pair
EVEN^#(NUMERAL(n)) → EVEN^#(n) (160)

1.1.10 Size-Change Termination

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

EVEN^#(NUMERAL(n)) → EVEN^#(n) (160)

1 > 1

As there is no critical graph in the transitive closure, there are no infinite chains.
The 11^th component contains the pair
ODD^#(NUMERAL(n)) → ODD^#(n) (161)

1.1.11 Size-Change Termination

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

ODD^#(NUMERAL(n)) → ODD^#(n) (161)

1 > 1

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

The 12^th component contains the pair

gt^#(BIT1(n),BIT1(m))	→	gt^#(n,m)	(190)
gt^#(BIT0(n),BIT1(m))	→	gt^#(n,m)	(189)
gt^#(BIT1(n),BIT0(m))	→	ge^#(n,m)	(188)
ge^#(BIT1(n),BIT1(m))	→	ge^#(n,m)	(184)
ge^#(BIT0(n),BIT1(m))	→	gt^#(n,m)	(183)
gt^#(BIT0(n),BIT0(m))	→	gt^#(n,m)	(187)
gt^#(NUMERAL(n),NUMERAL(m))	→	gt^#(n,m)	(185)
ge^#(BIT1(n),BIT0(m))	→	ge^#(n,m)	(182)
ge^#(BIT0(n),BIT0(m))	→	ge^#(n,m)	(181)
ge^#(NUMERAL(n),NUMERAL(m))	→	ge^#(n,m)	(179)

1.1.12 Size-Change Termination

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

gt^#(BIT1(n),BIT1(m))	→	gt^#(n,m)	(190)

2	>	2
1	>	1
gt^#(BIT0(n),BIT1(m))	→	gt^#(n,m)	(189)

2	>	2
1	>	1
gt^#(BIT1(n),BIT0(m))	→	ge^#(n,m)	(188)

2	>	2
1	>	1
ge^#(BIT1(n),BIT1(m))	→	ge^#(n,m)	(184)

2	>	2
1	>	1
ge^#(BIT0(n),BIT1(m))	→	gt^#(n,m)	(183)

2	>	2
1	>	1
gt^#(BIT0(n),BIT0(m))	→	gt^#(n,m)	(187)

2	>	2
1	>	1
gt^#(NUMERAL(n),NUMERAL(m))	→	gt^#(n,m)	(185)

2	>	2
1	>	1
ge^#(BIT1(n),BIT0(m))	→	ge^#(n,m)	(182)

2	>	2
1	>	1
ge^#(BIT0(n),BIT0(m))	→	ge^#(n,m)	(181)

2	>	2
1	>	1
ge^#(NUMERAL(n),NUMERAL(m))	→	ge^#(n,m)	(179)

2	>	2
1	>	1

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

The 13^th component contains the pair
ge^#(0,BIT0(n)) → ge^#(0,n) (180)

1.1.13 Size-Change Termination

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

ge^#(0,BIT0(n)) → ge^#(0,n) (180)

2 > 2

1 ≥ 1

As there is no critical graph in the transitive closure, there are no infinite chains.
The 14^th component contains the pair
gt^#(BIT0(n),0) → gt^#(n,0) (186)

1.1.14 Size-Change Termination

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

gt^#(BIT0(n),0) → gt^#(n,0) (186)

2 ≥ 2

1 > 1

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

The 15^th component contains the pair

minus^#(BIT1(m),BIT1(n))	→	minus^#(m,n)	(200)
minus^#(BIT1(m),BIT0(n))	→	minus^#(m,n)	(198)
minus^#(BIT0(m),BIT1(n))	→	minus^#(m,n)	(195)
minus^#(BIT0(m),BIT0(n))	→	minus^#(m,n)	(193)
minus^#(NUMERAL(m),NUMERAL(n))	→	minus^#(m,n)	(191)

1.1.15 Size-Change Termination

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

minus^#(BIT1(m),BIT1(n))	→	minus^#(m,n)	(200)

2	>	2
1	>	1
minus^#(BIT1(m),BIT0(n))	→	minus^#(m,n)	(198)

2	>	2
1	>	1
minus^#(BIT0(m),BIT1(n))	→	minus^#(m,n)	(195)

2	>	2
1	>	1
minus^#(BIT0(m),BIT0(n))	→	minus^#(m,n)	(193)

2	>	2
1	>	1
minus^#(NUMERAL(m),NUMERAL(n))	→	minus^#(m,n)	(191)

2	>	2
1	>	1

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

The 16^th component contains the pair

PRE^#(BIT0(n)) → PRE^#(n) (115)

PRE^#(NUMERAL(n)) → PRE^#(n) (113)

1.1.16 Size-Change Termination

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

PRE^#(BIT0(n)) → PRE^#(n) (115)

1 > 1

PRE^#(NUMERAL(n)) → PRE^#(n) (113)

1 > 1

As there is no critical graph in the transitive closure, there are no infinite chains.
The 17^th component contains the pair
eq^#(BIT0(n),0) → eq^#(n,0) (163)

1.1.17 Size-Change Termination

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

eq^#(BIT0(n),0) → eq^#(n,0) (163)

2 ≥ 2

1 > 1

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

The 18^th component contains the pair

le^#(BIT1(m),BIT1(n))	→	le^#(m,n)	(172)
le^#(BIT1(m),BIT0(n))	→	lt^#(m,n)	(171)
lt^#(BIT1(m),BIT1(n))	→	lt^#(m,n)	(178)
lt^#(BIT1(m),BIT0(n))	→	lt^#(m,n)	(177)
lt^#(BIT0(m),BIT1(n))	→	le^#(m,n)	(176)
le^#(BIT0(m),BIT1(n))	→	le^#(m,n)	(170)
le^#(BIT0(m),BIT0(n))	→	le^#(m,n)	(169)
le^#(NUMERAL(m),NUMERAL(n))	→	le^#(m,n)	(167)
lt^#(BIT0(m),BIT0(n))	→	lt^#(m,n)	(175)
lt^#(NUMERAL(m),NUMERAL(n))	→	lt^#(m,n)	(173)

1.1.18 Size-Change Termination

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

le^#(BIT1(m),BIT1(n))	→	le^#(m,n)	(172)

2	>	2
1	>	1
le^#(BIT1(m),BIT0(n))	→	lt^#(m,n)	(171)

2	>	2
1	>	1
lt^#(BIT1(m),BIT1(n))	→	lt^#(m,n)	(178)

2	>	2
1	>	1
lt^#(BIT1(m),BIT0(n))	→	lt^#(m,n)	(177)

2	>	2
1	>	1
lt^#(BIT0(m),BIT1(n))	→	le^#(m,n)	(176)

2	>	2
1	>	1
le^#(BIT0(m),BIT1(n))	→	le^#(m,n)	(170)

2	>	2
1	>	1
le^#(BIT0(m),BIT0(n))	→	le^#(m,n)	(169)

2	>	2
1	>	1
le^#(NUMERAL(m),NUMERAL(n))	→	le^#(m,n)	(167)

2	>	2
1	>	1
lt^#(BIT0(m),BIT0(n))	→	lt^#(m,n)	(175)

2	>	2
1	>	1
lt^#(NUMERAL(m),NUMERAL(n))	→	lt^#(m,n)	(173)

2	>	2
1	>	1

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

The 19^th component contains the pair
lt^#(0,BIT0(n)) → lt^#(0,n) (174)

1.1.19 Size-Change Termination

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

lt^#(0,BIT0(n)) → lt^#(0,n) (174)

2 > 2

1 ≥ 1

As there is no critical graph in the transitive closure, there are no infinite chains.
The 20^th component contains the pair
le^#(BIT0(n),0) → le^#(n,0) (168)

1.1.20 Size-Change Termination

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

le^#(BIT0(n),0) → le^#(n,0) (168)

2 ≥ 2

1 > 1

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

Certification Problem

Input (TPDB TRS_Standard/Kaliszyk_19/arith)

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 Size-Change Termination

1.1.11 Size-Change Termination

1.1.12 Size-Change Termination

1.1.13 Size-Change Termination

1.1.14 Size-Change Termination

1.1.15 Size-Change Termination

1.1.16 Size-Change Termination

1.1.17 Size-Change Termination

1.1.18 Size-Change Termination

1.1.19 Size-Change Termination

1.1.20 Size-Change Termination