YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

0(0(1(0(2(x0)))))	→	0(0(1(2(2(x0)))))
0(0(1(0(2(x0)))))	→	0(0(2(1(2(x0)))))
0(0(1(0(2(x0)))))	→	0(1(0(2(2(x0)))))
0(0(1(0(2(x0)))))	→	0(1(1(2(2(x0)))))
0(0(1(0(2(x0)))))	→	0(1(2(0(2(x0)))))
0(0(1(0(2(x0)))))	→	0(1(2(2(0(x0)))))
0(0(1(0(2(x0)))))	→	0(1(2(2(2(x0)))))
0(0(1(0(2(x0)))))	→	0(2(1(0(2(x0)))))
0(0(1(0(2(x0)))))	→	0(2(1(2(2(x0)))))
0(0(1(0(2(x0)))))	→	0(2(2(1(0(x0)))))
0(0(1(0(2(x0)))))	→	0(2(2(1(2(x0)))))
0(0(1(0(2(x0)))))	→	1(0(0(2(2(x0)))))
0(0(1(0(2(x0)))))	→	1(0(2(0(2(x0)))))
0(0(1(0(2(x0)))))	→	1(0(2(2(0(x0)))))
0(0(1(0(2(x0)))))	→	1(0(2(2(2(x0)))))
0(0(1(0(2(x0)))))	→	1(1(0(2(2(x0)))))
0(0(1(0(2(x0)))))	→	1(2(0(2(2(x0)))))
0(0(1(0(2(x0)))))	→	1(2(1(0(2(x0)))))
0(0(1(0(2(x0)))))	→	1(2(2(0(2(x0)))))
0(0(1(0(2(x0)))))	→	1(2(2(2(0(x0)))))
0(0(1(0(2(x0)))))	→	2(1(0(2(2(x0)))))
0(0(1(0(2(x0)))))	→	2(2(1(0(2(x0)))))
0(0(1(0(2(x0)))))	→	2(2(2(1(0(x0)))))
0(1(2(0(2(x0)))))	→	0(1(0(2(2(x0)))))
0(1(2(0(2(x0)))))	→	0(1(1(2(2(x0)))))
0(1(2(0(2(x0)))))	→	0(1(2(2(2(x0)))))
0(1(2(0(2(x0)))))	→	0(2(1(0(2(x0)))))
0(1(2(0(2(x0)))))	→	0(2(1(2(2(x0)))))
0(1(2(0(2(x0)))))	→	0(2(2(1(0(x0)))))
0(1(2(0(2(x0)))))	→	0(2(2(1(2(x0)))))
0(1(2(0(2(x0)))))	→	1(0(2(2(2(x0)))))
0(1(2(0(2(x0)))))	→	1(2(0(2(2(x0)))))
0(1(2(0(2(x0)))))	→	1(2(2(0(2(x0)))))
0(1(2(0(2(x0)))))	→	1(2(2(2(0(x0)))))
1(0(1(0(2(x0)))))	→	0(1(2(2(2(x0)))))
1(0(1(0(2(x0)))))	→	0(2(1(2(2(x0)))))
1(0(1(0(2(x0)))))	→	1(0(0(2(2(x0)))))
1(0(1(0(2(x0)))))	→	1(0(1(2(2(x0)))))
1(0(1(0(2(x0)))))	→	1(0(2(0(2(x0)))))
1(0(1(0(2(x0)))))	→	1(0(2(1(2(x0)))))
1(0(1(0(2(x0)))))	→	1(0(2(2(0(x0)))))
1(0(1(0(2(x0)))))	→	1(0(2(2(2(x0)))))
1(0(1(0(2(x0)))))	→	1(1(0(2(2(x0)))))
1(0(1(0(2(x0)))))	→	1(2(0(2(2(x0)))))
1(0(1(0(2(x0)))))	→	1(2(1(0(2(x0)))))
1(0(1(0(2(x0)))))	→	1(2(2(0(2(x0)))))
1(0(1(0(2(x0)))))	→	1(2(2(2(0(x0)))))
1(0(1(0(2(x0)))))	→	2(0(1(2(2(x0)))))
1(0(1(0(2(x0)))))	→	2(0(2(1(2(x0)))))
1(0(1(0(2(x0)))))	→	2(1(0(2(2(x0)))))
1(0(1(0(2(x0)))))	→	2(1(2(0(2(x0)))))
1(0(1(0(2(x0)))))	→	2(1(2(2(0(x0)))))
1(0(1(0(2(x0)))))	→	2(2(0(1(2(x0)))))
1(0(1(0(2(x0)))))	→	2(2(1(0(2(x0)))))
1(0(1(0(2(x0)))))	→	2(2(1(2(0(x0)))))
1(0(1(0(2(x0)))))	→	2(2(2(1(0(x0)))))
1(0(2(0(2(x0)))))	→	1(0(2(2(2(x0)))))
1(0(2(0(2(x0)))))	→	1(2(0(2(2(x0)))))
1(0(2(0(2(x0)))))	→	1(2(2(0(2(x0)))))
1(0(2(0(2(x0)))))	→	1(2(2(2(0(x0)))))
1(0(2(0(2(x0)))))	→	2(1(0(2(2(x0)))))
1(0(2(0(2(x0)))))	→	2(2(1(0(2(x0)))))
1(1(2(0(2(x0)))))	→	0(1(2(2(2(x0)))))
1(1(2(0(2(x0)))))	→	0(2(1(2(2(x0)))))
1(1(2(0(2(x0)))))	→	0(2(2(1(2(x0)))))
1(1(2(0(2(x0)))))	→	1(0(0(2(2(x0)))))
1(1(2(0(2(x0)))))	→	1(0(1(2(2(x0)))))
1(1(2(0(2(x0)))))	→	1(0(2(0(2(x0)))))
1(1(2(0(2(x0)))))	→	1(0(2(1(2(x0)))))
1(1(2(0(2(x0)))))	→	1(0(2(2(0(x0)))))
1(1(2(0(2(x0)))))	→	1(0(2(2(2(x0)))))
1(1(2(0(2(x0)))))	→	1(1(0(2(2(x0)))))
1(1(2(0(2(x0)))))	→	1(2(0(2(2(x0)))))
1(1(2(0(2(x0)))))	→	1(2(1(0(2(x0)))))
1(1(2(0(2(x0)))))	→	1(2(2(0(2(x0)))))
1(1(2(0(2(x0)))))	→	1(2(2(2(0(x0)))))
1(1(2(0(2(x0)))))	→	2(0(1(2(2(x0)))))
1(1(2(0(2(x0)))))	→	2(1(0(2(2(x0)))))
1(1(2(0(2(x0)))))	→	2(1(2(0(2(x0)))))
1(1(2(0(2(x0)))))	→	2(2(0(1(2(x0)))))
1(1(2(0(2(x0)))))	→	2(2(1(0(2(x0)))))
1(1(2(0(2(x0)))))	→	2(2(2(1(0(x0)))))
1(2(2(0(2(x0)))))	→	1(0(2(2(2(x0)))))
2(0(1(0(2(x0)))))	→	2(0(1(2(2(x0)))))
2(0(1(0(2(x0)))))	→	2(0(2(1(2(x0)))))
2(0(1(0(2(x0)))))	→	2(1(0(2(2(x0)))))
2(0(1(0(2(x0)))))	→	2(1(2(0(2(x0)))))
2(0(1(0(2(x0)))))	→	2(1(2(2(0(x0)))))
2(0(1(0(2(x0)))))	→	2(2(0(1(2(x0)))))
2(0(1(0(2(x0)))))	→	2(2(1(0(2(x0)))))
2(0(1(0(2(x0)))))	→	2(2(1(2(0(x0)))))
2(0(1(0(2(x0)))))	→	2(2(2(1(0(x0)))))
2(1(1(0(2(x0)))))	→	2(0(1(0(2(x0)))))
2(1(1(0(2(x0)))))	→	2(0(2(1(2(x0)))))
2(1(1(0(2(x0)))))	→	2(1(2(0(2(x0)))))
2(1(1(0(2(x0)))))	→	2(2(1(0(2(x0)))))
2(1(2(0(2(x0)))))	→	2(0(1(2(2(x0)))))
2(1(2(0(2(x0)))))	→	2(1(0(2(2(x0)))))
2(1(2(0(2(x0)))))	→	2(2(1(0(2(x0)))))
2(1(2(0(2(x0)))))	→	2(2(2(1(0(x0)))))

Proof

1 Rule Removal

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

[0(x₁)]	=	2 · x₁ + -∞
[2(x₁)]	=	0 · x₁ + -∞
[1(x₁)]	=	2 · x₁ + -∞

the rules

0(1(2(0(2(x0)))))	→	0(1(0(2(2(x0)))))
0(1(2(0(2(x0)))))	→	0(1(1(2(2(x0)))))
0(1(2(0(2(x0)))))	→	0(2(1(0(2(x0)))))
0(1(2(0(2(x0)))))	→	0(2(2(1(0(x0)))))
1(1(2(0(2(x0)))))	→	1(0(0(2(2(x0)))))
1(1(2(0(2(x0)))))	→	1(0(1(2(2(x0)))))
1(1(2(0(2(x0)))))	→	1(0(2(0(2(x0)))))
1(1(2(0(2(x0)))))	→	1(0(2(1(2(x0)))))
1(1(2(0(2(x0)))))	→	1(0(2(2(0(x0)))))
1(1(2(0(2(x0)))))	→	1(1(0(2(2(x0)))))
1(1(2(0(2(x0)))))	→	1(2(1(0(2(x0)))))
1(2(2(0(2(x0)))))	→	1(0(2(2(2(x0)))))
2(1(1(0(2(x0)))))	→	2(0(1(0(2(x0)))))
2(1(2(0(2(x0)))))	→	2(0(1(2(2(x0)))))
2(1(2(0(2(x0)))))	→	2(1(0(2(2(x0)))))
2(1(2(0(2(x0)))))	→	2(2(1(0(2(x0)))))
2(1(2(0(2(x0)))))	→	2(2(2(1(0(x0)))))

remain.

1.1 Bounds

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

final states:

{44, 43, 42, 41, 39, 36, 35, 34, 30, 26, 23, 21, 19, 14, 10, 7, 1}

transitions:

10 → 15

41 → 28

41 → 3

39 → 3

1 → 15

44 → 28

44 → 3

36 → 8

36 → 27

14 → 15

7 → 15

42 → 28

42 → 3

43 → 28

43 → 3

f3₀ → 2

0₀(37) → 38

0₀(5) → 20

0₀(9) → 7

0₀(8) → 22

0₀(2) → 15

0₀(32) → 33

0₀(12) → 40

0₀(18) → 14

0₀(6) → 1

0₀(24) → 25

0₀(4) → 5

0₀(3) → 11

0₀(13) → 10

0₀(28) → 29

2₀(11) → 24

2₀(22) → 41

2₀(3) → 4

2₀(18) → 44

2₀(15) → 31

2₀(40) → 39

2₀(16) → 17

2₀(2) → 3

2₀(4) → 37

2₀(31) → 32

2₀(27) → 28

2₀(12) → 13

2₀(13) → 43

2₀(17) → 18

2₀(6) → 42

1₀(22) → 21

1₀(38) → 36

1₀(8) → 9

1₀(15) → 16

1₀(29) → 26

1₀(6) → 34

1₀(13) → 35

1₀(33) → 30

1₀(5) → 6

1₀(20) → 19

1₀(11) → 12

1₀(25) → 23

1₀(3) → 27

1₀(4) → 8

10	→	15
41	→	28
41	→	3
39	→	3
1	→	15
44	→	28
44	→	3
36	→	8
36	→	27
14	→	15
7	→	15
42	→	28
42	→	3
43	→	28
43	→	3
f3₀	→	2
0₀(37)	→	38
0₀(5)	→	20
0₀(9)	→	7
0₀(8)	→	22
0₀(2)	→	15
0₀(32)	→	33
0₀(12)	→	40
0₀(18)	→	14
0₀(6)	→	1
0₀(24)	→	25
0₀(4)	→	5
0₀(3)	→	11
0₀(13)	→	10
0₀(28)	→	29
2₀(11)	→	24
2₀(22)	→	41
2₀(3)	→	4
2₀(18)	→	44
2₀(15)	→	31
2₀(40)	→	39
2₀(16)	→	17
2₀(2)	→	3
2₀(4)	→	37
2₀(31)	→	32
2₀(27)	→	28
2₀(12)	→	13
2₀(13)	→	43
2₀(17)	→	18
2₀(6)	→	42
1₀(22)	→	21
1₀(38)	→	36
1₀(8)	→	9
1₀(15)	→	16
1₀(29)	→	26
1₀(6)	→	34
1₀(13)	→	35
1₀(33)	→	30
1₀(5)	→	6
1₀(20)	→	19
1₀(11)	→	12
1₀(25)	→	23
1₀(3)	→	27
1₀(4)	→	8