YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

a(a(b(b(x0))))	→	C(C(x0))
b(b(c(c(x0))))	→	A(A(x0))
c(c(a(a(x0))))	→	B(B(x0))
A(A(C(C(x0))))	→	b(b(x0))
C(C(B(B(x0))))	→	a(a(x0))
B(B(A(A(x0))))	→	c(c(x0))
a(a(a(a(a(a(a(a(a(a(x0))))))))))	→	A(A(A(A(A(A(x0))))))
A(A(A(A(A(A(A(A(x0))))))))	→	a(a(a(a(a(a(a(a(x0))))))))
b(b(b(b(b(b(b(b(b(b(x0))))))))))	→	B(B(B(B(B(B(x0))))))
B(B(B(B(B(B(B(B(x0))))))))	→	b(b(b(b(b(b(b(b(x0))))))))
c(c(c(c(c(c(c(c(c(c(x0))))))))))	→	C(C(C(C(C(C(x0))))))
C(C(C(C(C(C(C(C(x0))))))))	→	c(c(c(c(c(c(c(c(x0))))))))
B(B(a(a(a(a(a(a(a(a(x0))))))))))	→	c(c(A(A(A(A(A(A(x0))))))))
A(A(A(A(A(A(b(b(x0))))))))	→	a(a(a(a(a(a(a(a(C(C(x0))))))))))
C(C(b(b(b(b(b(b(b(b(x0))))))))))	→	a(a(B(B(B(B(B(B(x0))))))))
B(B(B(B(B(B(c(c(x0))))))))	→	b(b(b(b(b(b(b(b(A(A(x0))))))))))
A(A(c(c(c(c(c(c(c(c(x0))))))))))	→	b(b(C(C(C(C(C(C(x0))))))))
C(C(C(C(C(C(a(a(x0))))))))	→	c(c(c(c(c(c(c(c(B(B(x0))))))))))
a(a(A(A(x0))))	→	x0
A(A(a(a(x0))))	→	x0
b(b(B(B(x0))))	→	x0
B(B(b(b(x0))))	→	x0
c(c(C(C(x0))))	→	x0
C(C(c(c(x0))))	→	x0

Proof

1 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers

[A(x₁)]	=	3 · x₁ + -∞
[a(x₁)]	=	2 · x₁ + -∞
[c(x₁)]	=	2 · x₁ + -∞
[B(x₁)]	=	3 · x₁ + -∞
[b(x₁)]	=	2 · x₁ + -∞
[C(x₁)]	=	3 · x₁ + -∞

the rules

B(B(a(a(a(a(a(a(a(a(x0))))))))))	→	c(c(A(A(A(A(A(A(x0))))))))
A(A(A(A(A(A(b(b(x0))))))))	→	a(a(a(a(a(a(a(a(C(C(x0))))))))))
C(C(b(b(b(b(b(b(b(b(x0))))))))))	→	a(a(B(B(B(B(B(B(x0))))))))
B(B(B(B(B(B(c(c(x0))))))))	→	b(b(b(b(b(b(b(b(A(A(x0))))))))))
A(A(c(c(c(c(c(c(c(c(x0))))))))))	→	b(b(C(C(C(C(C(C(x0))))))))
C(C(C(C(C(C(a(a(x0))))))))	→	c(c(c(c(c(c(c(c(B(B(x0))))))))))

remain.

1.1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS

a(a(a(a(a(a(a(a(B(B(x0))))))))))	→	A(A(A(A(A(A(c(c(x0))))))))
b(b(A(A(A(A(A(A(x0))))))))	→	C(C(a(a(a(a(a(a(a(a(x0))))))))))
b(b(b(b(b(b(b(b(C(C(x0))))))))))	→	B(B(B(B(B(B(a(a(x0))))))))
c(c(B(B(B(B(B(B(x0))))))))	→	A(A(b(b(b(b(b(b(b(b(x0))))))))))
c(c(c(c(c(c(c(c(A(A(x0))))))))))	→	C(C(C(C(C(C(b(b(x0))))))))
a(a(C(C(C(C(C(C(x0))))))))	→	B(B(c(c(c(c(c(c(c(c(x0))))))))))

1.1.1 Bounds

The given TRS is match-bounded by 0. This is shown by the following automaton.

final states:

{42, 36, 26, 20, 10, 1}

transitions:

10 → 28

10 → 27

20 → 34

20 → 33

20 → 32

20 → 31

20 → 30

20 → 29

20 → 28

20 → 27

1 → 18

1 → 17

1 → 16

1 → 15

1 → 14

1 → 13

1 → 12

1 → 11

26 → 4

26 → 3

36 → 48

36 → 47

36 → 46

36 → 45

36 → 44

36 → 43

36 → 4

36 → 3

42 → 12

42 → 11

f6₀ → 2

b₀(31) → 32

b₀(32) → 33

b₀(2) → 27

b₀(30) → 31

b₀(27) → 28

b₀(28) → 29

b₀(29) → 30

b₀(33) → 34

c₀(45) → 46

c₀(43) → 44

c₀(46) → 47

c₀(3) → 4

c₀(47) → 48

c₀(2) → 3

c₀(4) → 43

c₀(44) → 45

C₀(19) → 10

C₀(37) → 38

C₀(41) → 36

C₀(18) → 19

C₀(39) → 40

C₀(28) → 37

C₀(40) → 41

C₀(38) → 39

a₀(2) → 11

a₀(16) → 17

a₀(12) → 13

a₀(11) → 12

a₀(14) → 15

a₀(13) → 14

a₀(17) → 18

a₀(15) → 16

A₀(9) → 1

A₀(4) → 5

A₀(8) → 9

A₀(6) → 7

A₀(7) → 8

A₀(35) → 26

A₀(34) → 35

A₀(5) → 6

B₀(25) → 20

B₀(21) → 22

B₀(22) → 23

B₀(49) → 42

B₀(48) → 49

B₀(24) → 25

B₀(23) → 24

B₀(12) → 21

10	→	28
10	→	27
20	→	34
20	→	33
20	→	32
20	→	31
20	→	30
20	→	29
20	→	28
20	→	27
1	→	18
1	→	17
1	→	16
1	→	15
1	→	14
1	→	13
1	→	12
1	→	11
26	→	4
26	→	3
36	→	48
36	→	47
36	→	46
36	→	45
36	→	44
36	→	43
36	→	4
36	→	3
42	→	12
42	→	11
f6₀	→	2
b₀(31)	→	32
b₀(32)	→	33
b₀(2)	→	27
b₀(30)	→	31
b₀(27)	→	28
b₀(28)	→	29
b₀(29)	→	30
b₀(33)	→	34
c₀(45)	→	46
c₀(43)	→	44
c₀(46)	→	47
c₀(3)	→	4
c₀(47)	→	48
c₀(2)	→	3
c₀(4)	→	43
c₀(44)	→	45
C₀(19)	→	10
C₀(37)	→	38
C₀(41)	→	36
C₀(18)	→	19
C₀(39)	→	40
C₀(28)	→	37
C₀(40)	→	41
C₀(38)	→	39
a₀(2)	→	11
a₀(16)	→	17
a₀(12)	→	13
a₀(11)	→	12
a₀(14)	→	15
a₀(13)	→	14
a₀(17)	→	18
a₀(15)	→	16
A₀(9)	→	1
A₀(4)	→	5
A₀(8)	→	9
A₀(6)	→	7
A₀(7)	→	8
A₀(35)	→	26
A₀(34)	→	35
A₀(5)	→	6
B₀(25)	→	20
B₀(21)	→	22
B₀(22)	→	23
B₀(49)	→	42
B₀(48)	→	49
B₀(24)	→	25
B₀(23)	→	24
B₀(12)	→	21