YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

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

Proof

1 String Reversal

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

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

1.1 Bounds

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

final states:

{99, 84, 68, 53, 36, 19, 1}

transitions:

84 → 101

84 → 23

84 → 38

84 → 37

99 → 69

99 → 20

1 → 69

1 → 20

36 → 22

36 → 37

53 → 85

53 → 3

68 → 37

19 → 37

1₀(104) → 105

1₀(78) → 79

1₀(14) → 15

1₀(79) → 80

1₀(51) → 52

1₀(70) → 71

1₀(5) → 6

1₀(24) → 25

1₀(26) → 27

1₀(76) → 77

1₀(39) → 40

1₀(54) → 55

1₀(58) → 59

1₀(38) → 85

1₀(49) → 50

1₀(10) → 11

1₀(2) → 3

1₀(31) → 32

1₀(92) → 93

1₀(25) → 26

1₀(43) → 44

1₀(42) → 43

1₀(73) → 74

1₀(77) → 78

1₀(32) → 33

1₀(30) → 31

1₀(21) → 54

2₀(111) → 112

2₀(59) → 60

2₀(82) → 83

2₀(20) → 21

2₀(17) → 18

2₀(37) → 69

2₀(33) → 34

2₀(85) → 86

2₀(45) → 46

2₀(8) → 9

2₀(93) → 94

2₀(69) → 70

2₀(102) → 103

2₀(2) → 20

2₀(12) → 13

2₀(47) → 48

2₀(90) → 91

2₀(18) → 1

2₀(23) → 24

2₀(112) → 99

2₀(101) → 102

2₀(65) → 66

2₀(103) → 104

2₀(55) → 56

2₀(60) → 61

2₀(4) → 5

2₀(109) → 110

2₀(89) → 90

2₀(66) → 67

2₀(95) → 96

2₀(11) → 12

2₀(38) → 39

2₀(108) → 109

2₀(96) → 97

2₀(44) → 45

2₀(46) → 47

2₀(62) → 63

2₀(50) → 51

2₀(3) → 4

2₀(67) → 53

2₀(48) → 49

2₀(94) → 95

2₀(105) → 106

2₀(34) → 35

f3₀ → 2

0₀(64) → 65

0₀(22) → 23

0₀(97) → 98

0₀(75) → 76

0₀(71) → 72

0₀(100) → 101

0₀(107) → 108

0₀(41) → 42

0₀(110) → 111

0₀(56) → 57

0₀(15) → 16

0₀(29) → 30

0₀(70) → 100

0₀(6) → 7

0₀(13) → 14

0₀(63) → 64

0₀(88) → 89

0₀(80) → 81

0₀(86) → 87

0₀(81) → 82

0₀(106) → 107

0₀(87) → 88

0₀(98) → 84

0₀(28) → 29

0₀(91) → 92

0₀(74) → 75

0₀(35) → 19

0₀(2) → 37

0₀(21) → 22

0₀(72) → 73

0₀(37) → 38

0₀(61) → 62

0₀(57) → 58

0₀(52) → 36

0₀(9) → 10

0₀(27) → 28

0₀(83) → 68

0₀(40) → 41

0₀(16) → 17

0₀(7) → 8

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