YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

1(4(x0))	→	3(1(1(2(2(4(x0))))))
5(4(x0))	→	4(2(3(1(1(1(x0))))))
0(3(0(x0)))	→	2(1(1(0(2(0(x0))))))
0(5(5(x0)))	→	1(0(1(3(4(2(x0))))))
1(5(4(x0)))	→	0(2(5(2(0(4(x0))))))
3(5(4(x0)))	→	4(1(3(4(2(3(x0))))))
4(1(4(x0)))	→	3(3(2(2(3(1(x0))))))
5(4(0(x0)))	→	2(4(0(4(4(0(x0))))))
5(4(0(x0)))	→	5(1(5(2(1(0(x0))))))
5(4(4(x0)))	→	4(1(1(3(2(4(x0))))))
5(5(4(x0)))	→	3(4(4(1(2(2(x0))))))
0(5(5(0(x0))))	→	0(2(0(0(3(0(x0))))))
0(5(5(4(x0))))	→	0(1(3(4(3(4(x0))))))
1(4(5(4(x0))))	→	0(4(5(0(2(1(x0))))))
1(4(5(5(x0))))	→	0(0(1(3(4(1(x0))))))
2(5(4(0(x0))))	→	0(4(1(2(4(0(x0))))))
4(3(0(5(x0))))	→	3(3(2(3(5(5(x0))))))
5(4(0(0(x0))))	→	1(0(4(0(2(2(x0))))))
5(4(0(2(x0))))	→	3(0(4(5(0(2(x0))))))

Proof

1 String Reversal

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

4(1(x0))	→	4(2(2(1(1(3(x0))))))
4(5(x0))	→	1(1(1(3(2(4(x0))))))
0(3(0(x0)))	→	0(2(0(1(1(2(x0))))))
5(5(0(x0)))	→	2(4(3(1(0(1(x0))))))
4(5(1(x0)))	→	4(0(2(5(2(0(x0))))))
4(5(3(x0)))	→	3(2(4(3(1(4(x0))))))
4(1(4(x0)))	→	1(3(2(2(3(3(x0))))))
0(4(5(x0)))	→	0(4(4(0(4(2(x0))))))
0(4(5(x0)))	→	0(1(2(5(1(5(x0))))))
4(4(5(x0)))	→	4(2(3(1(1(4(x0))))))
4(5(5(x0)))	→	2(2(1(4(4(3(x0))))))
0(5(5(0(x0))))	→	0(3(0(0(2(0(x0))))))
4(5(5(0(x0))))	→	4(3(4(3(1(0(x0))))))
4(5(4(1(x0))))	→	1(2(0(5(4(0(x0))))))
5(5(4(1(x0))))	→	1(4(3(1(0(0(x0))))))
0(4(5(2(x0))))	→	0(4(2(1(4(0(x0))))))
5(0(3(4(x0))))	→	5(5(3(2(3(3(x0))))))
0(0(4(5(x0))))	→	2(2(0(4(0(1(x0))))))
2(0(4(5(x0))))	→	2(0(5(4(0(3(x0))))))

1.1 Bounds

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

final states:

{92, 88, 85, 81, 76, 71, 66, 62, 57, 53, 47, 42, 37, 32, 26, 20, 14, 8, 1}

transitions:

32 → 9

81 → 27

103 → 62

57 → 9

37 → 9

20 → 48

62 → 27

1 → 9

8 → 9

71 → 9

26 → 9

76 → 48

88 → 77

88 → 27

53 → 9

66 → 9

14 → 93

14 → 27

63 → 97

85 → 48

42 → 27

47 → 27

92 → 28

92 → 15

2₁(101) → 102

2₁(97) → 98

1₀(51) → 52

1₀(16) → 17

1₀(11) → 12

1₀(41) → 37

1₀(3) → 4

1₀(33) → 54

1₀(77) → 78

1₀(48) → 49

1₀(80) → 76

1₀(9) → 33

1₀(59) → 60

1₀(27) → 67

1₀(75) → 71

1₀(72) → 82

1₀(15) → 16

1₀(13) → 8

1₀(4) → 5

1₀(22) → 23

1₀(2) → 21

1₀(12) → 13

3₀(2) → 3

3₀(78) → 79

3₀(36) → 32

3₀(23) → 24

3₀(54) → 55

3₀(64) → 65

3₀(67) → 68

3₀(69) → 70

3₀(39) → 86

3₀(33) → 34

3₀(3) → 38

3₀(10) → 11

3₀(40) → 41

2₀(91) → 88

2₀(35) → 36

2₀(38) → 39

2₀(6) → 7

2₀(60) → 61

2₀(55) → 56

2₀(90) → 91

2₀(29) → 30

2₀(18) → 19

2₀(82) → 83

2₀(9) → 10

2₀(25) → 20

2₀(96) → 92

2₀(50) → 51

2₀(61) → 57

2₀(27) → 28

2₀(74) → 75

2₀(5) → 6

2₀(2) → 15

2₀(39) → 40

0₀(19) → 14

0₀(17) → 18

0₀(21) → 22

0₀(46) → 42

0₀(63) → 64

0₀(27) → 77

0₀(28) → 63

0₀(84) → 81

0₀(43) → 44

0₀(89) → 90

0₀(52) → 47

0₀(3) → 93

0₀(30) → 31

0₀(65) → 62

0₀(95) → 96

0₀(2) → 27

0₀(73) → 74

5₀(87) → 85

5₀(72) → 73

5₀(94) → 95

5₀(49) → 50

5₀(2) → 48

5₀(28) → 29

5₀(86) → 87

f6₀ → 2

4₀(2) → 9

4₀(56) → 53

4₀(79) → 80

4₀(24) → 25

4₀(3) → 58

4₀(83) → 84

4₀(70) → 66

4₀(7) → 1

4₀(15) → 43

4₀(27) → 72

4₀(93) → 94

4₀(45) → 46

4₀(22) → 89

4₀(34) → 35

4₀(44) → 45

4₀(31) → 26

4₀(58) → 59

4₀(68) → 69

1₁(98) → 99

1₁(99) → 100

0₁(100) → 101

0₁(102) → 103

32	→	9
81	→	27
103	→	62
57	→	9
37	→	9
20	→	48
62	→	27
1	→	9
8	→	9
71	→	9
26	→	9
76	→	48
88	→	77
88	→	27
53	→	9
66	→	9
14	→	93
14	→	27
63	→	97
85	→	48
42	→	27
47	→	27
92	→	28
92	→	15
2₁(101)	→	102
2₁(97)	→	98
1₀(51)	→	52
1₀(16)	→	17
1₀(11)	→	12
1₀(41)	→	37
1₀(3)	→	4
1₀(33)	→	54
1₀(77)	→	78
1₀(48)	→	49
1₀(80)	→	76
1₀(9)	→	33
1₀(59)	→	60
1₀(27)	→	67
1₀(75)	→	71
1₀(72)	→	82
1₀(15)	→	16
1₀(13)	→	8
1₀(4)	→	5
1₀(22)	→	23
1₀(2)	→	21
1₀(12)	→	13
3₀(2)	→	3
3₀(78)	→	79
3₀(36)	→	32
3₀(23)	→	24
3₀(54)	→	55
3₀(64)	→	65
3₀(67)	→	68
3₀(69)	→	70
3₀(39)	→	86
3₀(33)	→	34
3₀(3)	→	38
3₀(10)	→	11
3₀(40)	→	41
2₀(91)	→	88
2₀(35)	→	36
2₀(38)	→	39
2₀(6)	→	7
2₀(60)	→	61
2₀(55)	→	56
2₀(90)	→	91
2₀(29)	→	30
2₀(18)	→	19
2₀(82)	→	83
2₀(9)	→	10
2₀(25)	→	20
2₀(96)	→	92
2₀(50)	→	51
2₀(61)	→	57
2₀(27)	→	28
2₀(74)	→	75
2₀(5)	→	6
2₀(2)	→	15
2₀(39)	→	40
0₀(19)	→	14
0₀(17)	→	18
0₀(21)	→	22
0₀(46)	→	42
0₀(63)	→	64
0₀(27)	→	77
0₀(28)	→	63
0₀(84)	→	81
0₀(43)	→	44
0₀(89)	→	90
0₀(52)	→	47
0₀(3)	→	93
0₀(30)	→	31
0₀(65)	→	62
0₀(95)	→	96
0₀(2)	→	27
0₀(73)	→	74
5₀(87)	→	85
5₀(72)	→	73
5₀(94)	→	95
5₀(49)	→	50
5₀(2)	→	48
5₀(28)	→	29
5₀(86)	→	87
f6₀	→	2
4₀(2)	→	9
4₀(56)	→	53
4₀(79)	→	80
4₀(24)	→	25
4₀(3)	→	58
4₀(83)	→	84
4₀(70)	→	66
4₀(7)	→	1
4₀(15)	→	43
4₀(27)	→	72
4₀(93)	→	94
4₀(45)	→	46
4₀(22)	→	89
4₀(34)	→	35
4₀(44)	→	45
4₀(31)	→	26
4₀(58)	→	59
4₀(68)	→	69
1₁(98)	→	99
1₁(99)	→	100
0₁(100)	→	101
0₁(102)	→	103