Certification Problem

Input (TPDB TRS_Standard/HirokawaMiddeldorp_04/t009)

The rewrite relation of the following TRS is considered.

start(i)	→	busy(F,closed,stop,false,false,false,i)	(1)
busy(BF,d,stop,b1,b2,b3,i)	→	incorrect	(2)
busy(FS,d,stop,b1,b2,b3,i)	→	incorrect	(3)
busy(fl,open,up,b1,b2,b3,i)	→	incorrect	(4)
busy(fl,open,down,b1,b2,b3,i)	→	incorrect	(5)
busy(B,closed,stop,false,false,false,empty)	→	correct	(6)
busy(F,closed,stop,false,false,false,empty)	→	correct	(7)
busy(S,closed,stop,false,false,false,empty)	→	correct	(8)
busy(B,closed,stop,false,false,false,newbuttons(i1,i2,i3,i))	→	idle(B,closed,stop,false,false,false,newbuttons(i1,i2,i3,i))	(9)
busy(F,closed,stop,false,false,false,newbuttons(i1,i2,i3,i))	→	idle(F,closed,stop,false,false,false,newbuttons(i1,i2,i3,i))	(10)
busy(S,closed,stop,false,false,false,newbuttons(i1,i2,i3,i))	→	idle(S,closed,stop,false,false,false,newbuttons(i1,i2,i3,i))	(11)
busy(B,open,stop,false,b2,b3,i)	→	idle(B,closed,stop,false,b2,b3,i)	(12)
busy(F,open,stop,b1,false,b3,i)	→	idle(F,closed,stop,b1,false,b3,i)	(13)
busy(S,open,stop,b1,b2,false,i)	→	idle(S,closed,stop,b1,b2,false,i)	(14)
busy(B,d,stop,true,b2,b3,i)	→	idle(B,open,stop,false,b2,b3,i)	(15)
busy(F,d,stop,b1,true,b3,i)	→	idle(F,open,stop,b1,false,b3,i)	(16)
busy(S,d,stop,b1,b2,true,i)	→	idle(S,open,stop,b1,b2,false,i)	(17)
busy(B,closed,down,b1,b2,b3,i)	→	idle(B,closed,stop,b1,b2,b3,i)	(18)
busy(S,closed,up,b1,b2,b3,i)	→	idle(S,closed,stop,b1,b2,b3,i)	(19)
busy(B,closed,up,true,b2,b3,i)	→	idle(B,closed,stop,true,b2,b3,i)	(20)
busy(F,closed,up,b1,true,b3,i)	→	idle(F,closed,stop,b1,true,b3,i)	(21)
busy(F,closed,down,b1,true,b3,i)	→	idle(F,closed,stop,b1,true,b3,i)	(22)
busy(S,closed,down,b1,b2,true,i)	→	idle(S,closed,stop,b1,b2,true,i)	(23)
busy(B,closed,up,false,b2,b3,i)	→	idle(BF,closed,up,false,b2,b3,i)	(24)
busy(F,closed,up,b1,false,b3,i)	→	idle(FS,closed,up,b1,false,b3,i)	(25)
busy(F,closed,down,b1,false,b3,i)	→	idle(BF,closed,down,b1,false,b3,i)	(26)
busy(S,closed,down,b1,b2,false,i)	→	idle(FS,closed,down,b1,b2,false,i)	(27)
busy(BF,closed,up,b1,b2,b3,i)	→	idle(F,closed,up,b1,b2,b3,i)	(28)
busy(BF,closed,down,b1,b2,b3,i)	→	idle(B,closed,down,b1,b2,b3,i)	(29)
busy(FS,closed,up,b1,b2,b3,i)	→	idle(S,closed,up,b1,b2,b3,i)	(30)
busy(FS,closed,down,b1,b2,b3,i)	→	idle(F,closed,down,b1,b2,b3,i)	(31)
busy(B,closed,stop,false,true,b3,i)	→	idle(B,closed,up,false,true,b3,i)	(32)
busy(B,closed,stop,false,false,true,i)	→	idle(B,closed,up,false,false,true,i)	(33)
busy(F,closed,stop,true,false,b3,i)	→	idle(F,closed,down,true,false,b3,i)	(34)
busy(F,closed,stop,false,false,true,i)	→	idle(F,closed,up,false,false,true,i)	(35)
busy(S,closed,stop,b1,true,false,i)	→	idle(S,closed,down,b1,true,false,i)	(36)
busy(S,closed,stop,true,false,false,i)	→	idle(S,closed,down,true,false,false,i)	(37)
idle(fl,d,m,b1,b2,b3,empty)	→	busy(fl,d,m,b1,b2,b3,empty)	(38)
idle(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i))	→	busy(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i)	(39)
or(true,b)	→	true	(40)
or(false,b)	→	b	(41)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

busy^#(F,closed,stop,false,false,true,i)	→	idle^#(F,closed,up,false,false,true,i)	(42)
busy^#(F,closed,down,b1,false,b3,i)	→	idle^#(BF,closed,down,b1,false,b3,i)	(43)
busy^#(B,closed,down,b1,b2,b3,i)	→	idle^#(B,closed,stop,b1,b2,b3,i)	(44)
busy^#(B,closed,stop,false,false,false,newbuttons(i1,i2,i3,i))	→	idle^#(B,closed,stop,false,false,false,newbuttons(i1,i2,i3,i))	(45)
busy^#(FS,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,up,b1,b2,b3,i)	(46)
busy^#(S,closed,down,b1,b2,true,i)	→	idle^#(S,closed,stop,b1,b2,true,i)	(47)
busy^#(FS,closed,down,b1,b2,b3,i)	→	idle^#(F,closed,down,b1,b2,b3,i)	(48)
busy^#(F,closed,stop,true,false,b3,i)	→	idle^#(F,closed,down,true,false,b3,i)	(49)
busy^#(F,closed,down,b1,true,b3,i)	→	idle^#(F,closed,stop,b1,true,b3,i)	(50)
busy^#(S,open,stop,b1,b2,false,i)	→	idle^#(S,closed,stop,b1,b2,false,i)	(51)
busy^#(F,closed,up,b1,true,b3,i)	→	idle^#(F,closed,stop,b1,true,b3,i)	(52)
busy^#(F,closed,up,b1,false,b3,i)	→	idle^#(FS,closed,up,b1,false,b3,i)	(53)
busy^#(S,closed,stop,b1,true,false,i)	→	idle^#(S,closed,down,b1,true,false,i)	(54)
busy^#(S,closed,down,b1,b2,false,i)	→	idle^#(FS,closed,down,b1,b2,false,i)	(55)
busy^#(F,closed,stop,false,false,false,newbuttons(i1,i2,i3,i))	→	idle^#(F,closed,stop,false,false,false,newbuttons(i1,i2,i3,i))	(56)
busy^#(S,closed,stop,false,false,false,newbuttons(i1,i2,i3,i))	→	idle^#(S,closed,stop,false,false,false,newbuttons(i1,i2,i3,i))	(57)
busy^#(B,open,stop,false,b2,b3,i)	→	idle^#(B,closed,stop,false,b2,b3,i)	(58)
start^#(i)	→	busy^#(F,closed,stop,false,false,false,i)	(59)
busy^#(F,open,stop,b1,false,b3,i)	→	idle^#(F,closed,stop,b1,false,b3,i)	(60)
busy^#(S,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,stop,b1,b2,b3,i)	(61)
busy^#(BF,closed,up,b1,b2,b3,i)	→	idle^#(F,closed,up,b1,b2,b3,i)	(62)
busy^#(B,d,stop,true,b2,b3,i)	→	idle^#(B,open,stop,false,b2,b3,i)	(63)
busy^#(B,closed,stop,false,true,b3,i)	→	idle^#(B,closed,up,false,true,b3,i)	(64)
idle^#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i))	→	or^#(b1,i1)	(65)
busy^#(F,d,stop,b1,true,b3,i)	→	idle^#(F,open,stop,b1,false,b3,i)	(66)
idle^#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i))	→	or^#(b3,i3)	(67)
busy^#(S,d,stop,b1,b2,true,i)	→	idle^#(S,open,stop,b1,b2,false,i)	(68)
busy^#(B,closed,stop,false,false,true,i)	→	idle^#(B,closed,up,false,false,true,i)	(69)
idle^#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i))	→	busy^#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i)	(70)
busy^#(S,closed,stop,true,false,false,i)	→	idle^#(S,closed,down,true,false,false,i)	(71)
busy^#(BF,closed,down,b1,b2,b3,i)	→	idle^#(B,closed,down,b1,b2,b3,i)	(72)
busy^#(B,closed,up,false,b2,b3,i)	→	idle^#(BF,closed,up,false,b2,b3,i)	(73)
busy^#(B,closed,up,true,b2,b3,i)	→	idle^#(B,closed,stop,true,b2,b3,i)	(74)
idle^#(fl,d,m,b1,b2,b3,empty)	→	busy^#(fl,d,m,b1,b2,b3,empty)	(75)
idle^#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i))	→	or^#(b2,i2)	(76)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

busy^#(S,closed,down,b1,b2,false,i)	→	idle^#(FS,closed,down,b1,b2,false,i)	(55)
idle^#(fl,d,m,b1,b2,b3,empty)	→	busy^#(fl,d,m,b1,b2,b3,empty)	(75)
busy^#(S,closed,stop,b1,true,false,i)	→	idle^#(S,closed,down,b1,true,false,i)	(54)
busy^#(F,closed,up,b1,false,b3,i)	→	idle^#(FS,closed,up,b1,false,b3,i)	(53)
busy^#(B,closed,up,true,b2,b3,i)	→	idle^#(B,closed,stop,true,b2,b3,i)	(74)
busy^#(F,closed,up,b1,true,b3,i)	→	idle^#(F,closed,stop,b1,true,b3,i)	(52)
busy^#(S,open,stop,b1,b2,false,i)	→	idle^#(S,closed,stop,b1,b2,false,i)	(51)
busy^#(B,closed,up,false,b2,b3,i)	→	idle^#(BF,closed,up,false,b2,b3,i)	(73)
busy^#(BF,closed,down,b1,b2,b3,i)	→	idle^#(B,closed,down,b1,b2,b3,i)	(72)
busy^#(F,closed,down,b1,true,b3,i)	→	idle^#(F,closed,stop,b1,true,b3,i)	(50)
busy^#(S,closed,stop,true,false,false,i)	→	idle^#(S,closed,down,true,false,false,i)	(71)
busy^#(F,closed,stop,true,false,b3,i)	→	idle^#(F,closed,down,true,false,b3,i)	(49)
idle^#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i))	→	busy^#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i)	(70)
busy^#(B,closed,stop,false,false,true,i)	→	idle^#(B,closed,up,false,false,true,i)	(69)
busy^#(S,d,stop,b1,b2,true,i)	→	idle^#(S,open,stop,b1,b2,false,i)	(68)
busy^#(FS,closed,down,b1,b2,b3,i)	→	idle^#(F,closed,down,b1,b2,b3,i)	(48)
busy^#(S,closed,down,b1,b2,true,i)	→	idle^#(S,closed,stop,b1,b2,true,i)	(47)
busy^#(FS,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,up,b1,b2,b3,i)	(46)
busy^#(F,d,stop,b1,true,b3,i)	→	idle^#(F,open,stop,b1,false,b3,i)	(66)
busy^#(B,closed,stop,false,false,false,newbuttons(i1,i2,i3,i))	→	idle^#(B,closed,stop,false,false,false,newbuttons(i1,i2,i3,i))	(45)
busy^#(B,closed,stop,false,true,b3,i)	→	idle^#(B,closed,up,false,true,b3,i)	(64)
busy^#(B,d,stop,true,b2,b3,i)	→	idle^#(B,open,stop,false,b2,b3,i)	(63)
busy^#(BF,closed,up,b1,b2,b3,i)	→	idle^#(F,closed,up,b1,b2,b3,i)	(62)
busy^#(S,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,stop,b1,b2,b3,i)	(61)
busy^#(F,open,stop,b1,false,b3,i)	→	idle^#(F,closed,stop,b1,false,b3,i)	(60)
busy^#(B,open,stop,false,b2,b3,i)	→	idle^#(B,closed,stop,false,b2,b3,i)	(58)
busy^#(S,closed,stop,false,false,false,newbuttons(i1,i2,i3,i))	→	idle^#(S,closed,stop,false,false,false,newbuttons(i1,i2,i3,i))	(57)
busy^#(B,closed,down,b1,b2,b3,i)	→	idle^#(B,closed,stop,b1,b2,b3,i)	(44)
busy^#(F,closed,down,b1,false,b3,i)	→	idle^#(BF,closed,down,b1,false,b3,i)	(43)
busy^#(F,closed,stop,false,false,true,i)	→	idle^#(F,closed,up,false,false,true,i)	(42)
busy^#(F,closed,stop,false,false,false,newbuttons(i1,i2,i3,i))	→	idle^#(F,closed,stop,false,false,false,newbuttons(i1,i2,i3,i))	(56)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[stop]	=	12280
[newbuttons(x₁,...,x₄)]	=	x₂ + x₃ + x₄ + 13508
[S]	=	1
[F]	=	1
[idle^#(x₁,...,x₇)]	=	x₃ + x₆ + x₇ + 0
[false]	=	1
[closed]	=	1
[down]	=	12280
[incorrect]	=	0
[idle(x₁,...,x₇)]	=	0
[true]	=	2
[correct]	=	0
[B]	=	1
[FS]	=	1
[or(x₁, x₂)]	=	x₂ + 13507
[busy(x₁,...,x₇)]	=	0
[start^#(x₁)]	=	0
[open]	=	1
[busy^#(x₁,...,x₇)]	=	x₃ + x₆ + x₇ + 0
[empty]	=	0
[start(x₁)]	=	0
[BF]	=	1
[or^#(x₁, x₂)]	=	0
[up]	=	12280

together with the usable rules

or(true,b)	→	true	(40)
or(false,b)	→	b	(41)

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

idle^#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i))	→	busy^#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i)	(70)
busy^#(S,d,stop,b1,b2,true,i)	→	idle^#(S,open,stop,b1,b2,false,i)	(68)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

busy^#(B,closed,down,b1,b2,b3,i)	→	idle^#(B,closed,stop,b1,b2,b3,i)	(44)
busy^#(B,d,stop,true,b2,b3,i)	→	idle^#(B,open,stop,false,b2,b3,i)	(63)
busy^#(F,d,stop,b1,true,b3,i)	→	idle^#(F,open,stop,b1,false,b3,i)	(66)
busy^#(F,closed,up,b1,true,b3,i)	→	idle^#(F,closed,stop,b1,true,b3,i)	(52)
busy^#(S,closed,stop,b1,true,false,i)	→	idle^#(S,closed,down,b1,true,false,i)	(54)
busy^#(F,closed,down,b1,false,b3,i)	→	idle^#(BF,closed,down,b1,false,b3,i)	(43)
busy^#(S,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,stop,b1,b2,b3,i)	(61)
busy^#(B,closed,stop,false,true,b3,i)	→	idle^#(B,closed,up,false,true,b3,i)	(64)
busy^#(S,closed,down,b1,b2,false,i)	→	idle^#(FS,closed,down,b1,b2,false,i)	(55)
busy^#(F,closed,stop,true,false,b3,i)	→	idle^#(F,closed,down,true,false,b3,i)	(49)
busy^#(F,closed,down,b1,true,b3,i)	→	idle^#(F,closed,stop,b1,true,b3,i)	(50)
busy^#(BF,closed,up,b1,b2,b3,i)	→	idle^#(F,closed,up,b1,b2,b3,i)	(62)
busy^#(B,closed,stop,false,false,true,i)	→	idle^#(B,closed,up,false,false,true,i)	(69)
busy^#(B,closed,up,true,b2,b3,i)	→	idle^#(B,closed,stop,true,b2,b3,i)	(74)
busy^#(F,closed,up,b1,false,b3,i)	→	idle^#(FS,closed,up,b1,false,b3,i)	(53)
busy^#(FS,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,up,b1,b2,b3,i)	(46)
busy^#(S,open,stop,b1,b2,false,i)	→	idle^#(S,closed,stop,b1,b2,false,i)	(51)
busy^#(FS,closed,down,b1,b2,b3,i)	→	idle^#(F,closed,down,b1,b2,b3,i)	(48)
busy^#(B,open,stop,false,b2,b3,i)	→	idle^#(B,closed,stop,false,b2,b3,i)	(58)
busy^#(S,closed,down,b1,b2,true,i)	→	idle^#(S,closed,stop,b1,b2,true,i)	(47)
busy^#(B,closed,up,false,b2,b3,i)	→	idle^#(BF,closed,up,false,b2,b3,i)	(73)
busy^#(F,open,stop,b1,false,b3,i)	→	idle^#(F,closed,stop,b1,false,b3,i)	(60)
idle^#(fl,d,m,b1,b2,b3,empty)	→	busy^#(fl,d,m,b1,b2,b3,empty)	(75)
busy^#(S,closed,stop,true,false,false,i)	→	idle^#(S,closed,down,true,false,false,i)	(71)
busy^#(F,closed,stop,false,false,true,i)	→	idle^#(F,closed,up,false,false,true,i)	(42)
busy^#(BF,closed,down,b1,b2,b3,i)	→	idle^#(B,closed,down,b1,b2,b3,i)	(72)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[stop]	=	1
[newbuttons(x₁,...,x₄)]	=	13508
[S]	=	1
[F]	=	1
[idle^#(x₁,...,x₇)]	=	x₄ + x₆ + x₇ + 0
[false]	=	1
[closed]	=	1
[down]	=	1
[incorrect]	=	0
[idle(x₁,...,x₇)]	=	0
[true]	=	2
[correct]	=	0
[B]	=	1
[FS]	=	1
[or(x₁, x₂)]	=	x₂ + 13507
[busy(x₁,...,x₇)]	=	0
[start^#(x₁)]	=	0
[open]	=	1
[busy^#(x₁,...,x₇)]	=	x₄ + x₆ + x₇ + 0
[empty]	=	39945
[start(x₁)]	=	0
[BF]	=	1
[or^#(x₁, x₂)]	=	0
[up]	=	1

together with the usable rules

or(true,b)	→	true	(40)
or(false,b)	→	b	(41)

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

busy^#(B,d,stop,true,b2,b3,i)

→

idle^#(B,open,stop,false,b2,b3,i)

(63)

could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

busy^#(B,closed,down,b1,b2,b3,i)	→	idle^#(B,closed,stop,b1,b2,b3,i)	(44)
busy^#(F,d,stop,b1,true,b3,i)	→	idle^#(F,open,stop,b1,false,b3,i)	(66)
busy^#(F,closed,up,b1,true,b3,i)	→	idle^#(F,closed,stop,b1,true,b3,i)	(52)
busy^#(S,closed,stop,b1,true,false,i)	→	idle^#(S,closed,down,b1,true,false,i)	(54)
busy^#(F,closed,down,b1,false,b3,i)	→	idle^#(BF,closed,down,b1,false,b3,i)	(43)
busy^#(S,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,stop,b1,b2,b3,i)	(61)
busy^#(B,closed,stop,false,true,b3,i)	→	idle^#(B,closed,up,false,true,b3,i)	(64)
busy^#(S,closed,down,b1,b2,false,i)	→	idle^#(FS,closed,down,b1,b2,false,i)	(55)
busy^#(F,closed,stop,true,false,b3,i)	→	idle^#(F,closed,down,true,false,b3,i)	(49)
busy^#(F,closed,down,b1,true,b3,i)	→	idle^#(F,closed,stop,b1,true,b3,i)	(50)
busy^#(BF,closed,up,b1,b2,b3,i)	→	idle^#(F,closed,up,b1,b2,b3,i)	(62)
busy^#(B,closed,stop,false,false,true,i)	→	idle^#(B,closed,up,false,false,true,i)	(69)
busy^#(B,closed,up,true,b2,b3,i)	→	idle^#(B,closed,stop,true,b2,b3,i)	(74)
busy^#(F,closed,up,b1,false,b3,i)	→	idle^#(FS,closed,up,b1,false,b3,i)	(53)
busy^#(FS,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,up,b1,b2,b3,i)	(46)
busy^#(S,open,stop,b1,b2,false,i)	→	idle^#(S,closed,stop,b1,b2,false,i)	(51)
busy^#(FS,closed,down,b1,b2,b3,i)	→	idle^#(F,closed,down,b1,b2,b3,i)	(48)
busy^#(B,open,stop,false,b2,b3,i)	→	idle^#(B,closed,stop,false,b2,b3,i)	(58)
busy^#(S,closed,down,b1,b2,true,i)	→	idle^#(S,closed,stop,b1,b2,true,i)	(47)
busy^#(B,closed,up,false,b2,b3,i)	→	idle^#(BF,closed,up,false,b2,b3,i)	(73)
busy^#(F,open,stop,b1,false,b3,i)	→	idle^#(F,closed,stop,b1,false,b3,i)	(60)
idle^#(fl,d,m,b1,b2,b3,empty)	→	busy^#(fl,d,m,b1,b2,b3,empty)	(75)
busy^#(S,closed,stop,true,false,false,i)	→	idle^#(S,closed,down,true,false,false,i)	(71)
busy^#(F,closed,stop,false,false,true,i)	→	idle^#(F,closed,up,false,false,true,i)	(42)
busy^#(BF,closed,down,b1,b2,b3,i)	→	idle^#(B,closed,down,b1,b2,b3,i)	(72)

1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[stop]	=	1
[newbuttons(x₁,...,x₄)]	=	13508
[S]	=	1
[F]	=	1
[idle^#(x₁,...,x₇)]	=	x₄ + x₅ + x₆ + x₇ + 2
[false]	=	1
[closed]	=	1
[down]	=	1
[incorrect]	=	0
[idle(x₁,...,x₇)]	=	0
[true]	=	4
[correct]	=	0
[B]	=	1
[FS]	=	1
[or(x₁, x₂)]	=	x₂ + 13507
[busy(x₁,...,x₇)]	=	0
[start^#(x₁)]	=	0
[open]	=	1
[busy^#(x₁,...,x₇)]	=	x₄ + x₅ + x₆ + x₇ + 2
[empty]	=	28386
[start(x₁)]	=	0
[BF]	=	1
[or^#(x₁, x₂)]	=	0
[up]	=	1

together with the usable rules

or(true,b)	→	true	(40)
or(false,b)	→	b	(41)

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

busy^#(F,d,stop,b1,true,b3,i)

→

idle^#(F,open,stop,b1,false,b3,i)

(66)

could be deleted.

1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

busy^#(B,closed,down,b1,b2,b3,i)	→	idle^#(B,closed,stop,b1,b2,b3,i)	(44)
busy^#(F,closed,up,b1,true,b3,i)	→	idle^#(F,closed,stop,b1,true,b3,i)	(52)
busy^#(S,closed,stop,b1,true,false,i)	→	idle^#(S,closed,down,b1,true,false,i)	(54)
busy^#(F,closed,down,b1,false,b3,i)	→	idle^#(BF,closed,down,b1,false,b3,i)	(43)
busy^#(S,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,stop,b1,b2,b3,i)	(61)
busy^#(B,closed,stop,false,true,b3,i)	→	idle^#(B,closed,up,false,true,b3,i)	(64)
busy^#(S,closed,down,b1,b2,false,i)	→	idle^#(FS,closed,down,b1,b2,false,i)	(55)
busy^#(F,closed,stop,true,false,b3,i)	→	idle^#(F,closed,down,true,false,b3,i)	(49)
busy^#(F,closed,down,b1,true,b3,i)	→	idle^#(F,closed,stop,b1,true,b3,i)	(50)
busy^#(BF,closed,up,b1,b2,b3,i)	→	idle^#(F,closed,up,b1,b2,b3,i)	(62)
busy^#(B,closed,stop,false,false,true,i)	→	idle^#(B,closed,up,false,false,true,i)	(69)
busy^#(B,closed,up,true,b2,b3,i)	→	idle^#(B,closed,stop,true,b2,b3,i)	(74)
busy^#(F,closed,up,b1,false,b3,i)	→	idle^#(FS,closed,up,b1,false,b3,i)	(53)
busy^#(FS,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,up,b1,b2,b3,i)	(46)
busy^#(S,open,stop,b1,b2,false,i)	→	idle^#(S,closed,stop,b1,b2,false,i)	(51)
busy^#(FS,closed,down,b1,b2,b3,i)	→	idle^#(F,closed,down,b1,b2,b3,i)	(48)
busy^#(B,open,stop,false,b2,b3,i)	→	idle^#(B,closed,stop,false,b2,b3,i)	(58)
busy^#(S,closed,down,b1,b2,true,i)	→	idle^#(S,closed,stop,b1,b2,true,i)	(47)
busy^#(B,closed,up,false,b2,b3,i)	→	idle^#(BF,closed,up,false,b2,b3,i)	(73)
busy^#(F,open,stop,b1,false,b3,i)	→	idle^#(F,closed,stop,b1,false,b3,i)	(60)
idle^#(fl,d,m,b1,b2,b3,empty)	→	busy^#(fl,d,m,b1,b2,b3,empty)	(75)
busy^#(S,closed,stop,true,false,false,i)	→	idle^#(S,closed,down,true,false,false,i)	(71)
busy^#(F,closed,stop,false,false,true,i)	→	idle^#(F,closed,up,false,false,true,i)	(42)
busy^#(BF,closed,down,b1,b2,b3,i)	→	idle^#(B,closed,down,b1,b2,b3,i)	(72)

1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[stop]	=	1
[newbuttons(x₁,...,x₄)]	=	13508
[S]	=	28805
[F]	=	28805
[idle^#(x₁,...,x₇)]	=	x₁ + x₂ + x₆ + x₇ + 2
[false]	=	6617
[closed]	=	19514
[down]	=	1
[incorrect]	=	0
[idle(x₁,...,x₇)]	=	0
[true]	=	12148
[correct]	=	0
[B]	=	28805
[FS]	=	28805
[or(x₁, x₂)]	=	x₂ + 13507
[busy(x₁,...,x₇)]	=	0
[start^#(x₁)]	=	0
[open]	=	19515
[busy^#(x₁,...,x₇)]	=	x₁ + x₂ + x₆ + x₇ + 2
[empty]	=	41745
[start(x₁)]	=	0
[BF]	=	28805
[or^#(x₁, x₂)]	=	0
[up]	=	1

together with the usable rules

or(true,b)	→	true	(40)
or(false,b)	→	b	(41)

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

busy^#(S,open,stop,b1,b2,false,i)	→	idle^#(S,closed,stop,b1,b2,false,i)	(51)
busy^#(B,open,stop,false,b2,b3,i)	→	idle^#(B,closed,stop,false,b2,b3,i)	(58)
busy^#(F,open,stop,b1,false,b3,i)	→	idle^#(F,closed,stop,b1,false,b3,i)	(60)

could be deleted.

1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

busy^#(B,closed,down,b1,b2,b3,i)	→	idle^#(B,closed,stop,b1,b2,b3,i)	(44)
busy^#(F,closed,up,b1,true,b3,i)	→	idle^#(F,closed,stop,b1,true,b3,i)	(52)
busy^#(S,closed,stop,b1,true,false,i)	→	idle^#(S,closed,down,b1,true,false,i)	(54)
busy^#(F,closed,down,b1,false,b3,i)	→	idle^#(BF,closed,down,b1,false,b3,i)	(43)
busy^#(S,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,stop,b1,b2,b3,i)	(61)
busy^#(B,closed,stop,false,true,b3,i)	→	idle^#(B,closed,up,false,true,b3,i)	(64)
busy^#(S,closed,down,b1,b2,false,i)	→	idle^#(FS,closed,down,b1,b2,false,i)	(55)
busy^#(F,closed,stop,true,false,b3,i)	→	idle^#(F,closed,down,true,false,b3,i)	(49)
busy^#(F,closed,down,b1,true,b3,i)	→	idle^#(F,closed,stop,b1,true,b3,i)	(50)
busy^#(BF,closed,up,b1,b2,b3,i)	→	idle^#(F,closed,up,b1,b2,b3,i)	(62)
busy^#(B,closed,stop,false,false,true,i)	→	idle^#(B,closed,up,false,false,true,i)	(69)
busy^#(B,closed,up,true,b2,b3,i)	→	idle^#(B,closed,stop,true,b2,b3,i)	(74)
busy^#(F,closed,up,b1,false,b3,i)	→	idle^#(FS,closed,up,b1,false,b3,i)	(53)
busy^#(FS,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,up,b1,b2,b3,i)	(46)
busy^#(FS,closed,down,b1,b2,b3,i)	→	idle^#(F,closed,down,b1,b2,b3,i)	(48)
busy^#(S,closed,down,b1,b2,true,i)	→	idle^#(S,closed,stop,b1,b2,true,i)	(47)
busy^#(B,closed,up,false,b2,b3,i)	→	idle^#(BF,closed,up,false,b2,b3,i)	(73)
idle^#(fl,d,m,b1,b2,b3,empty)	→	busy^#(fl,d,m,b1,b2,b3,empty)	(75)
busy^#(S,closed,stop,true,false,false,i)	→	idle^#(S,closed,down,true,false,false,i)	(71)
busy^#(F,closed,stop,false,false,true,i)	→	idle^#(F,closed,up,false,false,true,i)	(42)
busy^#(BF,closed,down,b1,b2,b3,i)	→	idle^#(B,closed,down,b1,b2,b3,i)	(72)

1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[stop]	=	43005
[newbuttons(x₁,...,x₄)]	=	max(0)
[S]	=	86013
[F]	=	64508
[idle^#(x₁,...,x₇)]	=	max(x₁ + 15330, x₂ + 26079, x₃ + 36832, x₅ + 26078, x₇ + 26077, 0)
[false]	=	75265
[closed]	=	10750
[down]	=	64510
[incorrect]	=	0
[idle(x₁,...,x₇)]	=	max(0)
[true]	=	0
[correct]	=	0
[B]	=	86013
[FS]	=	86013
[or(x₁, x₂)]	=	max(0)
[busy(x₁,...,x₇)]	=	max(0)
[start^#(x₁)]	=	0
[open]	=	0
[busy^#(x₁,...,x₇)]	=	max(x₁ + 15330, x₂ + 15329, x₃ + 15329, x₅ + 26078, x₇ + 36830, 0)
[empty]	=	2
[start(x₁)]	=	0
[BF]	=	86013
[or^#(x₁, x₂)]	=	max(0)
[up]	=	21501

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

busy^#(F,closed,down,b1,true,b3,i)

→

idle^#(F,closed,stop,b1,true,b3,i)

(50)

could be deleted.

1.1.1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

busy^#(B,closed,down,b1,b2,b3,i)	→	idle^#(B,closed,stop,b1,b2,b3,i)	(44)
busy^#(F,closed,up,b1,true,b3,i)	→	idle^#(F,closed,stop,b1,true,b3,i)	(52)
busy^#(S,closed,stop,b1,true,false,i)	→	idle^#(S,closed,down,b1,true,false,i)	(54)
busy^#(F,closed,down,b1,false,b3,i)	→	idle^#(BF,closed,down,b1,false,b3,i)	(43)
busy^#(S,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,stop,b1,b2,b3,i)	(61)
busy^#(B,closed,stop,false,true,b3,i)	→	idle^#(B,closed,up,false,true,b3,i)	(64)
busy^#(S,closed,down,b1,b2,false,i)	→	idle^#(FS,closed,down,b1,b2,false,i)	(55)
busy^#(F,closed,stop,true,false,b3,i)	→	idle^#(F,closed,down,true,false,b3,i)	(49)
busy^#(BF,closed,up,b1,b2,b3,i)	→	idle^#(F,closed,up,b1,b2,b3,i)	(62)
busy^#(B,closed,stop,false,false,true,i)	→	idle^#(B,closed,up,false,false,true,i)	(69)
busy^#(B,closed,up,true,b2,b3,i)	→	idle^#(B,closed,stop,true,b2,b3,i)	(74)
busy^#(F,closed,up,b1,false,b3,i)	→	idle^#(FS,closed,up,b1,false,b3,i)	(53)
busy^#(FS,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,up,b1,b2,b3,i)	(46)
busy^#(FS,closed,down,b1,b2,b3,i)	→	idle^#(F,closed,down,b1,b2,b3,i)	(48)
busy^#(S,closed,down,b1,b2,true,i)	→	idle^#(S,closed,stop,b1,b2,true,i)	(47)
busy^#(B,closed,up,false,b2,b3,i)	→	idle^#(BF,closed,up,false,b2,b3,i)	(73)
idle^#(fl,d,m,b1,b2,b3,empty)	→	busy^#(fl,d,m,b1,b2,b3,empty)	(75)
busy^#(S,closed,stop,true,false,false,i)	→	idle^#(S,closed,down,true,false,false,i)	(71)
busy^#(F,closed,stop,false,false,true,i)	→	idle^#(F,closed,up,false,false,true,i)	(42)
busy^#(BF,closed,down,b1,b2,b3,i)	→	idle^#(B,closed,down,b1,b2,b3,i)	(72)

1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[stop]	=	3
[newbuttons(x₁,...,x₄)]	=	max(0)
[S]	=	1
[F]	=	4
[idle^#(x₁,...,x₇)]	=	max(x₁ + 56529, x₂ + 31679, x₃ + 24850, x₆ + 56528, x₇ + 24847, 0)
[false]	=	5
[closed]	=	24849
[down]	=	31683
[incorrect]	=	0
[idle(x₁,...,x₇)]	=	max(0)
[true]	=	1
[correct]	=	0
[B]	=	4
[FS]	=	4
[or(x₁, x₂)]	=	max(0)
[busy(x₁,...,x₇)]	=	max(0)
[start^#(x₁)]	=	0
[open]	=	0
[busy^#(x₁,...,x₇)]	=	max(x₁ + 56529, x₂ + 0, x₃ + 24848, x₆ + 56528, x₇ + 24848, 0)
[empty]	=	1
[start(x₁)]	=	0
[BF]	=	4
[or^#(x₁, x₂)]	=	max(0)
[up]	=	0

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

busy^#(S,closed,down,b1,b2,true,i)

→

idle^#(S,closed,stop,b1,b2,true,i)

(47)

could be deleted.

1.1.1.1.1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

busy^#(B,closed,down,b1,b2,b3,i)	→	idle^#(B,closed,stop,b1,b2,b3,i)	(44)
busy^#(F,closed,up,b1,true,b3,i)	→	idle^#(F,closed,stop,b1,true,b3,i)	(52)
busy^#(S,closed,stop,b1,true,false,i)	→	idle^#(S,closed,down,b1,true,false,i)	(54)
busy^#(F,closed,down,b1,false,b3,i)	→	idle^#(BF,closed,down,b1,false,b3,i)	(43)
busy^#(S,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,stop,b1,b2,b3,i)	(61)
busy^#(B,closed,stop,false,true,b3,i)	→	idle^#(B,closed,up,false,true,b3,i)	(64)
busy^#(S,closed,down,b1,b2,false,i)	→	idle^#(FS,closed,down,b1,b2,false,i)	(55)
busy^#(F,closed,stop,true,false,b3,i)	→	idle^#(F,closed,down,true,false,b3,i)	(49)
busy^#(BF,closed,up,b1,b2,b3,i)	→	idle^#(F,closed,up,b1,b2,b3,i)	(62)
busy^#(B,closed,stop,false,false,true,i)	→	idle^#(B,closed,up,false,false,true,i)	(69)
busy^#(B,closed,up,true,b2,b3,i)	→	idle^#(B,closed,stop,true,b2,b3,i)	(74)
busy^#(F,closed,up,b1,false,b3,i)	→	idle^#(FS,closed,up,b1,false,b3,i)	(53)
busy^#(FS,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,up,b1,b2,b3,i)	(46)
busy^#(FS,closed,down,b1,b2,b3,i)	→	idle^#(F,closed,down,b1,b2,b3,i)	(48)
busy^#(B,closed,up,false,b2,b3,i)	→	idle^#(BF,closed,up,false,b2,b3,i)	(73)
idle^#(fl,d,m,b1,b2,b3,empty)	→	busy^#(fl,d,m,b1,b2,b3,empty)	(75)
busy^#(S,closed,stop,true,false,false,i)	→	idle^#(S,closed,down,true,false,false,i)	(71)
busy^#(F,closed,stop,false,false,true,i)	→	idle^#(F,closed,up,false,false,true,i)	(42)
busy^#(BF,closed,down,b1,b2,b3,i)	→	idle^#(B,closed,down,b1,b2,b3,i)	(72)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[stop]	=	8
[newbuttons(x₁,...,x₄)]	=	max(0)
[S]	=	6
[F]	=	4
[idle^#(x₁,...,x₇)]	=	max(x₁ + 22478, x₂ + 22484, x₃ + 22482, x₄ + 22479, 0)
[false]	=	12
[closed]	=	6
[down]	=	8
[incorrect]	=	0
[idle(x₁,...,x₇)]	=	max(0)
[true]	=	0
[correct]	=	0
[B]	=	2
[FS]	=	0
[or(x₁, x₂)]	=	max(0)
[busy(x₁,...,x₇)]	=	max(0)
[start^#(x₁)]	=	0
[open]	=	0
[busy^#(x₁,...,x₇)]	=	max(x₁ + 22476, x₂ + 22479, x₃ + 22482, x₄ + 22479, x₇ + 22483, 0)
[empty]	=	0
[start(x₁)]	=	0
[BF]	=	12
[or^#(x₁, x₂)]	=	max(0)
[up]	=	9

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

busy^#(B,closed,up,true,b2,b3,i)

→

idle^#(B,closed,stop,true,b2,b3,i)

(74)

could be deleted.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

busy^#(B,closed,down,b1,b2,b3,i)	→	idle^#(B,closed,stop,b1,b2,b3,i)	(44)
busy^#(F,closed,up,b1,true,b3,i)	→	idle^#(F,closed,stop,b1,true,b3,i)	(52)
busy^#(S,closed,stop,b1,true,false,i)	→	idle^#(S,closed,down,b1,true,false,i)	(54)
busy^#(F,closed,down,b1,false,b3,i)	→	idle^#(BF,closed,down,b1,false,b3,i)	(43)
busy^#(S,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,stop,b1,b2,b3,i)	(61)
busy^#(B,closed,stop,false,true,b3,i)	→	idle^#(B,closed,up,false,true,b3,i)	(64)
busy^#(S,closed,down,b1,b2,false,i)	→	idle^#(FS,closed,down,b1,b2,false,i)	(55)
busy^#(F,closed,stop,true,false,b3,i)	→	idle^#(F,closed,down,true,false,b3,i)	(49)
busy^#(BF,closed,up,b1,b2,b3,i)	→	idle^#(F,closed,up,b1,b2,b3,i)	(62)
busy^#(B,closed,stop,false,false,true,i)	→	idle^#(B,closed,up,false,false,true,i)	(69)
busy^#(F,closed,up,b1,false,b3,i)	→	idle^#(FS,closed,up,b1,false,b3,i)	(53)
busy^#(FS,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,up,b1,b2,b3,i)	(46)
busy^#(FS,closed,down,b1,b2,b3,i)	→	idle^#(F,closed,down,b1,b2,b3,i)	(48)
busy^#(B,closed,up,false,b2,b3,i)	→	idle^#(BF,closed,up,false,b2,b3,i)	(73)
idle^#(fl,d,m,b1,b2,b3,empty)	→	busy^#(fl,d,m,b1,b2,b3,empty)	(75)
busy^#(S,closed,stop,true,false,false,i)	→	idle^#(S,closed,down,true,false,false,i)	(71)
busy^#(F,closed,stop,false,false,true,i)	→	idle^#(F,closed,up,false,false,true,i)	(42)
busy^#(BF,closed,down,b1,b2,b3,i)	→	idle^#(B,closed,down,b1,b2,b3,i)	(72)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[stop]	=	15
[newbuttons(x₁,...,x₄)]	=	max(0)
[S]	=	10
[F]	=	2
[idle^#(x₁,...,x₇)]	=	max(x₁ + 4, x₂ + 3, x₃ + 2, x₅ + 12, x₆ + 5, x₇ + 1, 0)
[false]	=	8
[closed]	=	13
[down]	=	1
[incorrect]	=	0
[idle(x₁,...,x₇)]	=	max(0)
[true]	=	0
[correct]	=	0
[B]	=	15
[FS]	=	11
[or(x₁, x₂)]	=	max(0)
[busy(x₁,...,x₇)]	=	max(0)
[start^#(x₁)]	=	0
[open]	=	0
[busy^#(x₁,...,x₇)]	=	max(x₁ + 4, x₂ + 3, x₃ + 2, x₅ + 12, x₆ + 5, x₇ + 4, 0)
[empty]	=	2
[start(x₁)]	=	0
[BF]	=	15
[or^#(x₁, x₂)]	=	max(0)
[up]	=	16

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

busy^#(S,closed,stop,b1,true,false,i)

→

idle^#(S,closed,down,b1,true,false,i)

(54)

could be deleted.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

busy^#(B,closed,down,b1,b2,b3,i)	→	idle^#(B,closed,stop,b1,b2,b3,i)	(44)
busy^#(F,closed,up,b1,true,b3,i)	→	idle^#(F,closed,stop,b1,true,b3,i)	(52)
busy^#(F,closed,down,b1,false,b3,i)	→	idle^#(BF,closed,down,b1,false,b3,i)	(43)
busy^#(S,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,stop,b1,b2,b3,i)	(61)
busy^#(B,closed,stop,false,true,b3,i)	→	idle^#(B,closed,up,false,true,b3,i)	(64)
busy^#(S,closed,down,b1,b2,false,i)	→	idle^#(FS,closed,down,b1,b2,false,i)	(55)
busy^#(F,closed,stop,true,false,b3,i)	→	idle^#(F,closed,down,true,false,b3,i)	(49)
busy^#(BF,closed,up,b1,b2,b3,i)	→	idle^#(F,closed,up,b1,b2,b3,i)	(62)
busy^#(B,closed,stop,false,false,true,i)	→	idle^#(B,closed,up,false,false,true,i)	(69)
busy^#(F,closed,up,b1,false,b3,i)	→	idle^#(FS,closed,up,b1,false,b3,i)	(53)
busy^#(FS,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,up,b1,b2,b3,i)	(46)
busy^#(FS,closed,down,b1,b2,b3,i)	→	idle^#(F,closed,down,b1,b2,b3,i)	(48)
busy^#(B,closed,up,false,b2,b3,i)	→	idle^#(BF,closed,up,false,b2,b3,i)	(73)
idle^#(fl,d,m,b1,b2,b3,empty)	→	busy^#(fl,d,m,b1,b2,b3,empty)	(75)
busy^#(S,closed,stop,true,false,false,i)	→	idle^#(S,closed,down,true,false,false,i)	(71)
busy^#(F,closed,stop,false,false,true,i)	→	idle^#(F,closed,up,false,false,true,i)	(42)
busy^#(BF,closed,down,b1,b2,b3,i)	→	idle^#(B,closed,down,b1,b2,b3,i)	(72)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[stop]	=	5
[newbuttons(x₁,...,x₄)]	=	max(0)
[S]	=	0
[F]	=	2
[idle^#(x₁,...,x₇)]	=	max(x₁ + 29943, x₂ + 2, x₃ + 29937, x₄ + 13864, 0)
[false]	=	16076
[closed]	=	29937
[down]	=	10
[incorrect]	=	0
[idle(x₁,...,x₇)]	=	max(0)
[true]	=	16083
[correct]	=	0
[B]	=	4
[FS]	=	1
[or(x₁, x₂)]	=	max(0)
[busy(x₁,...,x₇)]	=	max(0)
[start^#(x₁)]	=	0
[open]	=	0
[busy^#(x₁,...,x₇)]	=	max(x₁ + 29943, x₂ + 1, x₃ + 29937, x₄ + 13864, x₇ + 29941, 0)
[empty]	=	2
[start(x₁)]	=	0
[BF]	=	3
[or^#(x₁, x₂)]	=	max(0)
[up]	=	0

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

busy^#(B,closed,up,false,b2,b3,i)

→

idle^#(BF,closed,up,false,b2,b3,i)

(73)

could be deleted.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

busy^#(B,closed,down,b1,b2,b3,i)	→	idle^#(B,closed,stop,b1,b2,b3,i)	(44)
busy^#(F,closed,up,b1,true,b3,i)	→	idle^#(F,closed,stop,b1,true,b3,i)	(52)
busy^#(F,closed,down,b1,false,b3,i)	→	idle^#(BF,closed,down,b1,false,b3,i)	(43)
busy^#(S,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,stop,b1,b2,b3,i)	(61)
busy^#(B,closed,stop,false,true,b3,i)	→	idle^#(B,closed,up,false,true,b3,i)	(64)
busy^#(S,closed,down,b1,b2,false,i)	→	idle^#(FS,closed,down,b1,b2,false,i)	(55)
busy^#(F,closed,stop,true,false,b3,i)	→	idle^#(F,closed,down,true,false,b3,i)	(49)
busy^#(BF,closed,up,b1,b2,b3,i)	→	idle^#(F,closed,up,b1,b2,b3,i)	(62)
busy^#(B,closed,stop,false,false,true,i)	→	idle^#(B,closed,up,false,false,true,i)	(69)
busy^#(F,closed,up,b1,false,b3,i)	→	idle^#(FS,closed,up,b1,false,b3,i)	(53)
busy^#(FS,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,up,b1,b2,b3,i)	(46)
busy^#(FS,closed,down,b1,b2,b3,i)	→	idle^#(F,closed,down,b1,b2,b3,i)	(48)
idle^#(fl,d,m,b1,b2,b3,empty)	→	busy^#(fl,d,m,b1,b2,b3,empty)	(75)
busy^#(S,closed,stop,true,false,false,i)	→	idle^#(S,closed,down,true,false,false,i)	(71)
busy^#(F,closed,stop,false,false,true,i)	→	idle^#(F,closed,up,false,false,true,i)	(42)
busy^#(BF,closed,down,b1,b2,b3,i)	→	idle^#(B,closed,down,b1,b2,b3,i)	(72)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[stop]	=	1
[newbuttons(x₁,...,x₄)]	=	13508
[S]	=	68692
[F]	=	68692
[idle^#(x₁,...,x₇)]	=	x₁ + x₂ + x₇ + 5
[false]	=	1
[closed]	=	1
[down]	=	1
[incorrect]	=	0
[idle(x₁,...,x₇)]	=	0
[true]	=	1
[correct]	=	0
[B]	=	38797
[FS]	=	68692
[or(x₁, x₂)]	=	0
[busy(x₁,...,x₇)]	=	0
[start^#(x₁)]	=	0
[open]	=	19515
[busy^#(x₁,...,x₇)]	=	x₁ + x₂ + x₇ + 5
[empty]	=	53225
[start(x₁)]	=	0
[BF]	=	68692
[or^#(x₁, x₂)]	=	0
[up]	=	1

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

busy^#(BF,closed,down,b1,b2,b3,i)

→

idle^#(B,closed,down,b1,b2,b3,i)

(72)

could be deleted.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

busy^#(B,closed,down,b1,b2,b3,i)	→	idle^#(B,closed,stop,b1,b2,b3,i)	(44)
busy^#(F,closed,up,b1,true,b3,i)	→	idle^#(F,closed,stop,b1,true,b3,i)	(52)
busy^#(F,closed,down,b1,false,b3,i)	→	idle^#(BF,closed,down,b1,false,b3,i)	(43)
busy^#(S,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,stop,b1,b2,b3,i)	(61)
busy^#(B,closed,stop,false,true,b3,i)	→	idle^#(B,closed,up,false,true,b3,i)	(64)
busy^#(S,closed,down,b1,b2,false,i)	→	idle^#(FS,closed,down,b1,b2,false,i)	(55)
busy^#(F,closed,stop,true,false,b3,i)	→	idle^#(F,closed,down,true,false,b3,i)	(49)
busy^#(BF,closed,up,b1,b2,b3,i)	→	idle^#(F,closed,up,b1,b2,b3,i)	(62)
busy^#(B,closed,stop,false,false,true,i)	→	idle^#(B,closed,up,false,false,true,i)	(69)
busy^#(F,closed,up,b1,false,b3,i)	→	idle^#(FS,closed,up,b1,false,b3,i)	(53)
busy^#(FS,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,up,b1,b2,b3,i)	(46)
busy^#(FS,closed,down,b1,b2,b3,i)	→	idle^#(F,closed,down,b1,b2,b3,i)	(48)
idle^#(fl,d,m,b1,b2,b3,empty)	→	busy^#(fl,d,m,b1,b2,b3,empty)	(75)
busy^#(S,closed,stop,true,false,false,i)	→	idle^#(S,closed,down,true,false,false,i)	(71)
busy^#(F,closed,stop,false,false,true,i)	→	idle^#(F,closed,up,false,false,true,i)	(42)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[stop]	=	15
[newbuttons(x₁,...,x₄)]	=	max(0)
[S]	=	15
[F]	=	3
[idle^#(x₁,...,x₇)]	=	max(x₁ + 24128, x₂ + 24127, x₃ + 24129, x₄ + 24142, x₅ + 24132, x₇ + 24130, 0)
[false]	=	5
[closed]	=	15
[down]	=	0
[incorrect]	=	0
[idle(x₁,...,x₇)]	=	max(0)
[true]	=	0
[correct]	=	0
[B]	=	18
[FS]	=	11
[or(x₁, x₂)]	=	max(0)
[busy(x₁,...,x₇)]	=	max(0)
[start^#(x₁)]	=	0
[open]	=	0
[busy^#(x₁,...,x₇)]	=	max(x₁ + 24128, x₂ + 24123, x₃ + 24129, x₄ + 24142, x₅ + 24132, x₇ + 24140, 0)
[empty]	=	2
[start(x₁)]	=	0
[BF]	=	0
[or^#(x₁, x₂)]	=	max(0)
[up]	=	16

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

busy^#(F,closed,stop,true,false,b3,i)	→	idle^#(F,closed,down,true,false,b3,i)	(49)
busy^#(S,closed,stop,true,false,false,i)	→	idle^#(S,closed,down,true,false,false,i)	(71)

could be deleted.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

busy^#(B,closed,down,b1,b2,b3,i)	→	idle^#(B,closed,stop,b1,b2,b3,i)	(44)
busy^#(F,closed,up,b1,true,b3,i)	→	idle^#(F,closed,stop,b1,true,b3,i)	(52)
busy^#(F,closed,down,b1,false,b3,i)	→	idle^#(BF,closed,down,b1,false,b3,i)	(43)
busy^#(S,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,stop,b1,b2,b3,i)	(61)
busy^#(B,closed,stop,false,true,b3,i)	→	idle^#(B,closed,up,false,true,b3,i)	(64)
busy^#(S,closed,down,b1,b2,false,i)	→	idle^#(FS,closed,down,b1,b2,false,i)	(55)
busy^#(BF,closed,up,b1,b2,b3,i)	→	idle^#(F,closed,up,b1,b2,b3,i)	(62)
busy^#(B,closed,stop,false,false,true,i)	→	idle^#(B,closed,up,false,false,true,i)	(69)
busy^#(F,closed,up,b1,false,b3,i)	→	idle^#(FS,closed,up,b1,false,b3,i)	(53)
busy^#(FS,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,up,b1,b2,b3,i)	(46)
busy^#(FS,closed,down,b1,b2,b3,i)	→	idle^#(F,closed,down,b1,b2,b3,i)	(48)
idle^#(fl,d,m,b1,b2,b3,empty)	→	busy^#(fl,d,m,b1,b2,b3,empty)	(75)
busy^#(F,closed,stop,false,false,true,i)	→	idle^#(F,closed,up,false,false,true,i)	(42)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[stop]	=	0
[newbuttons(x₁,...,x₄)]	=	13508
[S]	=	1
[F]	=	1
[idle^#(x₁,...,x₇)]	=	x₃ + x₄ + x₅ + 1
[false]	=	1
[closed]	=	1
[down]	=	36617
[incorrect]	=	0
[idle(x₁,...,x₇)]	=	0
[true]	=	1
[correct]	=	0
[B]	=	1
[FS]	=	1
[or(x₁, x₂)]	=	x₁ + x₂ + 0
[busy(x₁,...,x₇)]	=	0
[start^#(x₁)]	=	0
[open]	=	19515
[busy^#(x₁,...,x₇)]	=	x₃ + x₄ + x₅ + 1
[empty]	=	1
[start(x₁)]	=	0
[BF]	=	1
[or^#(x₁, x₂)]	=	0
[up]	=	0

together with the usable rules

or(true,b)	→	true	(40)
or(false,b)	→	b	(41)

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

busy^#(B,closed,down,b1,b2,b3,i)

→

idle^#(B,closed,stop,b1,b2,b3,i)

(44)

could be deleted.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

busy^#(F,closed,up,b1,true,b3,i)	→	idle^#(F,closed,stop,b1,true,b3,i)	(52)
busy^#(F,closed,down,b1,false,b3,i)	→	idle^#(BF,closed,down,b1,false,b3,i)	(43)
busy^#(S,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,stop,b1,b2,b3,i)	(61)
busy^#(B,closed,stop,false,true,b3,i)	→	idle^#(B,closed,up,false,true,b3,i)	(64)
busy^#(S,closed,down,b1,b2,false,i)	→	idle^#(FS,closed,down,b1,b2,false,i)	(55)
busy^#(BF,closed,up,b1,b2,b3,i)	→	idle^#(F,closed,up,b1,b2,b3,i)	(62)
busy^#(B,closed,stop,false,false,true,i)	→	idle^#(B,closed,up,false,false,true,i)	(69)
busy^#(F,closed,up,b1,false,b3,i)	→	idle^#(FS,closed,up,b1,false,b3,i)	(53)
busy^#(FS,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,up,b1,b2,b3,i)	(46)
busy^#(FS,closed,down,b1,b2,b3,i)	→	idle^#(F,closed,down,b1,b2,b3,i)	(48)
idle^#(fl,d,m,b1,b2,b3,empty)	→	busy^#(fl,d,m,b1,b2,b3,empty)	(75)
busy^#(F,closed,stop,false,false,true,i)	→	idle^#(F,closed,up,false,false,true,i)	(42)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[stop]	=	5
[newbuttons(x₁,...,x₄)]	=	max(0)
[S]	=	8
[F]	=	8
[idle^#(x₁,...,x₇)]	=	max(x₁ + 32664, x₂ + 32665, x₃ + 32667, x₅ + 32668, x₆ + 32666, 0)
[false]	=	0
[closed]	=	0
[down]	=	0
[incorrect]	=	0
[idle(x₁,...,x₇)]	=	max(0)
[true]	=	3
[correct]	=	0
[B]	=	6
[FS]	=	8
[or(x₁, x₂)]	=	max(0)
[busy(x₁,...,x₇)]	=	max(0)
[start^#(x₁)]	=	0
[open]	=	0
[busy^#(x₁,...,x₇)]	=	max(x₁ + 32664, x₃ + 32667, x₅ + 32668, x₆ + 32666, 0)
[empty]	=	0
[start(x₁)]	=	0
[BF]	=	8
[or^#(x₁, x₂)]	=	max(0)
[up]	=	0

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

busy^#(B,closed,stop,false,false,true,i)

→

idle^#(B,closed,up,false,false,true,i)

(69)

could be deleted.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

busy^#(F,closed,up,b1,true,b3,i)	→	idle^#(F,closed,stop,b1,true,b3,i)	(52)
busy^#(F,closed,down,b1,false,b3,i)	→	idle^#(BF,closed,down,b1,false,b3,i)	(43)
busy^#(S,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,stop,b1,b2,b3,i)	(61)
busy^#(B,closed,stop,false,true,b3,i)	→	idle^#(B,closed,up,false,true,b3,i)	(64)
busy^#(S,closed,down,b1,b2,false,i)	→	idle^#(FS,closed,down,b1,b2,false,i)	(55)
busy^#(BF,closed,up,b1,b2,b3,i)	→	idle^#(F,closed,up,b1,b2,b3,i)	(62)
busy^#(F,closed,up,b1,false,b3,i)	→	idle^#(FS,closed,up,b1,false,b3,i)	(53)
busy^#(FS,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,up,b1,b2,b3,i)	(46)
busy^#(FS,closed,down,b1,b2,b3,i)	→	idle^#(F,closed,down,b1,b2,b3,i)	(48)
idle^#(fl,d,m,b1,b2,b3,empty)	→	busy^#(fl,d,m,b1,b2,b3,empty)	(75)
busy^#(F,closed,stop,false,false,true,i)	→	idle^#(F,closed,up,false,false,true,i)	(42)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[stop]	=	72633
[newbuttons(x₁,...,x₄)]	=	max(0)
[S]	=	105006
[F]	=	105006
[idle^#(x₁,...,x₇)]	=	max(x₁ + 0, x₂ + 1, x₃ + 32372, x₄ + 64749, x₅ + 32371, x₇ + 7877, 0)
[false]	=	7883
[closed]	=	40251
[down]	=	40253
[incorrect]	=	0
[idle(x₁,...,x₇)]	=	max(0)
[true]	=	7878
[correct]	=	0
[B]	=	40250
[FS]	=	105006
[or(x₁, x₂)]	=	max(0)
[busy(x₁,...,x₇)]	=	max(0)
[start^#(x₁)]	=	0
[open]	=	0
[busy^#(x₁,...,x₇)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, x₄ + 64749, x₅ + 32371, x₇ + 40255, 0)
[empty]	=	24493
[start(x₁)]	=	0
[BF]	=	105006
[or^#(x₁, x₂)]	=	max(0)
[up]	=	7876

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

busy^#(B,closed,stop,false,true,b3,i)

→

idle^#(B,closed,up,false,true,b3,i)

(64)

could be deleted.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

busy^#(F,closed,up,b1,true,b3,i)	→	idle^#(F,closed,stop,b1,true,b3,i)	(52)
busy^#(F,closed,down,b1,false,b3,i)	→	idle^#(BF,closed,down,b1,false,b3,i)	(43)
busy^#(S,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,stop,b1,b2,b3,i)	(61)
busy^#(S,closed,down,b1,b2,false,i)	→	idle^#(FS,closed,down,b1,b2,false,i)	(55)
busy^#(BF,closed,up,b1,b2,b3,i)	→	idle^#(F,closed,up,b1,b2,b3,i)	(62)
busy^#(F,closed,up,b1,false,b3,i)	→	idle^#(FS,closed,up,b1,false,b3,i)	(53)
busy^#(FS,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,up,b1,b2,b3,i)	(46)
busy^#(FS,closed,down,b1,b2,b3,i)	→	idle^#(F,closed,down,b1,b2,b3,i)	(48)
idle^#(fl,d,m,b1,b2,b3,empty)	→	busy^#(fl,d,m,b1,b2,b3,empty)	(75)
busy^#(F,closed,stop,false,false,true,i)	→	idle^#(F,closed,up,false,false,true,i)	(42)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[stop]	=	9
[newbuttons(x₁,...,x₄)]	=	max(0)
[S]	=	6
[F]	=	0
[idle^#(x₁,...,x₇)]	=	max(x₁ + 4, x₂ + 8, x₃ + 3, 0)
[false]	=	7883
[closed]	=	0
[down]	=	13
[incorrect]	=	0
[idle(x₁,...,x₇)]	=	max(0)
[true]	=	7878
[correct]	=	0
[B]	=	40250
[FS]	=	8
[or(x₁, x₂)]	=	max(0)
[busy(x₁,...,x₇)]	=	max(0)
[start^#(x₁)]	=	0
[open]	=	0
[busy^#(x₁,...,x₇)]	=	max(x₁ + 1, x₂ + 6, x₃ + 3, x₇ + 7, 0)
[empty]	=	1
[start(x₁)]	=	0
[BF]	=	12
[or^#(x₁, x₂)]	=	max(0)
[up]	=	9

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

busy^#(BF,closed,up,b1,b2,b3,i)

→

idle^#(F,closed,up,b1,b2,b3,i)

(62)

could be deleted.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

busy^#(F,closed,up,b1,true,b3,i)	→	idle^#(F,closed,stop,b1,true,b3,i)	(52)
busy^#(F,closed,down,b1,false,b3,i)	→	idle^#(BF,closed,down,b1,false,b3,i)	(43)
busy^#(S,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,stop,b1,b2,b3,i)	(61)
busy^#(S,closed,down,b1,b2,false,i)	→	idle^#(FS,closed,down,b1,b2,false,i)	(55)
busy^#(F,closed,up,b1,false,b3,i)	→	idle^#(FS,closed,up,b1,false,b3,i)	(53)
busy^#(FS,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,up,b1,b2,b3,i)	(46)
busy^#(FS,closed,down,b1,b2,b3,i)	→	idle^#(F,closed,down,b1,b2,b3,i)	(48)
idle^#(fl,d,m,b1,b2,b3,empty)	→	busy^#(fl,d,m,b1,b2,b3,empty)	(75)
busy^#(F,closed,stop,false,false,true,i)	→	idle^#(F,closed,up,false,false,true,i)	(42)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[stop]	=	12016
[newbuttons(x₁,...,x₄)]	=	13508
[S]	=	41973
[F]	=	41973
[idle^#(x₁,...,x₇)]	=	x₁ + x₃ + x₇ + 0
[false]	=	1
[closed]	=	1
[down]	=	33957
[incorrect]	=	0
[idle(x₁,...,x₇)]	=	0
[true]	=	1
[correct]	=	0
[B]	=	0
[FS]	=	41973
[or(x₁, x₂)]	=	0
[busy(x₁,...,x₇)]	=	0
[start^#(x₁)]	=	0
[open]	=	19515
[busy^#(x₁,...,x₇)]	=	x₁ + x₃ + x₇ + 0
[empty]	=	20377
[start(x₁)]	=	0
[BF]	=	22266
[or^#(x₁, x₂)]	=	0
[up]	=	12016

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

busy^#(F,closed,down,b1,false,b3,i)

→

idle^#(BF,closed,down,b1,false,b3,i)

(43)

could be deleted.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

busy^#(F,closed,up,b1,true,b3,i)	→	idle^#(F,closed,stop,b1,true,b3,i)	(52)
busy^#(S,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,stop,b1,b2,b3,i)	(61)
busy^#(S,closed,down,b1,b2,false,i)	→	idle^#(FS,closed,down,b1,b2,false,i)	(55)
busy^#(F,closed,up,b1,false,b3,i)	→	idle^#(FS,closed,up,b1,false,b3,i)	(53)
busy^#(FS,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,up,b1,b2,b3,i)	(46)
busy^#(FS,closed,down,b1,b2,b3,i)	→	idle^#(F,closed,down,b1,b2,b3,i)	(48)
idle^#(fl,d,m,b1,b2,b3,empty)	→	busy^#(fl,d,m,b1,b2,b3,empty)	(75)
busy^#(F,closed,stop,false,false,true,i)	→	idle^#(F,closed,up,false,false,true,i)	(42)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[stop]	=	23118
[newbuttons(x₁,...,x₄)]	=	max(0)
[S]	=	3
[F]	=	23119
[idle^#(x₁,...,x₇)]	=	max(x₁ + 23108, x₂ + 40344, x₃ + 23107, x₅ + 23109, x₇ + 0, 0)
[false]	=	0
[closed]	=	5880
[down]	=	23121
[incorrect]	=	0
[idle(x₁,...,x₇)]	=	max(0)
[true]	=	0
[correct]	=	0
[B]	=	40250
[FS]	=	4
[or(x₁, x₂)]	=	max(0)
[busy(x₁,...,x₇)]	=	max(0)
[start^#(x₁)]	=	0
[open]	=	0
[busy^#(x₁,...,x₇)]	=	max(x₁ + 23108, x₂ + 17233, x₃ + 23107, x₅ + 23109, x₇ + 23110, 0)
[empty]	=	17233
[start(x₁)]	=	0
[BF]	=	12
[or^#(x₁, x₂)]	=	max(0)
[up]	=	23119

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

busy^#(F,closed,up,b1,false,b3,i)

→

idle^#(FS,closed,up,b1,false,b3,i)

(53)

could be deleted.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

busy^#(F,closed,up,b1,true,b3,i)	→	idle^#(F,closed,stop,b1,true,b3,i)	(52)
busy^#(S,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,stop,b1,b2,b3,i)	(61)
busy^#(S,closed,down,b1,b2,false,i)	→	idle^#(FS,closed,down,b1,b2,false,i)	(55)
busy^#(FS,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,up,b1,b2,b3,i)	(46)
busy^#(FS,closed,down,b1,b2,b3,i)	→	idle^#(F,closed,down,b1,b2,b3,i)	(48)
idle^#(fl,d,m,b1,b2,b3,empty)	→	busy^#(fl,d,m,b1,b2,b3,empty)	(75)
busy^#(F,closed,stop,false,false,true,i)	→	idle^#(F,closed,up,false,false,true,i)	(42)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[stop]	=	17908
[newbuttons(x₁,...,x₄)]	=	13508
[S]	=	19516
[F]	=	19515
[idle^#(x₁,...,x₇)]	=	x₁ + x₂ + x₃ + x₇ + 0
[false]	=	2
[closed]	=	1
[down]	=	17778
[incorrect]	=	0
[idle(x₁,...,x₇)]	=	0
[true]	=	1
[correct]	=	0
[B]	=	0
[FS]	=	19516
[or(x₁, x₂)]	=	0
[busy(x₁,...,x₇)]	=	0
[start^#(x₁)]	=	0
[open]	=	19515
[busy^#(x₁,...,x₇)]	=	x₁ + x₂ + x₃ + x₇ + 0
[empty]	=	1
[start(x₁)]	=	0
[BF]	=	22266
[or^#(x₁, x₂)]	=	0
[up]	=	17908

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

busy^#(FS,closed,down,b1,b2,b3,i)

→

idle^#(F,closed,down,b1,b2,b3,i)

(48)

could be deleted.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

busy^#(F,closed,up,b1,true,b3,i)	→	idle^#(F,closed,stop,b1,true,b3,i)	(52)
busy^#(S,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,stop,b1,b2,b3,i)	(61)
busy^#(S,closed,down,b1,b2,false,i)	→	idle^#(FS,closed,down,b1,b2,false,i)	(55)
busy^#(FS,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,up,b1,b2,b3,i)	(46)
idle^#(fl,d,m,b1,b2,b3,empty)	→	busy^#(fl,d,m,b1,b2,b3,empty)	(75)
busy^#(F,closed,stop,false,false,true,i)	→	idle^#(F,closed,up,false,false,true,i)	(42)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[stop]	=	30271
[newbuttons(x₁,...,x₄)]	=	max(0)
[S]	=	60540
[F]	=	0
[idle^#(x₁,...,x₇)]	=	max(x₁ + 2, x₂ + 4, x₃ + 30271, x₅ + 1, 0)
[false]	=	0
[closed]	=	0
[down]	=	30271
[incorrect]	=	0
[idle(x₁,...,x₇)]	=	max(0)
[true]	=	60542
[correct]	=	0
[B]	=	40250
[FS]	=	60540
[or(x₁, x₂)]	=	max(0)
[busy(x₁,...,x₇)]	=	max(0)
[start^#(x₁)]	=	0
[open]	=	0
[busy^#(x₁,...,x₇)]	=	max(x₁ + 2, x₂ + 3, x₃ + 2, x₅ + 1, x₇ + 30271, 0)
[empty]	=	0
[start(x₁)]	=	0
[BF]	=	12
[or^#(x₁, x₂)]	=	max(0)
[up]	=	1

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

busy^#(F,closed,stop,false,false,true,i)

→

idle^#(F,closed,up,false,false,true,i)

(42)

could be deleted.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

busy^#(F,closed,up,b1,true,b3,i)	→	idle^#(F,closed,stop,b1,true,b3,i)	(52)
busy^#(S,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,stop,b1,b2,b3,i)	(61)
busy^#(S,closed,down,b1,b2,false,i)	→	idle^#(FS,closed,down,b1,b2,false,i)	(55)
busy^#(FS,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,up,b1,b2,b3,i)	(46)
idle^#(fl,d,m,b1,b2,b3,empty)	→	busy^#(fl,d,m,b1,b2,b3,empty)	(75)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[stop]	=	1
[newbuttons(x₁,...,x₄)]	=	13508
[S]	=	1
[F]	=	1
[idle^#(x₁,...,x₇)]	=	x₃ + x₇ + 0
[false]	=	16831
[closed]	=	1
[down]	=	24852
[incorrect]	=	0
[idle(x₁,...,x₇)]	=	0
[true]	=	19825
[correct]	=	0
[B]	=	0
[FS]	=	1
[or(x₁, x₂)]	=	x₁ + 0
[busy(x₁,...,x₇)]	=	0
[start^#(x₁)]	=	0
[open]	=	19515
[busy^#(x₁,...,x₇)]	=	x₃ + x₇ + 0
[empty]	=	15146
[start(x₁)]	=	0
[BF]	=	22266
[or^#(x₁, x₂)]	=	0
[up]	=	2

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

busy^#(F,closed,up,b1,true,b3,i)	→	idle^#(F,closed,stop,b1,true,b3,i)	(52)
busy^#(S,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,stop,b1,b2,b3,i)	(61)

could be deleted.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

busy^#(S,closed,down,b1,b2,false,i)	→	idle^#(FS,closed,down,b1,b2,false,i)	(55)
busy^#(FS,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,up,b1,b2,b3,i)	(46)
idle^#(fl,d,m,b1,b2,b3,empty)	→	busy^#(fl,d,m,b1,b2,b3,empty)	(75)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[stop]	=	30271
[newbuttons(x₁,...,x₄)]	=	max(0)
[S]	=	7
[F]	=	0
[idle^#(x₁,...,x₇)]	=	max(x₁ + 17538, x₂ + 17536, x₃ + 17541, x₆ + 17534, 0)
[false]	=	9
[closed]	=	4
[down]	=	1
[incorrect]	=	0
[idle(x₁,...,x₇)]	=	max(0)
[true]	=	60542
[correct]	=	0
[B]	=	40250
[FS]	=	0
[or(x₁, x₂)]	=	max(0)
[busy(x₁,...,x₇)]	=	max(0)
[start^#(x₁)]	=	0
[open]	=	0
[busy^#(x₁,...,x₇)]	=	max(x₁ + 17537, x₂ + 17535, x₃ + 17541, x₆ + 17534, x₇ + 17541, 0)
[empty]	=	0
[start(x₁)]	=	0
[BF]	=	12
[or^#(x₁, x₂)]	=	max(0)
[up]	=	5

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

busy^#(S,closed,down,b1,b2,false,i)

→

idle^#(FS,closed,down,b1,b2,false,i)

(55)

could be deleted.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

busy^#(FS,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,up,b1,b2,b3,i)	(46)
idle^#(fl,d,m,b1,b2,b3,empty)	→	busy^#(fl,d,m,b1,b2,b3,empty)	(75)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[stop]	=	1
[newbuttons(x₁,...,x₄)]	=	13508
[S]	=	1
[F]	=	1
[idle^#(x₁,...,x₇)]	=	x₁ + x₇ + 1
[false]	=	16831
[closed]	=	1
[down]	=	1
[incorrect]	=	0
[idle(x₁,...,x₇)]	=	0
[true]	=	19825
[correct]	=	0
[B]	=	0
[FS]	=	3
[or(x₁, x₂)]	=	x₁ + 0
[busy(x₁,...,x₇)]	=	0
[start^#(x₁)]	=	0
[open]	=	19515
[busy^#(x₁,...,x₇)]	=	x₁ + x₇ + 0
[empty]	=	29846
[start(x₁)]	=	0
[BF]	=	22266
[or^#(x₁, x₂)]	=	0
[up]	=	1

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

busy^#(FS,closed,up,b1,b2,b3,i)	→	idle^#(S,closed,up,b1,b2,b3,i)	(46)
idle^#(fl,d,m,b1,b2,b3,empty)	→	busy^#(fl,d,m,b1,b2,b3,empty)	(75)

could be deleted.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.