Certification Problem

Input (TPDB TRS_Equational/Mixed_AC/sequent_modulo)

The rewrite relation of the following equational TRS is considered.

substt(ef(x),y)	→	ef(substt(x,y))	(1)
substf(Pe(x),y)	→	Pe(substt(x,y))	(2)
substf(neg(f),s)	→	neg(substf(f,s))	(3)
substf(and(f,g),s)	→	and(substf(f,s),substf(g,s))	(4)
substf(or(f,g),s)	→	or(substf(f,s),substf(g,s))	(5)
substf(imp(f,g),s)	→	imp(substf(f,s),substf(g,s))	(6)
substf(forall(f),s)	→	forall(substf(f,.(1,ron(s,shift))))	(7)
substf(exists(f),s)	→	exists(substf(f,.(1,ron(s,shift))))	(8)
substt(x,id)	→	x	(9)
substf(f,id)	→	f	(10)
substt(substt(x,s),t)	→	substt(x,ron(s,t))	(11)
substf(substf(f,s),t)	→	substf(f,ron(s,t))	(12)
substt(1,.(x,s))	→	x	(13)
ron(id,s)	→	s	(14)
ron(shift,.(x,s))	→	s	(15)
ron(ron(s,t),u)	→	ron(s,ron(t,u))	(16)
ron(.(x,s),t)	→	.(substt(x,t),ron(s,t))	(17)
ron(s,id)	→	s	(18)
.(1,shift)	→	id	(19)
.(substt(1,s),ron(shift,s))	→	s	(20)
virg(emptyfset,a)	→	a	(21)
virg(a,a)	→	a	(22)
*(emptysset,a)	→	a	(23)
*(a,a)	→	a	(24)
neg(neg(f))	→	f	(25)
and(f,f)	→	f	(26)
or(f,f)	→	f	(27)
imp(f,g)	→	or(neg(f),g)	(28)
exists(f)	→	neg(forall(neg(f)))	(29)
sequent(virg(convf(neg(f)),a),b)	→	sequent(a,virg(convf(f),b))	(30)
sequent(convf(neg(f)),b)	→	sequent(emptyfset,virg(convf(f),b))	(31)
sequent(a,virg(convf(neg(f)),b))	→	sequent(virg(convf(f),a),b)	(32)
sequent(a,convf(neg(f)))	→	sequent(virg(convf(f),a),emptyfset)	(33)
sequent(virg(convf(and(f,g)),a),b)	→	sequent(virg(convf(g),virg(convf(f),a)),b)	(34)
sequent(convf(and(f,g)),b)	→	sequent(virg(convf(f),convf(g)),b)	(35)
sequent(a,virg(convf(or(f,g)),b))	→	sequent(a,virg(virg(convf(f),convf(g)),b))	(36)
sequent(a,convf(or(f,g)))	→	sequent(a,virg(convf(f),convf(g)))	(37)
convs(sequent(a,virg(convf(and(f,g)),b)))	→	*(convs(sequent(a,virg(convf(f),b))),convs(sequent(a,virg(convf(g),b))))	(38)
convs(sequent(a,convf(and(f,g))))	→	*(convs(sequent(a,convf(f))),convs(sequent(a,convf(g))))	(39)
convs(sequent(virg(convf(or(f,g)),a),b))	→	*(convs(sequent(virg(convf(f),a),b)),convs(sequent(virg(convf(g),a),b)))	(40)
convs(sequent(convf(or(f,g)),b))	→	*(convs(sequent(convf(f),b)),convs(sequent(convf(g),b)))	(41)
convs(sequent(virg(convf(f),a),virg(convf(f),b)))	→	emptysset	(42)
convs(sequent(virg(convf(f),a),convf(f)))	→	emptysset	(43)
convs(sequent(convf(f),virg(convf(f),b)))	→	emptysset	(44)
convs(sequent(convf(f),convf(f)))	→	emptysset	(45)
*(convs(sequent(virg(f,a),virg(g,b))),convs(sequent(a,b)))	→	convs(sequent(a,b))	(46)
*(convs(sequent(virg(f,a),b)),convs(sequent(a,b)))	→	convs(sequent(a,b))	(47)
*(convs(sequent(a,virg(f,b))),convs(sequent(a,b)))	→	convs(sequent(a,b))	(48)
*(convs(sequent(virg(f,a),b)),convs(sequent(a,emptyfset)))	→	convs(sequent(a,emptyfset))	(49)
*(convs(sequent(emptyfset,b)),convs(sequent(a,virg(f,b))))	→	convs(sequent(emptyfset,b))	(50)
*(convs(sequent(emptyfset,b)),convs(sequent(a,b)))	→	convs(sequent(emptyfset,b))	(51)
*(convs(sequent(a,emptyfset)),convs(sequent(a,b)))	→	convs(sequent(a,emptyfset))	(52)
*(convs(sequent(emptyfset,emptyfset)),convs(sequent(a,b)))	→	convs(sequent(emptyfset,emptyfset))	(53)

Associative symbols: *, virg

Commutative symbols: *, virg

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 AC Dependency Pair Transformation

The following set of (strict) dependency pairs is constructed for the TRS.

substt^#(ef(x),y)	→	substt^#(x,y)	(64)
substf^#(Pe(x),y)	→	substt^#(x,y)	(65)
substf^#(neg(f),s)	→	neg^#(substf(f,s))	(66)
substf^#(neg(f),s)	→	substf^#(f,s)	(67)
substf^#(and(f,g),s)	→	and^#(substf(f,s),substf(g,s))	(68)
substf^#(and(f,g),s)	→	substf^#(f,s)	(69)
substf^#(and(f,g),s)	→	substf^#(g,s)	(70)
substf^#(or(f,g),s)	→	or^#(substf(f,s),substf(g,s))	(71)
substf^#(or(f,g),s)	→	substf^#(f,s)	(72)
substf^#(or(f,g),s)	→	substf^#(g,s)	(73)
substf^#(imp(f,g),s)	→	imp^#(substf(f,s),substf(g,s))	(74)
substf^#(imp(f,g),s)	→	substf^#(f,s)	(75)
substf^#(imp(f,g),s)	→	substf^#(g,s)	(76)
substf^#(forall(f),s)	→	substf^#(f,.(1,ron(s,shift)))	(77)
substf^#(forall(f),s)	→	.^#(1,ron(s,shift))	(78)
substf^#(forall(f),s)	→	ron^#(s,shift)	(79)
substf^#(exists(f),s)	→	exists^#(substf(f,.(1,ron(s,shift))))	(80)
substf^#(exists(f),s)	→	substf^#(f,.(1,ron(s,shift)))	(81)
substf^#(exists(f),s)	→	.^#(1,ron(s,shift))	(82)
substf^#(exists(f),s)	→	ron^#(s,shift)	(83)
substt^#(substt(x,s),t)	→	substt^#(x,ron(s,t))	(84)
substt^#(substt(x,s),t)	→	ron^#(s,t)	(85)
substf^#(substf(f,s),t)	→	substf^#(f,ron(s,t))	(86)
substf^#(substf(f,s),t)	→	ron^#(s,t)	(87)
ron^#(ron(s,t),u)	→	ron^#(s,ron(t,u))	(88)
ron^#(ron(s,t),u)	→	ron^#(t,u)	(89)
ron^#(.(x,s),t)	→	.^#(substt(x,t),ron(s,t))	(90)
ron^#(.(x,s),t)	→	substt^#(x,t)	(91)
ron^#(.(x,s),t)	→	ron^#(s,t)	(92)
imp^#(f,g)	→	or^#(neg(f),g)	(93)
imp^#(f,g)	→	neg^#(f)	(94)
exists^#(f)	→	neg^#(forall(neg(f)))	(95)
exists^#(f)	→	neg^#(f)	(96)
sequent^#(virg(convf(neg(f)),a),b)	→	sequent^#(a,virg(convf(f),b))	(97)
sequent^#(virg(convf(neg(f)),a),b)	→	virg^#(convf(f),b)	(98)
sequent^#(convf(neg(f)),b)	→	sequent^#(emptyfset,virg(convf(f),b))	(99)
sequent^#(convf(neg(f)),b)	→	virg^#(convf(f),b)	(100)
sequent^#(a,virg(convf(neg(f)),b))	→	sequent^#(virg(convf(f),a),b)	(101)
sequent^#(a,virg(convf(neg(f)),b))	→	virg^#(convf(f),a)	(102)
sequent^#(a,convf(neg(f)))	→	sequent^#(virg(convf(f),a),emptyfset)	(103)
sequent^#(a,convf(neg(f)))	→	virg^#(convf(f),a)	(104)
sequent^#(virg(convf(and(f,g)),a),b)	→	sequent^#(virg(convf(g),virg(convf(f),a)),b)	(105)
sequent^#(virg(convf(and(f,g)),a),b)	→	virg^#(convf(g),virg(convf(f),a))	(106)
sequent^#(virg(convf(and(f,g)),a),b)	→	virg^#(convf(f),a)	(107)
sequent^#(convf(and(f,g)),b)	→	sequent^#(virg(convf(f),convf(g)),b)	(108)
sequent^#(convf(and(f,g)),b)	→	virg^#(convf(f),convf(g))	(109)
sequent^#(a,virg(convf(or(f,g)),b))	→	sequent^#(a,virg(virg(convf(f),convf(g)),b))	(110)
sequent^#(a,virg(convf(or(f,g)),b))	→	virg^#(virg(convf(f),convf(g)),b)	(111)
sequent^#(a,virg(convf(or(f,g)),b))	→	virg^#(convf(f),convf(g))	(112)
sequent^#(a,convf(or(f,g)))	→	sequent^#(a,virg(convf(f),convf(g)))	(113)
sequent^#(a,convf(or(f,g)))	→	virg^#(convf(f),convf(g))	(114)
convs^#(sequent(a,virg(convf(and(f,g)),b)))	→	*^#(convs(sequent(a,virg(convf(f),b))),convs(sequent(a,virg(convf(g),b))))	(115)
convs^#(sequent(a,virg(convf(and(f,g)),b)))	→	convs^#(sequent(a,virg(convf(f),b)))	(116)
convs^#(sequent(a,virg(convf(and(f,g)),b)))	→	sequent^#(a,virg(convf(f),b))	(117)
convs^#(sequent(a,virg(convf(and(f,g)),b)))	→	virg^#(convf(f),b)	(118)
convs^#(sequent(a,virg(convf(and(f,g)),b)))	→	convs^#(sequent(a,virg(convf(g),b)))	(119)
convs^#(sequent(a,virg(convf(and(f,g)),b)))	→	sequent^#(a,virg(convf(g),b))	(120)
convs^#(sequent(a,virg(convf(and(f,g)),b)))	→	virg^#(convf(g),b)	(121)
convs^#(sequent(a,convf(and(f,g))))	→	*^#(convs(sequent(a,convf(f))),convs(sequent(a,convf(g))))	(122)
convs^#(sequent(a,convf(and(f,g))))	→	convs^#(sequent(a,convf(f)))	(123)
convs^#(sequent(a,convf(and(f,g))))	→	sequent^#(a,convf(f))	(124)
convs^#(sequent(a,convf(and(f,g))))	→	convs^#(sequent(a,convf(g)))	(125)
convs^#(sequent(a,convf(and(f,g))))	→	sequent^#(a,convf(g))	(126)
convs^#(sequent(virg(convf(or(f,g)),a),b))	→	*^#(convs(sequent(virg(convf(f),a),b)),convs(sequent(virg(convf(g),a),b)))	(127)
convs^#(sequent(virg(convf(or(f,g)),a),b))	→	convs^#(sequent(virg(convf(f),a),b))	(128)
convs^#(sequent(virg(convf(or(f,g)),a),b))	→	sequent^#(virg(convf(f),a),b)	(129)
convs^#(sequent(virg(convf(or(f,g)),a),b))	→	virg^#(convf(f),a)	(130)
convs^#(sequent(virg(convf(or(f,g)),a),b))	→	convs^#(sequent(virg(convf(g),a),b))	(131)
convs^#(sequent(virg(convf(or(f,g)),a),b))	→	sequent^#(virg(convf(g),a),b)	(132)
convs^#(sequent(virg(convf(or(f,g)),a),b))	→	virg^#(convf(g),a)	(133)
convs^#(sequent(convf(or(f,g)),b))	→	*^#(convs(sequent(convf(f),b)),convs(sequent(convf(g),b)))	(134)
convs^#(sequent(convf(or(f,g)),b))	→	convs^#(sequent(convf(f),b))	(135)
convs^#(sequent(convf(or(f,g)),b))	→	sequent^#(convf(f),b)	(136)
convs^#(sequent(convf(or(f,g)),b))	→	convs^#(sequent(convf(g),b))	(137)
convs^#(sequent(convf(or(f,g)),b))	→	sequent^#(convf(g),b)	(138)
^#((emptysset,a),ext)	→	*^#(a,ext)	(139)
^#((a,a),ext)	→	*^#(a,ext)	(140)
^#((convs(sequent(virg(f,a),virg(g,b))),convs(sequent(a,b))),ext)	→	*^#(convs(sequent(a,b)),ext)	(141)
^#((convs(sequent(virg(f,a),b)),convs(sequent(a,b))),ext)	→	*^#(convs(sequent(a,b)),ext)	(142)
^#((convs(sequent(a,virg(f,b))),convs(sequent(a,b))),ext)	→	*^#(convs(sequent(a,b)),ext)	(143)
^#((convs(sequent(virg(f,a),b)),convs(sequent(a,emptyfset))),ext)	→	*^#(convs(sequent(a,emptyfset)),ext)	(144)
^#((convs(sequent(emptyfset,b)),convs(sequent(a,virg(f,b)))),ext)	→	*^#(convs(sequent(emptyfset,b)),ext)	(145)
^#((convs(sequent(emptyfset,b)),convs(sequent(a,b))),ext)	→	*^#(convs(sequent(emptyfset,b)),ext)	(146)
^#((convs(sequent(a,emptyfset)),convs(sequent(a,b))),ext)	→	*^#(convs(sequent(a,emptyfset)),ext)	(147)
^#((convs(sequent(emptyfset,emptyfset)),convs(sequent(a,b))),ext)	→	*^#(convs(sequent(emptyfset,emptyfset)),ext)	(148)
virg^#(virg(emptyfset,a),ext)	→	virg^#(a,ext)	(149)
virg^#(virg(a,a),ext)	→	virg^#(a,ext)	(150)

The extended rules of the TRS

((emptysset,a),ext)	→	*(a,ext)	(151)
((a,a),ext)	→	*(a,ext)	(152)
((convs(sequent(virg(f,a),virg(g,b))),convs(sequent(a,b))),ext)	→	*(convs(sequent(a,b)),ext)	(153)
((convs(sequent(virg(f,a),b)),convs(sequent(a,b))),ext)	→	*(convs(sequent(a,b)),ext)	(154)
((convs(sequent(a,virg(f,b))),convs(sequent(a,b))),ext)	→	*(convs(sequent(a,b)),ext)	(155)
((convs(sequent(virg(f,a),b)),convs(sequent(a,emptyfset))),ext)	→	*(convs(sequent(a,emptyfset)),ext)	(156)
((convs(sequent(emptyfset,b)),convs(sequent(a,virg(f,b)))),ext)	→	*(convs(sequent(emptyfset,b)),ext)	(157)
((convs(sequent(emptyfset,b)),convs(sequent(a,b))),ext)	→	*(convs(sequent(emptyfset,b)),ext)	(158)
((convs(sequent(a,emptyfset)),convs(sequent(a,b))),ext)	→	*(convs(sequent(a,emptyfset)),ext)	(159)
((convs(sequent(emptyfset,emptyfset)),convs(sequent(a,b))),ext)	→	*(convs(sequent(emptyfset,emptyfset)),ext)	(160)
virg(virg(emptyfset,a),ext)	→	virg(a,ext)	(161)
virg(virg(a,a),ext)	→	virg(a,ext)	(162)

give rise to even more dependency pairs (by sharping the root symbols of each rule). Finiteness for all DPs in combination with the equational DPs is proven as follows.

1.1 Dependency Graph Processor

The dependency pairs are split into 6 components.

The 1^st component contains the pair

substf^#(and(f,g),s)	→	substf^#(f,s)	(69)
substf^#(neg(f),s)	→	substf^#(f,s)	(67)
substf^#(and(f,g),s)	→	substf^#(g,s)	(70)
substf^#(or(f,g),s)	→	substf^#(f,s)	(72)
substf^#(or(f,g),s)	→	substf^#(g,s)	(73)
substf^#(imp(f,g),s)	→	substf^#(f,s)	(75)
substf^#(imp(f,g),s)	→	substf^#(g,s)	(76)
substf^#(forall(f),s)	→	substf^#(f,.(1,ron(s,shift)))	(77)
substf^#(exists(f),s)	→	substf^#(f,.(1,ron(s,shift)))	(81)
substf^#(substf(f,s),t)	→	substf^#(f,ron(s,t))	(86)

1.1.1 AC Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[substf^#(x₁, x₂)]	=	1 · x₁
[neg(x₁)]	=	3 + 3 · x₁
[or(x₁, x₂)]	=	3 + 3 · x₁ + 3 · x₂
[and(x₁, x₂)]	=	3 + 3 · x₁ + 3 · x₂
[imp(x₁, x₂)]	=	3 + 3 · x₁ + 3 · x₂
[forall(x₁)]	=	3 + 3 · x₁
[.(x₁, x₂)]	=	0
[1]	=	0
[ron(x₁, x₂)]	=	0
[shift]	=	0
[exists(x₁)]	=	3 · x₁
[substf(x₁, x₂)]	=	1 + 3 · x₁
[id]	=	3
[substt(x₁, x₂)]	=	0
[ef(x₁)]	=	0

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pairs

substf^#(neg(f),s)	→	substf^#(f,s)	(67)
substf^#(or(f,g),s)	→	substf^#(g,s)	(73)
substf^#(and(f,g),s)	→	substf^#(f,s)	(69)
substf^#(imp(f,g),s)	→	substf^#(g,s)	(76)
substf^#(or(f,g),s)	→	substf^#(f,s)	(72)
substf^#(and(f,g),s)	→	substf^#(g,s)	(70)
substf^#(imp(f,g),s)	→	substf^#(f,s)	(75)
substf^#(forall(f),s)	→	substf^#(f,.(1,ron(s,shift)))	(77)
substf^#(substf(f,s),t)	→	substf^#(f,ron(s,t))	(86)

could be deleted.

1.1.1.1 AC Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[substf^#(x₁, x₂)]	=	2 · x₁
[exists(x₁)]	=	2 + 3 · x₁
[.(x₁, x₂)]	=	0
[1]	=	0
[ron(x₁, x₂)]	=	0
[shift]	=	0
[id]	=	3
[substt(x₁, x₂)]	=	0
[ef(x₁)]	=	0

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pair

substf^#(exists(f),s)

→

substf^#(f,.(1,ron(s,shift)))

(81)

could be deleted.

1.1.1.1.1 AC Dependency Pair Problem is trivial

There are no strict pairs and rules remaining, or there are no DPs remaining. Therefore, finiteness is trivially satisfied.

The 2^nd component contains the pair

substt^#(substt(x,s),t)	→	substt^#(x,ron(s,t))	(84)
substt^#(ef(x),y)	→	substt^#(x,y)	(64)
substt^#(substt(x,s),t)	→	ron^#(s,t)	(85)
ron^#(ron(s,t),u)	→	ron^#(s,ron(t,u))	(88)
ron^#(ron(s,t),u)	→	ron^#(t,u)	(89)
ron^#(.(x,s),t)	→	substt^#(x,t)	(91)
ron^#(.(x,s),t)	→	ron^#(s,t)	(92)

1.1.2 AC Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[ron^#(x₁, x₂)]	=	3 + 1 · x₁
[.(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[substt^#(x₁, x₂)]	=	3 + 1 · x₁
[ron(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[ef(x₁)]	=	2 · x₁
[substt(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[1]	=	3
[shift]	=	3
[id]	=	3

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pairs

ron^#(.(x,s),t)	→	substt^#(x,t)	(91)
ron^#(ron(s,t),u)	→	ron^#(t,u)	(89)
ron^#(ron(s,t),u)	→	ron^#(s,ron(t,u))	(88)
substt^#(substt(x,s),t)	→	ron^#(s,t)	(85)
ron^#(.(x,s),t)	→	ron^#(s,t)	(92)
substt^#(substt(x,s),t)	→	substt^#(x,ron(s,t))	(84)

could be deleted.

1.1.2.1 AC Monotonic Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[substt^#(x₁, x₂)]	=	3 · x₁ + 1 · x₂
[ef(x₁)]	=	3 · x₁

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pair

substt^#(ef(x),y)

→

substt^#(x,y)

(64)

and the rules

substt(ef(x),y)	→	ef(substt(x,y))	(1)
substf(Pe(x),y)	→	Pe(substt(x,y))	(2)
substf(neg(f),s)	→	neg(substf(f,s))	(3)
substf(and(f,g),s)	→	and(substf(f,s),substf(g,s))	(4)
substf(or(f,g),s)	→	or(substf(f,s),substf(g,s))	(5)
substf(imp(f,g),s)	→	imp(substf(f,s),substf(g,s))	(6)
substf(forall(f),s)	→	forall(substf(f,.(1,ron(s,shift))))	(7)
substf(exists(f),s)	→	exists(substf(f,.(1,ron(s,shift))))	(8)
substt(x,id)	→	x	(9)
substf(f,id)	→	f	(10)
substt(substt(x,s),t)	→	substt(x,ron(s,t))	(11)
substf(substf(f,s),t)	→	substf(f,ron(s,t))	(12)
substt(1,.(x,s))	→	x	(13)
ron(id,s)	→	s	(14)
ron(shift,.(x,s))	→	s	(15)
ron(ron(s,t),u)	→	ron(s,ron(t,u))	(16)
ron(.(x,s),t)	→	.(substt(x,t),ron(s,t))	(17)
ron(s,id)	→	s	(18)
.(1,shift)	→	id	(19)
.(substt(1,s),ron(shift,s))	→	s	(20)
virg(emptyfset,a)	→	a	(21)
virg(a,a)	→	a	(22)
*(emptysset,a)	→	a	(23)
*(a,a)	→	a	(24)
neg(neg(f))	→	f	(25)
and(f,f)	→	f	(26)
or(f,f)	→	f	(27)
imp(f,g)	→	or(neg(f),g)	(28)
exists(f)	→	neg(forall(neg(f)))	(29)
sequent(virg(convf(neg(f)),a),b)	→	sequent(a,virg(convf(f),b))	(30)
sequent(convf(neg(f)),b)	→	sequent(emptyfset,virg(convf(f),b))	(31)
sequent(a,virg(convf(neg(f)),b))	→	sequent(virg(convf(f),a),b)	(32)
sequent(a,convf(neg(f)))	→	sequent(virg(convf(f),a),emptyfset)	(33)
sequent(virg(convf(and(f,g)),a),b)	→	sequent(virg(convf(g),virg(convf(f),a)),b)	(34)
sequent(convf(and(f,g)),b)	→	sequent(virg(convf(f),convf(g)),b)	(35)
sequent(a,virg(convf(or(f,g)),b))	→	sequent(a,virg(virg(convf(f),convf(g)),b))	(36)
sequent(a,convf(or(f,g)))	→	sequent(a,virg(convf(f),convf(g)))	(37)
convs(sequent(a,virg(convf(and(f,g)),b)))	→	*(convs(sequent(a,virg(convf(f),b))),convs(sequent(a,virg(convf(g),b))))	(38)
convs(sequent(a,convf(and(f,g))))	→	*(convs(sequent(a,convf(f))),convs(sequent(a,convf(g))))	(39)
convs(sequent(virg(convf(or(f,g)),a),b))	→	*(convs(sequent(virg(convf(f),a),b)),convs(sequent(virg(convf(g),a),b)))	(40)
convs(sequent(convf(or(f,g)),b))	→	*(convs(sequent(convf(f),b)),convs(sequent(convf(g),b)))	(41)
convs(sequent(virg(convf(f),a),virg(convf(f),b)))	→	emptysset	(42)
convs(sequent(virg(convf(f),a),convf(f)))	→	emptysset	(43)
convs(sequent(convf(f),virg(convf(f),b)))	→	emptysset	(44)
convs(sequent(convf(f),convf(f)))	→	emptysset	(45)
*(convs(sequent(virg(f,a),virg(g,b))),convs(sequent(a,b)))	→	convs(sequent(a,b))	(46)
*(convs(sequent(virg(f,a),b)),convs(sequent(a,b)))	→	convs(sequent(a,b))	(47)
*(convs(sequent(a,virg(f,b))),convs(sequent(a,b)))	→	convs(sequent(a,b))	(48)
*(convs(sequent(virg(f,a),b)),convs(sequent(a,emptyfset)))	→	convs(sequent(a,emptyfset))	(49)
*(convs(sequent(emptyfset,b)),convs(sequent(a,virg(f,b))))	→	convs(sequent(emptyfset,b))	(50)
*(convs(sequent(emptyfset,b)),convs(sequent(a,b)))	→	convs(sequent(emptyfset,b))	(51)
*(convs(sequent(a,emptyfset)),convs(sequent(a,b)))	→	convs(sequent(a,emptyfset))	(52)
*(convs(sequent(emptyfset,emptyfset)),convs(sequent(a,b)))	→	convs(sequent(emptyfset,emptyfset))	(53)
((emptysset,a),ext)	→	*(a,ext)	(151)
((a,a),ext)	→	*(a,ext)	(152)
((convs(sequent(virg(f,a),virg(g,b))),convs(sequent(a,b))),ext)	→	*(convs(sequent(a,b)),ext)	(153)
((convs(sequent(virg(f,a),b)),convs(sequent(a,b))),ext)	→	*(convs(sequent(a,b)),ext)	(154)
((convs(sequent(a,virg(f,b))),convs(sequent(a,b))),ext)	→	*(convs(sequent(a,b)),ext)	(155)
((convs(sequent(virg(f,a),b)),convs(sequent(a,emptyfset))),ext)	→	*(convs(sequent(a,emptyfset)),ext)	(156)
((convs(sequent(emptyfset,b)),convs(sequent(a,virg(f,b)))),ext)	→	*(convs(sequent(emptyfset,b)),ext)	(157)
((convs(sequent(emptyfset,b)),convs(sequent(a,b))),ext)	→	*(convs(sequent(emptyfset,b)),ext)	(158)
((convs(sequent(a,emptyfset)),convs(sequent(a,b))),ext)	→	*(convs(sequent(a,emptyfset)),ext)	(159)
((convs(sequent(emptyfset,emptyfset)),convs(sequent(a,b))),ext)	→	*(convs(sequent(emptyfset,emptyfset)),ext)	(160)
virg(virg(emptyfset,a),ext)	→	virg(a,ext)	(161)
virg(virg(a,a),ext)	→	virg(a,ext)	(162)

could be deleted.

1.1.2.1.1 AC Dependency Pair Problem is trivial

There are no strict pairs and rules remaining, or there are no DPs remaining. Therefore, finiteness is trivially satisfied.

The 3^rd component contains the pair

convs^#(sequent(a,virg(convf(and(f,g)),b)))	→	convs^#(sequent(a,virg(convf(g),b)))	(119)
convs^#(sequent(a,virg(convf(and(f,g)),b)))	→	convs^#(sequent(a,virg(convf(f),b)))	(116)
convs^#(sequent(a,convf(and(f,g))))	→	convs^#(sequent(a,convf(f)))	(123)
convs^#(sequent(a,convf(and(f,g))))	→	convs^#(sequent(a,convf(g)))	(125)
convs^#(sequent(virg(convf(or(f,g)),a),b))	→	convs^#(sequent(virg(convf(f),a),b))	(128)
convs^#(sequent(virg(convf(or(f,g)),a),b))	→	convs^#(sequent(virg(convf(g),a),b))	(131)
convs^#(sequent(convf(or(f,g)),b))	→	convs^#(sequent(convf(f),b))	(135)
convs^#(sequent(convf(or(f,g)),b))	→	convs^#(sequent(convf(g),b))	(137)

1.1.3 AC Monotonic Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[virg(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[sequent(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[convf(x₁)]	=	2 + 3 · x₁
[neg(x₁)]	=	2 · x₁
[emptyfset]	=	0
[and(x₁, x₂)]	=	3 + 2 · x₁ + 1 · x₂
[or(x₁, x₂)]	=	3 + 2 · x₁ + 2 · x₂
[convs^#(x₁)]	=	1 · x₁

together with the usable rules

virg(virg(a,a),ext)	→	virg(a,ext)	(162)
virg(a,a)	→	a	(22)
sequent(convf(neg(f)),b)	→	sequent(emptyfset,virg(convf(f),b))	(31)
sequent(a,virg(convf(neg(f)),b))	→	sequent(virg(convf(f),a),b)	(32)
sequent(a,convf(neg(f)))	→	sequent(virg(convf(f),a),emptyfset)	(33)
sequent(convf(and(f,g)),b)	→	sequent(virg(convf(f),convf(g)),b)	(35)
sequent(virg(convf(neg(f)),a),b)	→	sequent(a,virg(convf(f),b))	(30)
sequent(virg(convf(and(f,g)),a),b)	→	sequent(virg(convf(g),virg(convf(f),a)),b)	(34)
sequent(a,virg(convf(or(f,g)),b))	→	sequent(a,virg(virg(convf(f),convf(g)),b))	(36)
sequent(a,convf(or(f,g)))	→	sequent(a,virg(convf(f),convf(g)))	(37)
virg(emptyfset,a)	→	a	(21)
virg(virg(emptyfset,a),ext)	→	virg(a,ext)	(161)
virg(x,y)	→	virg(y,x)	(55)
virg(virg(x,y),z)	→	virg(x,virg(y,z))	(57)

(w.r.t. the implicit argument filter of the reduction pair), the pairs

convs^#(sequent(a,convf(and(f,g))))	→	convs^#(sequent(a,convf(g)))	(125)
convs^#(sequent(a,virg(convf(and(f,g)),b)))	→	convs^#(sequent(a,virg(convf(g),b)))	(119)
convs^#(sequent(convf(or(f,g)),b))	→	convs^#(sequent(convf(f),b))	(135)
convs^#(sequent(a,virg(convf(and(f,g)),b)))	→	convs^#(sequent(a,virg(convf(f),b)))	(116)
convs^#(sequent(virg(convf(or(f,g)),a),b))	→	convs^#(sequent(virg(convf(g),a),b))	(131)
convs^#(sequent(virg(convf(or(f,g)),a),b))	→	convs^#(sequent(virg(convf(f),a),b))	(128)
convs^#(sequent(convf(or(f,g)),b))	→	convs^#(sequent(convf(g),b))	(137)
convs^#(sequent(a,convf(and(f,g))))	→	convs^#(sequent(a,convf(f)))	(123)

and the rules

substt(ef(x),y)	→	ef(substt(x,y))	(1)
substf(Pe(x),y)	→	Pe(substt(x,y))	(2)
substf(neg(f),s)	→	neg(substf(f,s))	(3)
substf(and(f,g),s)	→	and(substf(f,s),substf(g,s))	(4)
substf(or(f,g),s)	→	or(substf(f,s),substf(g,s))	(5)
substf(imp(f,g),s)	→	imp(substf(f,s),substf(g,s))	(6)
substf(forall(f),s)	→	forall(substf(f,.(1,ron(s,shift))))	(7)
substf(exists(f),s)	→	exists(substf(f,.(1,ron(s,shift))))	(8)
substt(x,id)	→	x	(9)
substf(f,id)	→	f	(10)
substt(substt(x,s),t)	→	substt(x,ron(s,t))	(11)
substf(substf(f,s),t)	→	substf(f,ron(s,t))	(12)
substt(1,.(x,s))	→	x	(13)
ron(id,s)	→	s	(14)
ron(shift,.(x,s))	→	s	(15)
ron(ron(s,t),u)	→	ron(s,ron(t,u))	(16)
ron(.(x,s),t)	→	.(substt(x,t),ron(s,t))	(17)
ron(s,id)	→	s	(18)
.(1,shift)	→	id	(19)
.(substt(1,s),ron(shift,s))	→	s	(20)
*(emptysset,a)	→	a	(23)
*(a,a)	→	a	(24)
neg(neg(f))	→	f	(25)
and(f,f)	→	f	(26)
or(f,f)	→	f	(27)
imp(f,g)	→	or(neg(f),g)	(28)
exists(f)	→	neg(forall(neg(f)))	(29)
sequent(virg(convf(neg(f)),a),b)	→	sequent(a,virg(convf(f),b))	(30)
sequent(convf(neg(f)),b)	→	sequent(emptyfset,virg(convf(f),b))	(31)
sequent(a,virg(convf(neg(f)),b))	→	sequent(virg(convf(f),a),b)	(32)
sequent(a,convf(neg(f)))	→	sequent(virg(convf(f),a),emptyfset)	(33)
sequent(virg(convf(and(f,g)),a),b)	→	sequent(virg(convf(g),virg(convf(f),a)),b)	(34)
sequent(convf(and(f,g)),b)	→	sequent(virg(convf(f),convf(g)),b)	(35)
sequent(a,virg(convf(or(f,g)),b))	→	sequent(a,virg(virg(convf(f),convf(g)),b))	(36)
sequent(a,convf(or(f,g)))	→	sequent(a,virg(convf(f),convf(g)))	(37)
convs(sequent(a,virg(convf(and(f,g)),b)))	→	*(convs(sequent(a,virg(convf(f),b))),convs(sequent(a,virg(convf(g),b))))	(38)
convs(sequent(a,convf(and(f,g))))	→	*(convs(sequent(a,convf(f))),convs(sequent(a,convf(g))))	(39)
convs(sequent(virg(convf(or(f,g)),a),b))	→	*(convs(sequent(virg(convf(f),a),b)),convs(sequent(virg(convf(g),a),b)))	(40)
convs(sequent(convf(or(f,g)),b))	→	*(convs(sequent(convf(f),b)),convs(sequent(convf(g),b)))	(41)
convs(sequent(virg(convf(f),a),virg(convf(f),b)))	→	emptysset	(42)
convs(sequent(virg(convf(f),a),convf(f)))	→	emptysset	(43)
convs(sequent(convf(f),virg(convf(f),b)))	→	emptysset	(44)
convs(sequent(convf(f),convf(f)))	→	emptysset	(45)
*(convs(sequent(virg(f,a),virg(g,b))),convs(sequent(a,b)))	→	convs(sequent(a,b))	(46)
*(convs(sequent(virg(f,a),b)),convs(sequent(a,b)))	→	convs(sequent(a,b))	(47)
*(convs(sequent(a,virg(f,b))),convs(sequent(a,b)))	→	convs(sequent(a,b))	(48)
*(convs(sequent(virg(f,a),b)),convs(sequent(a,emptyfset)))	→	convs(sequent(a,emptyfset))	(49)
*(convs(sequent(emptyfset,b)),convs(sequent(a,virg(f,b))))	→	convs(sequent(emptyfset,b))	(50)
*(convs(sequent(emptyfset,b)),convs(sequent(a,b)))	→	convs(sequent(emptyfset,b))	(51)
*(convs(sequent(a,emptyfset)),convs(sequent(a,b)))	→	convs(sequent(a,emptyfset))	(52)
*(convs(sequent(emptyfset,emptyfset)),convs(sequent(a,b)))	→	convs(sequent(emptyfset,emptyfset))	(53)
((emptysset,a),ext)	→	*(a,ext)	(151)
((a,a),ext)	→	*(a,ext)	(152)
((convs(sequent(virg(f,a),virg(g,b))),convs(sequent(a,b))),ext)	→	*(convs(sequent(a,b)),ext)	(153)
((convs(sequent(virg(f,a),b)),convs(sequent(a,b))),ext)	→	*(convs(sequent(a,b)),ext)	(154)
((convs(sequent(a,virg(f,b))),convs(sequent(a,b))),ext)	→	*(convs(sequent(a,b)),ext)	(155)
((convs(sequent(virg(f,a),b)),convs(sequent(a,emptyfset))),ext)	→	*(convs(sequent(a,emptyfset)),ext)	(156)
((convs(sequent(emptyfset,b)),convs(sequent(a,virg(f,b)))),ext)	→	*(convs(sequent(emptyfset,b)),ext)	(157)
((convs(sequent(emptyfset,b)),convs(sequent(a,b))),ext)	→	*(convs(sequent(emptyfset,b)),ext)	(158)
((convs(sequent(a,emptyfset)),convs(sequent(a,b))),ext)	→	*(convs(sequent(a,emptyfset)),ext)	(159)
((convs(sequent(emptyfset,emptyfset)),convs(sequent(a,b))),ext)	→	*(convs(sequent(emptyfset,emptyfset)),ext)	(160)

could be deleted.

1.1.3.1 AC Dependency Pair Problem is trivial

There are no strict pairs and rules remaining, or there are no DPs remaining. Therefore, finiteness is trivially satisfied.

The 4^th component contains the pair

sequent^#(convf(neg(f)),b)	→	sequent^#(emptyfset,virg(convf(f),b))	(99)
sequent^#(a,virg(convf(neg(f)),b))	→	sequent^#(virg(convf(f),a),b)	(101)
sequent^#(virg(convf(neg(f)),a),b)	→	sequent^#(a,virg(convf(f),b))	(97)
sequent^#(a,convf(neg(f)))	→	sequent^#(virg(convf(f),a),emptyfset)	(103)
sequent^#(virg(convf(and(f,g)),a),b)	→	sequent^#(virg(convf(g),virg(convf(f),a)),b)	(105)
sequent^#(convf(and(f,g)),b)	→	sequent^#(virg(convf(f),convf(g)),b)	(108)
sequent^#(a,virg(convf(or(f,g)),b))	→	sequent^#(a,virg(virg(convf(f),convf(g)),b))	(110)
sequent^#(a,convf(or(f,g)))	→	sequent^#(a,virg(convf(f),convf(g)))	(113)

1.1.4 AC Monotonic Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[virg(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[emptyfset]	=	0
[sequent^#(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[convf(x₁)]	=	1 · x₁
[neg(x₁)]	=	1 + 3 · x₁
[and(x₁, x₂)]	=	1 + 2 · x₁ + 2 · x₂
[or(x₁, x₂)]	=	2 + 2 · x₁ + 2 · x₂

together with the usable rules

virg(virg(a,a),ext)	→	virg(a,ext)	(162)
virg(a,a)	→	a	(22)
virg(emptyfset,a)	→	a	(21)
virg(virg(emptyfset,a),ext)	→	virg(a,ext)	(161)
virg(x,y)	→	virg(y,x)	(55)
virg(virg(x,y),z)	→	virg(x,virg(y,z))	(57)

(w.r.t. the implicit argument filter of the reduction pair), the pairs

sequent^#(convf(neg(f)),b)	→	sequent^#(emptyfset,virg(convf(f),b))	(99)
sequent^#(a,virg(convf(neg(f)),b))	→	sequent^#(virg(convf(f),a),b)	(101)
sequent^#(a,convf(neg(f)))	→	sequent^#(virg(convf(f),a),emptyfset)	(103)
sequent^#(virg(convf(neg(f)),a),b)	→	sequent^#(a,virg(convf(f),b))	(97)
sequent^#(virg(convf(and(f,g)),a),b)	→	sequent^#(virg(convf(g),virg(convf(f),a)),b)	(105)
sequent^#(convf(and(f,g)),b)	→	sequent^#(virg(convf(f),convf(g)),b)	(108)
sequent^#(a,virg(convf(or(f,g)),b))	→	sequent^#(a,virg(virg(convf(f),convf(g)),b))	(110)
sequent^#(a,convf(or(f,g)))	→	sequent^#(a,virg(convf(f),convf(g)))	(113)

and the rules

substt(ef(x),y)	→	ef(substt(x,y))	(1)
substf(Pe(x),y)	→	Pe(substt(x,y))	(2)
substf(neg(f),s)	→	neg(substf(f,s))	(3)
substf(and(f,g),s)	→	and(substf(f,s),substf(g,s))	(4)
substf(or(f,g),s)	→	or(substf(f,s),substf(g,s))	(5)
substf(imp(f,g),s)	→	imp(substf(f,s),substf(g,s))	(6)
substf(forall(f),s)	→	forall(substf(f,.(1,ron(s,shift))))	(7)
substf(exists(f),s)	→	exists(substf(f,.(1,ron(s,shift))))	(8)
substt(x,id)	→	x	(9)
substf(f,id)	→	f	(10)
substt(substt(x,s),t)	→	substt(x,ron(s,t))	(11)
substf(substf(f,s),t)	→	substf(f,ron(s,t))	(12)
substt(1,.(x,s))	→	x	(13)
ron(id,s)	→	s	(14)
ron(shift,.(x,s))	→	s	(15)
ron(ron(s,t),u)	→	ron(s,ron(t,u))	(16)
ron(.(x,s),t)	→	.(substt(x,t),ron(s,t))	(17)
ron(s,id)	→	s	(18)
.(1,shift)	→	id	(19)
.(substt(1,s),ron(shift,s))	→	s	(20)
*(emptysset,a)	→	a	(23)
*(a,a)	→	a	(24)
neg(neg(f))	→	f	(25)
and(f,f)	→	f	(26)
or(f,f)	→	f	(27)
imp(f,g)	→	or(neg(f),g)	(28)
exists(f)	→	neg(forall(neg(f)))	(29)
sequent(virg(convf(neg(f)),a),b)	→	sequent(a,virg(convf(f),b))	(30)
sequent(convf(neg(f)),b)	→	sequent(emptyfset,virg(convf(f),b))	(31)
sequent(a,virg(convf(neg(f)),b))	→	sequent(virg(convf(f),a),b)	(32)
sequent(a,convf(neg(f)))	→	sequent(virg(convf(f),a),emptyfset)	(33)
sequent(virg(convf(and(f,g)),a),b)	→	sequent(virg(convf(g),virg(convf(f),a)),b)	(34)
sequent(convf(and(f,g)),b)	→	sequent(virg(convf(f),convf(g)),b)	(35)
sequent(a,virg(convf(or(f,g)),b))	→	sequent(a,virg(virg(convf(f),convf(g)),b))	(36)
sequent(a,convf(or(f,g)))	→	sequent(a,virg(convf(f),convf(g)))	(37)
convs(sequent(a,virg(convf(and(f,g)),b)))	→	*(convs(sequent(a,virg(convf(f),b))),convs(sequent(a,virg(convf(g),b))))	(38)
convs(sequent(a,convf(and(f,g))))	→	*(convs(sequent(a,convf(f))),convs(sequent(a,convf(g))))	(39)
convs(sequent(virg(convf(or(f,g)),a),b))	→	*(convs(sequent(virg(convf(f),a),b)),convs(sequent(virg(convf(g),a),b)))	(40)
convs(sequent(convf(or(f,g)),b))	→	*(convs(sequent(convf(f),b)),convs(sequent(convf(g),b)))	(41)
convs(sequent(virg(convf(f),a),virg(convf(f),b)))	→	emptysset	(42)
convs(sequent(virg(convf(f),a),convf(f)))	→	emptysset	(43)
convs(sequent(convf(f),virg(convf(f),b)))	→	emptysset	(44)
convs(sequent(convf(f),convf(f)))	→	emptysset	(45)
*(convs(sequent(virg(f,a),virg(g,b))),convs(sequent(a,b)))	→	convs(sequent(a,b))	(46)
*(convs(sequent(virg(f,a),b)),convs(sequent(a,b)))	→	convs(sequent(a,b))	(47)
*(convs(sequent(a,virg(f,b))),convs(sequent(a,b)))	→	convs(sequent(a,b))	(48)
*(convs(sequent(virg(f,a),b)),convs(sequent(a,emptyfset)))	→	convs(sequent(a,emptyfset))	(49)
*(convs(sequent(emptyfset,b)),convs(sequent(a,virg(f,b))))	→	convs(sequent(emptyfset,b))	(50)
*(convs(sequent(emptyfset,b)),convs(sequent(a,b)))	→	convs(sequent(emptyfset,b))	(51)
*(convs(sequent(a,emptyfset)),convs(sequent(a,b)))	→	convs(sequent(a,emptyfset))	(52)
*(convs(sequent(emptyfset,emptyfset)),convs(sequent(a,b)))	→	convs(sequent(emptyfset,emptyfset))	(53)
((emptysset,a),ext)	→	*(a,ext)	(151)
((a,a),ext)	→	*(a,ext)	(152)
((convs(sequent(virg(f,a),virg(g,b))),convs(sequent(a,b))),ext)	→	*(convs(sequent(a,b)),ext)	(153)
((convs(sequent(virg(f,a),b)),convs(sequent(a,b))),ext)	→	*(convs(sequent(a,b)),ext)	(154)
((convs(sequent(a,virg(f,b))),convs(sequent(a,b))),ext)	→	*(convs(sequent(a,b)),ext)	(155)
((convs(sequent(virg(f,a),b)),convs(sequent(a,emptyfset))),ext)	→	*(convs(sequent(a,emptyfset)),ext)	(156)
((convs(sequent(emptyfset,b)),convs(sequent(a,virg(f,b)))),ext)	→	*(convs(sequent(emptyfset,b)),ext)	(157)
((convs(sequent(emptyfset,b)),convs(sequent(a,b))),ext)	→	*(convs(sequent(emptyfset,b)),ext)	(158)
((convs(sequent(a,emptyfset)),convs(sequent(a,b))),ext)	→	*(convs(sequent(a,emptyfset)),ext)	(159)
((convs(sequent(emptyfset,emptyfset)),convs(sequent(a,b))),ext)	→	*(convs(sequent(emptyfset,emptyfset)),ext)	(160)

could be deleted.

1.1.4.1 AC Dependency Pair Problem is trivial

There are no strict pairs and rules remaining, or there are no DPs remaining. Therefore, finiteness is trivially satisfied.

The 5^th component contains the pair

^#((a,a),ext)	→	*^#(a,ext)	(140)
^#((emptysset,a),ext)	→	*^#(a,ext)	(139)
^#((convs(sequent(virg(f,a),virg(g,b))),convs(sequent(a,b))),ext)	→	*^#(convs(sequent(a,b)),ext)	(141)
^#((convs(sequent(virg(f,a),b)),convs(sequent(a,b))),ext)	→	*^#(convs(sequent(a,b)),ext)	(142)
^#((convs(sequent(a,virg(f,b))),convs(sequent(a,b))),ext)	→	*^#(convs(sequent(a,b)),ext)	(143)
^#((convs(sequent(virg(f,a),b)),convs(sequent(a,emptyfset))),ext)	→	*^#(convs(sequent(a,emptyfset)),ext)	(144)
^#((convs(sequent(emptyfset,b)),convs(sequent(a,virg(f,b)))),ext)	→	*^#(convs(sequent(emptyfset,b)),ext)	(145)
^#((convs(sequent(emptyfset,b)),convs(sequent(a,b))),ext)	→	*^#(convs(sequent(emptyfset,b)),ext)	(146)
^#((convs(sequent(a,emptyfset)),convs(sequent(a,b))),ext)	→	*^#(convs(sequent(a,emptyfset)),ext)	(147)
^#((convs(sequent(emptyfset,emptyfset)),convs(sequent(a,b))),ext)	→	*^#(convs(sequent(emptyfset,emptyfset)),ext)	(148)
^#((x,y),z)	→	*^#(y,z)	(62)
*^#(x,y)	→	*^#(y,x)	(58)
^#((x,y),z)	→	^#(x,(y,z))	(60)

1.1.5 AC Reduction Pair Processor with Usable Rules

Using the non-linear polynomial interpretation over the naturals

[*^#(x₁, x₂)]	=	1 · x₂ + 1 · x₁
[*(x₁, x₂)]	=	1 · x₂ + 1 · x₁
[convs(x₁)]	=	1 + 1 · x₁ · x₁
[sequent(x₁, x₂)]	=	1 · x₂ + 1 · x₁ + 1 · x₁ · x₂
[emptyfset]	=	0
[virg(x₁, x₂)]	=	1 · x₂ + 1 · x₁ + 1 · x₁ · x₂
[emptysset]	=	0
[convf(x₁)]	=	1 · x₁ · x₁
[and(x₁, x₂)]	=	1 + 1 · x₂ + 1 · x₁ + 1 · x₁ · x₂
[or(x₁, x₂)]	=	1 + 1 · x₂ + 1 · x₁ + 1 · x₁ · x₂
[neg(x₁)]	=	1 · x₁

together with the usable rules

((convs(sequent(emptyfset,emptyfset)),convs(sequent(a,b))),ext)	→	*(convs(sequent(emptyfset,emptyfset)),ext)	(160)
*(convs(sequent(emptyfset,b)),convs(sequent(a,virg(f,b))))	→	convs(sequent(emptyfset,b))	(50)
((convs(sequent(emptyfset,b)),convs(sequent(a,b))),ext)	→	*(convs(sequent(emptyfset,b)),ext)	(158)
((convs(sequent(a,emptyfset)),convs(sequent(a,b))),ext)	→	*(convs(sequent(a,emptyfset)),ext)	(159)
((convs(sequent(a,virg(f,b))),convs(sequent(a,b))),ext)	→	*(convs(sequent(a,b)),ext)	(155)
*(a,a)	→	a	(24)
((convs(sequent(virg(f,a),b)),convs(sequent(a,b))),ext)	→	*(convs(sequent(a,b)),ext)	(154)
*(convs(sequent(emptyfset,emptyfset)),convs(sequent(a,b)))	→	convs(sequent(emptyfset,emptyfset))	(53)
*(emptysset,a)	→	a	(23)
((emptysset,a),ext)	→	*(a,ext)	(151)
*(convs(sequent(virg(f,a),b)),convs(sequent(a,b)))	→	convs(sequent(a,b))	(47)
*(convs(sequent(a,virg(f,b))),convs(sequent(a,b)))	→	convs(sequent(a,b))	(48)
*(convs(sequent(virg(f,a),b)),convs(sequent(a,emptyfset)))	→	convs(sequent(a,emptyfset))	(49)
*(convs(sequent(virg(f,a),virg(g,b))),convs(sequent(a,b)))	→	convs(sequent(a,b))	(46)
((convs(sequent(virg(f,a),virg(g,b))),convs(sequent(a,b))),ext)	→	*(convs(sequent(a,b)),ext)	(153)
((convs(sequent(virg(f,a),b)),convs(sequent(a,emptyfset))),ext)	→	*(convs(sequent(a,emptyfset)),ext)	(156)
((a,a),ext)	→	*(a,ext)	(152)
((convs(sequent(emptyfset,b)),convs(sequent(a,virg(f,b)))),ext)	→	*(convs(sequent(emptyfset,b)),ext)	(157)
*(convs(sequent(emptyfset,b)),convs(sequent(a,b)))	→	convs(sequent(emptyfset,b))	(51)
*(convs(sequent(a,emptyfset)),convs(sequent(a,b)))	→	convs(sequent(a,emptyfset))	(52)
convs(sequent(a,convf(and(f,g))))	→	*(convs(sequent(a,convf(f))),convs(sequent(a,convf(g))))	(39)
convs(sequent(virg(convf(f),a),convf(f)))	→	emptysset	(43)
convs(sequent(convf(f),virg(convf(f),b)))	→	emptysset	(44)
convs(sequent(a,virg(convf(and(f,g)),b)))	→	*(convs(sequent(a,virg(convf(f),b))),convs(sequent(a,virg(convf(g),b))))	(38)
convs(sequent(convf(f),convf(f)))	→	emptysset	(45)
convs(sequent(convf(or(f,g)),b))	→	*(convs(sequent(convf(f),b)),convs(sequent(convf(g),b)))	(41)
convs(sequent(virg(convf(or(f,g)),a),b))	→	*(convs(sequent(virg(convf(f),a),b)),convs(sequent(virg(convf(g),a),b)))	(40)
convs(sequent(virg(convf(f),a),virg(convf(f),b)))	→	emptysset	(42)
sequent(a,virg(convf(neg(f)),b))	→	sequent(virg(convf(f),a),b)	(32)
sequent(virg(convf(neg(f)),a),b)	→	sequent(a,virg(convf(f),b))	(30)
sequent(virg(convf(and(f,g)),a),b)	→	sequent(virg(convf(g),virg(convf(f),a)),b)	(34)
sequent(convf(neg(f)),b)	→	sequent(emptyfset,virg(convf(f),b))	(31)
sequent(a,convf(neg(f)))	→	sequent(virg(convf(f),a),emptyfset)	(33)
sequent(convf(and(f,g)),b)	→	sequent(virg(convf(f),convf(g)),b)	(35)
sequent(a,virg(convf(or(f,g)),b))	→	sequent(a,virg(virg(convf(f),convf(g)),b))	(36)
sequent(a,convf(or(f,g)))	→	sequent(a,virg(convf(f),convf(g)))	(37)
virg(virg(a,a),ext)	→	virg(a,ext)	(162)
virg(virg(emptyfset,a),ext)	→	virg(a,ext)	(161)
virg(emptyfset,a)	→	a	(21)
virg(a,a)	→	a	(22)
((x,y),z)	→	(x,(y,z))	(56)
*(x,y)	→	*(y,x)	(54)
virg(x,y)	→	virg(y,x)	(55)
virg(virg(x,y),z)	→	virg(x,virg(y,z))	(57)

(w.r.t. the implicit argument filter of the reduction pair), the pairs

^#((convs(sequent(emptyfset,b)),convs(sequent(a,virg(f,b)))),ext)	→	*^#(convs(sequent(emptyfset,b)),ext)	(145)
^#((convs(sequent(virg(f,a),b)),convs(sequent(a,b))),ext)	→	*^#(convs(sequent(a,b)),ext)	(142)
^#((convs(sequent(a,virg(f,b))),convs(sequent(a,b))),ext)	→	*^#(convs(sequent(a,b)),ext)	(143)
^#((convs(sequent(virg(f,a),b)),convs(sequent(a,emptyfset))),ext)	→	*^#(convs(sequent(a,emptyfset)),ext)	(144)
^#((convs(sequent(emptyfset,emptyfset)),convs(sequent(a,b))),ext)	→	*^#(convs(sequent(emptyfset,emptyfset)),ext)	(148)
^#((convs(sequent(virg(f,a),virg(g,b))),convs(sequent(a,b))),ext)	→	*^#(convs(sequent(a,b)),ext)	(141)
^#((convs(sequent(emptyfset,b)),convs(sequent(a,b))),ext)	→	*^#(convs(sequent(emptyfset,b)),ext)	(146)
^#((convs(sequent(a,emptyfset)),convs(sequent(a,b))),ext)	→	*^#(convs(sequent(a,emptyfset)),ext)	(147)

could be deleted.

1.1.5.1 AC Reduction Pair Processor with Usable Rules

Using the non-linear polynomial interpretation over the naturals

[*^#(x₁, x₂)]	=	1 · x₂ + 1 · x₁
[*(x₁, x₂)]	=	1 + 1 · x₂ + 1 · x₁
[emptysset]	=	0
[convs(x₁)]	=	1 · x₁
[sequent(x₁, x₂)]	=	1 · x₂ + 1 · x₁ + 1 · x₁ · x₂
[emptyfset]	=	0
[virg(x₁, x₂)]	=	1 · x₂ + 1 · x₁ + 1 · x₁ · x₂
[convf(x₁)]	=	1 · x₁
[and(x₁, x₂)]	=	1 + 1 · x₂ + 1 · x₁ + 1 · x₁ · x₂
[or(x₁, x₂)]	=	1 + 1 · x₂ + 1 · x₁ + 1 · x₁ · x₂
[neg(x₁)]	=	1 · x₁ + 1 · x₁ · x₁

together with the usable rules

((convs(sequent(emptyfset,emptyfset)),convs(sequent(a,b))),ext)	→	*(convs(sequent(emptyfset,emptyfset)),ext)	(160)
*(convs(sequent(emptyfset,b)),convs(sequent(a,virg(f,b))))	→	convs(sequent(emptyfset,b))	(50)
((convs(sequent(emptyfset,b)),convs(sequent(a,b))),ext)	→	*(convs(sequent(emptyfset,b)),ext)	(158)
((convs(sequent(a,emptyfset)),convs(sequent(a,b))),ext)	→	*(convs(sequent(a,emptyfset)),ext)	(159)
((convs(sequent(a,virg(f,b))),convs(sequent(a,b))),ext)	→	*(convs(sequent(a,b)),ext)	(155)
*(a,a)	→	a	(24)
((convs(sequent(virg(f,a),b)),convs(sequent(a,b))),ext)	→	*(convs(sequent(a,b)),ext)	(154)
*(convs(sequent(emptyfset,emptyfset)),convs(sequent(a,b)))	→	convs(sequent(emptyfset,emptyfset))	(53)
*(emptysset,a)	→	a	(23)
((emptysset,a),ext)	→	*(a,ext)	(151)
*(convs(sequent(virg(f,a),b)),convs(sequent(a,b)))	→	convs(sequent(a,b))	(47)
*(convs(sequent(a,virg(f,b))),convs(sequent(a,b)))	→	convs(sequent(a,b))	(48)
*(convs(sequent(virg(f,a),b)),convs(sequent(a,emptyfset)))	→	convs(sequent(a,emptyfset))	(49)
*(convs(sequent(virg(f,a),virg(g,b))),convs(sequent(a,b)))	→	convs(sequent(a,b))	(46)
((convs(sequent(virg(f,a),virg(g,b))),convs(sequent(a,b))),ext)	→	*(convs(sequent(a,b)),ext)	(153)
((convs(sequent(virg(f,a),b)),convs(sequent(a,emptyfset))),ext)	→	*(convs(sequent(a,emptyfset)),ext)	(156)
((a,a),ext)	→	*(a,ext)	(152)
((convs(sequent(emptyfset,b)),convs(sequent(a,virg(f,b)))),ext)	→	*(convs(sequent(emptyfset,b)),ext)	(157)
*(convs(sequent(emptyfset,b)),convs(sequent(a,b)))	→	convs(sequent(emptyfset,b))	(51)
*(convs(sequent(a,emptyfset)),convs(sequent(a,b)))	→	convs(sequent(a,emptyfset))	(52)
convs(sequent(a,convf(and(f,g))))	→	*(convs(sequent(a,convf(f))),convs(sequent(a,convf(g))))	(39)
convs(sequent(virg(convf(f),a),convf(f)))	→	emptysset	(43)
convs(sequent(convf(f),virg(convf(f),b)))	→	emptysset	(44)
convs(sequent(a,virg(convf(and(f,g)),b)))	→	*(convs(sequent(a,virg(convf(f),b))),convs(sequent(a,virg(convf(g),b))))	(38)
convs(sequent(convf(f),convf(f)))	→	emptysset	(45)
convs(sequent(convf(or(f,g)),b))	→	*(convs(sequent(convf(f),b)),convs(sequent(convf(g),b)))	(41)
convs(sequent(virg(convf(or(f,g)),a),b))	→	*(convs(sequent(virg(convf(f),a),b)),convs(sequent(virg(convf(g),a),b)))	(40)
convs(sequent(virg(convf(f),a),virg(convf(f),b)))	→	emptysset	(42)
sequent(a,virg(convf(neg(f)),b))	→	sequent(virg(convf(f),a),b)	(32)
sequent(virg(convf(neg(f)),a),b)	→	sequent(a,virg(convf(f),b))	(30)
sequent(virg(convf(and(f,g)),a),b)	→	sequent(virg(convf(g),virg(convf(f),a)),b)	(34)
sequent(convf(neg(f)),b)	→	sequent(emptyfset,virg(convf(f),b))	(31)
sequent(a,convf(neg(f)))	→	sequent(virg(convf(f),a),emptyfset)	(33)
sequent(convf(and(f,g)),b)	→	sequent(virg(convf(f),convf(g)),b)	(35)
sequent(a,virg(convf(or(f,g)),b))	→	sequent(a,virg(virg(convf(f),convf(g)),b))	(36)
sequent(a,convf(or(f,g)))	→	sequent(a,virg(convf(f),convf(g)))	(37)
virg(virg(a,a),ext)	→	virg(a,ext)	(162)
virg(virg(emptyfset,a),ext)	→	virg(a,ext)	(161)
virg(emptyfset,a)	→	a	(21)
virg(a,a)	→	a	(22)
((x,y),z)	→	(x,(y,z))	(56)
*(x,y)	→	*(y,x)	(54)
virg(x,y)	→	virg(y,x)	(55)
virg(virg(x,y),z)	→	virg(x,virg(y,z))	(57)

(w.r.t. the implicit argument filter of the reduction pair), the pairs

^#((a,a),ext)	→	*^#(a,ext)	(140)
^#((emptysset,a),ext)	→	*^#(a,ext)	(139)
^#((x,y),z)	→	*^#(y,z)	(62)

could be deleted.

1.1.5.1.1 AC Dependency Pair Problem is trivial

There are no strict pairs and rules remaining, or there are no DPs remaining. Therefore, finiteness is trivially satisfied.

The 6^th component contains the pair

virg^#(virg(a,a),ext)	→	virg^#(a,ext)	(150)
virg^#(virg(emptyfset,a),ext)	→	virg^#(a,ext)	(149)
virg^#(virg(x,y),z)	→	virg^#(y,z)	(63)
virg^#(x,y)	→	virg^#(y,x)	(59)
virg^#(virg(x,y),z)	→	virg^#(x,virg(y,z))	(61)

1.1.6 AC Monotonic Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[virg^#(x₁, x₂)]	=	3 · x₁ + 3 · x₂
[virg(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[emptyfset]	=	0

together with the usable rules

virg(virg(a,a),ext)	→	virg(a,ext)	(162)
virg(a,a)	→	a	(22)
virg(emptyfset,a)	→	a	(21)
virg(virg(emptyfset,a),ext)	→	virg(a,ext)	(161)
virg(x,y)	→	virg(y,x)	(55)
virg(virg(x,y),z)	→	virg(x,virg(y,z))	(57)

(w.r.t. the implicit argument filter of the reduction pair), the pair

virg^#(virg(emptyfset,a),ext)

→

virg^#(a,ext)

(149)

and the rules

substt(ef(x),y)	→	ef(substt(x,y))	(1)
substf(Pe(x),y)	→	Pe(substt(x,y))	(2)
substf(neg(f),s)	→	neg(substf(f,s))	(3)
substf(and(f,g),s)	→	and(substf(f,s),substf(g,s))	(4)
substf(or(f,g),s)	→	or(substf(f,s),substf(g,s))	(5)
substf(imp(f,g),s)	→	imp(substf(f,s),substf(g,s))	(6)
substf(forall(f),s)	→	forall(substf(f,.(1,ron(s,shift))))	(7)
substf(exists(f),s)	→	exists(substf(f,.(1,ron(s,shift))))	(8)
substt(x,id)	→	x	(9)
substf(f,id)	→	f	(10)
substt(substt(x,s),t)	→	substt(x,ron(s,t))	(11)
substf(substf(f,s),t)	→	substf(f,ron(s,t))	(12)
substt(1,.(x,s))	→	x	(13)
ron(id,s)	→	s	(14)
ron(shift,.(x,s))	→	s	(15)
ron(ron(s,t),u)	→	ron(s,ron(t,u))	(16)
ron(.(x,s),t)	→	.(substt(x,t),ron(s,t))	(17)
ron(s,id)	→	s	(18)
.(1,shift)	→	id	(19)
.(substt(1,s),ron(shift,s))	→	s	(20)
virg(emptyfset,a)	→	a	(21)
*(emptysset,a)	→	a	(23)
*(a,a)	→	a	(24)
neg(neg(f))	→	f	(25)
and(f,f)	→	f	(26)
or(f,f)	→	f	(27)
imp(f,g)	→	or(neg(f),g)	(28)
exists(f)	→	neg(forall(neg(f)))	(29)
sequent(virg(convf(neg(f)),a),b)	→	sequent(a,virg(convf(f),b))	(30)
sequent(convf(neg(f)),b)	→	sequent(emptyfset,virg(convf(f),b))	(31)
sequent(a,virg(convf(neg(f)),b))	→	sequent(virg(convf(f),a),b)	(32)
sequent(a,convf(neg(f)))	→	sequent(virg(convf(f),a),emptyfset)	(33)
sequent(virg(convf(and(f,g)),a),b)	→	sequent(virg(convf(g),virg(convf(f),a)),b)	(34)
sequent(convf(and(f,g)),b)	→	sequent(virg(convf(f),convf(g)),b)	(35)
sequent(a,virg(convf(or(f,g)),b))	→	sequent(a,virg(virg(convf(f),convf(g)),b))	(36)
sequent(a,convf(or(f,g)))	→	sequent(a,virg(convf(f),convf(g)))	(37)
convs(sequent(a,virg(convf(and(f,g)),b)))	→	*(convs(sequent(a,virg(convf(f),b))),convs(sequent(a,virg(convf(g),b))))	(38)
convs(sequent(a,convf(and(f,g))))	→	*(convs(sequent(a,convf(f))),convs(sequent(a,convf(g))))	(39)
convs(sequent(virg(convf(or(f,g)),a),b))	→	*(convs(sequent(virg(convf(f),a),b)),convs(sequent(virg(convf(g),a),b)))	(40)
convs(sequent(convf(or(f,g)),b))	→	*(convs(sequent(convf(f),b)),convs(sequent(convf(g),b)))	(41)
convs(sequent(virg(convf(f),a),virg(convf(f),b)))	→	emptysset	(42)
convs(sequent(virg(convf(f),a),convf(f)))	→	emptysset	(43)
convs(sequent(convf(f),virg(convf(f),b)))	→	emptysset	(44)
convs(sequent(convf(f),convf(f)))	→	emptysset	(45)
*(convs(sequent(virg(f,a),virg(g,b))),convs(sequent(a,b)))	→	convs(sequent(a,b))	(46)
*(convs(sequent(virg(f,a),b)),convs(sequent(a,b)))	→	convs(sequent(a,b))	(47)
*(convs(sequent(a,virg(f,b))),convs(sequent(a,b)))	→	convs(sequent(a,b))	(48)
*(convs(sequent(virg(f,a),b)),convs(sequent(a,emptyfset)))	→	convs(sequent(a,emptyfset))	(49)
*(convs(sequent(emptyfset,b)),convs(sequent(a,virg(f,b))))	→	convs(sequent(emptyfset,b))	(50)
*(convs(sequent(emptyfset,b)),convs(sequent(a,b)))	→	convs(sequent(emptyfset,b))	(51)
*(convs(sequent(a,emptyfset)),convs(sequent(a,b)))	→	convs(sequent(a,emptyfset))	(52)
*(convs(sequent(emptyfset,emptyfset)),convs(sequent(a,b)))	→	convs(sequent(emptyfset,emptyfset))	(53)
((emptysset,a),ext)	→	*(a,ext)	(151)
((a,a),ext)	→	*(a,ext)	(152)
((convs(sequent(virg(f,a),virg(g,b))),convs(sequent(a,b))),ext)	→	*(convs(sequent(a,b)),ext)	(153)
((convs(sequent(virg(f,a),b)),convs(sequent(a,b))),ext)	→	*(convs(sequent(a,b)),ext)	(154)
((convs(sequent(a,virg(f,b))),convs(sequent(a,b))),ext)	→	*(convs(sequent(a,b)),ext)	(155)
((convs(sequent(virg(f,a),b)),convs(sequent(a,emptyfset))),ext)	→	*(convs(sequent(a,emptyfset)),ext)	(156)
((convs(sequent(emptyfset,b)),convs(sequent(a,virg(f,b)))),ext)	→	*(convs(sequent(emptyfset,b)),ext)	(157)
((convs(sequent(emptyfset,b)),convs(sequent(a,b))),ext)	→	*(convs(sequent(emptyfset,b)),ext)	(158)
((convs(sequent(a,emptyfset)),convs(sequent(a,b))),ext)	→	*(convs(sequent(a,emptyfset)),ext)	(159)
((convs(sequent(emptyfset,emptyfset)),convs(sequent(a,b))),ext)	→	*(convs(sequent(emptyfset,emptyfset)),ext)	(160)
virg(virg(emptyfset,a),ext)	→	virg(a,ext)	(161)

could be deleted.

1.1.6.1 AC Monotonic Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[virg^#(x₁, x₂)]	=	3 · x₁ + 3 · x₂
[virg(x₁, x₂)]	=	3 + 1 · x₁ + 1 · x₂
[*(x₁, x₂)]	=	1 · x₁ + 1 · x₂

together with the usable rules

virg(virg(a,a),ext)	→	virg(a,ext)	(162)
virg(a,a)	→	a	(22)
*(x,y)	→	*(y,x)	(54)
virg(x,y)	→	virg(y,x)	(55)
((x,y),z)	→	(x,(y,z))	(56)
virg(virg(x,y),z)	→	virg(x,virg(y,z))	(57)

(w.r.t. the implicit argument filter of the reduction pair), the pairs

virg^#(virg(a,a),ext)	→	virg^#(a,ext)	(150)
virg^#(virg(x,y),z)	→	virg^#(y,z)	(63)

and the rules

virg(virg(a,a),ext)	→	virg(a,ext)	(162)
virg(a,a)	→	a	(22)

could be deleted.

1.1.6.1.1 AC Dependency Pair Problem is trivial

There are no strict pairs and rules remaining, or there are no DPs remaining. Therefore, finiteness is trivially satisfied.