YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

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

Proof

1 String Reversal

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

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

1.1 Bounds

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

final states:

{12, 1}

transitions:

33 → 89

96 → 86

9 → 26

37 → 78

90 → 79

62 → 27

62 → 63

1 → 5

1 → 3

1 → 103

38 → 34

36 → 6

36 → 37

36 → 104

6 → 52

88 → 53

88 → 95

88 → 79

88 → 90

12 → 5

12 → 3

104 → 27

100 → 79

30 → 99

64 → 60

0₁(30) → 31

0₁(37) → 38

0₁(33) → 34

0₁(56) → 57

0₁(59) → 60

0₁(63) → 64

2₂(87) → 88

2₂(79) → 80

2₂(84) → 85

1₁(26) → 27

1₁(34) → 35

1₁(60) → 61

1₁(55) → 56

1₁(29) → 30

1₁(28) → 29

1₁(57) → 58

1₁(54) → 55

1₁(31) → 32

1₁(103) → 104

1₁(52) → 53

f3₀ → 2

2₀(8) → 9

2₀(14) → 12

2₀(11) → 1

2₀(3) → 4

1₂(78) → 79

1₂(99) → 100

1₂(86) → 87

1₂(89) → 90

1₂(83) → 84

1₂(80) → 81

1₂(81) → 82

0₂(95) → 96

0₂(85) → 86

0₂(82) → 83

0₀(9) → 10

0₀(1) → 13

0₀(6) → 7

2₁(61) → 62

2₁(53) → 54

2₁(32) → 33

2₁(27) → 28

2₁(35) → 36

2₁(58) → 59

1₀(10) → 11

1₀(13) → 14

1₀(5) → 6

1₀(2) → 3

1₀(4) → 5

1₀(7) → 8

33	→	89
96	→	86
9	→	26
37	→	78
90	→	79
62	→	27
62	→	63
1	→	5
1	→	3
1	→	103
38	→	34
36	→	6
36	→	37
36	→	104
6	→	52
88	→	53
88	→	95
88	→	79
88	→	90
12	→	5
12	→	3
104	→	27
100	→	79
30	→	99
64	→	60
0₁(30)	→	31
0₁(37)	→	38
0₁(33)	→	34
0₁(56)	→	57
0₁(59)	→	60
0₁(63)	→	64
2₂(87)	→	88
2₂(79)	→	80
2₂(84)	→	85
1₁(26)	→	27
1₁(34)	→	35
1₁(60)	→	61
1₁(55)	→	56
1₁(29)	→	30
1₁(28)	→	29
1₁(57)	→	58
1₁(54)	→	55
1₁(31)	→	32
1₁(103)	→	104
1₁(52)	→	53
f3₀	→	2
2₀(8)	→	9
2₀(14)	→	12
2₀(11)	→	1
2₀(3)	→	4
1₂(78)	→	79
1₂(99)	→	100
1₂(86)	→	87
1₂(89)	→	90
1₂(83)	→	84
1₂(80)	→	81
1₂(81)	→	82
0₂(95)	→	96
0₂(85)	→	86
0₂(82)	→	83
0₀(9)	→	10
0₀(1)	→	13
0₀(6)	→	7
2₁(61)	→	62
2₁(53)	→	54
2₁(32)	→	33
2₁(27)	→	28
2₁(35)	→	36
2₁(58)	→	59
1₀(10)	→	11
1₀(13)	→	14
1₀(5)	→	6
1₀(2)	→	3
1₀(4)	→	5
1₀(7)	→	8