YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

p(0(x0))	→	0(s(s(p(x0))))
p(s(x0))	→	x0
p(p(s(x0)))	→	p(x0)
f(s(x0))	→	p(s(g(p(s(s(x0))))))
g(s(x0))	→	p(p(s(s(s(j(s(p(s(p(s(x0)))))))))))
j(s(x0))	→	p(s(s(p(s(f(p(s(p(p(s(x0)))))))))))
half(0(x0))	→	0(s(s(half(p(s(p(s(x0))))))))
half(s(s(x0)))	→	s(half(p(p(s(s(x0))))))
rd(0(x0))	→	0(s(0(0(0(0(s(0(rd(x0)))))))))

Proof

1 Bounds

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

final states:

{38, 35, 31, 22, 12, 6, 3, 2, 1}

transitions:

23 → 25

29 → 22

89 → 109

87 → 89

80 → 82

10 → 6

15 → 71

96 → 6

96 → 10

84 → 74

136 → 112

18 → 12

18 → 54

120 → 91

108 → 96

31 → 32

31 → 37

1 → 112

1 → 84

1 → 3

1 → 25

1 → 23

1 → 48

1 → 136

71 → 73

71 → 83

13 → 15

73 → 87

26 → 28

38 → 39

6 → 117

6 → 79

6 → 28

6 → 26

6 → 77

6 → 115

109 → 111

109 → 135

54 → 12

82 → 17

2 → 13

2 → 47

2 → 36

2 → 56

2 → 112

2 → 84

2 → 3

2 → 25

2 → 23

2 → 48

2 → 136

118 → 120

93 → 95

93 → 107

112 → 114

77 → 79

7 → 9

7 → 55

35 → 32

35 → 37

115 → 117

48 → 23

74 → 76

92 → 96

92 → 108

19 → 21

19 → 53

56 → 36

p₂(113) → 114

p₂(116) → 117

p₂(110) → 111

p₂(83) → 84

p₂(107) → 108

p₂(119) → 120

p₂(111) → 112

p₁(73) → 74

p₁(47) → 48

p₁(95) → 96

p₁(75) → 76

p₁(72) → 73

p₁(53) → 54

p₁(81) → 82

p₁(78) → 79

p₁(88) → 89

p₁(94) → 95

p₁(55) → 56

s₁(79) → 80

s₁(77) → 78

s₁(80) → 81

s₁(71) → 72

s₁(93) → 94

s₁(74) → 75

s₁(92) → 93

s₁(89) → 90

s₁(87) → 88

s₁(91) → 92

rd₀(2) → 39

s₂(112) → 113

s₂(118) → 119

s₂(115) → 116

s₂(117) → 118

s₂(109) → 110

p₃(135) → 136

half₀(15) → 32

half₀(36) → 37

f₂(114) → 115

j₀(16) → 17

j₁(90) → 91

f₀(25) → 26

0₀(46) → 38

0₀(41) → 42

0₀(44) → 45

0₀(39) → 40

0₀(42) → 43

0₀(5) → 1

0₀(43) → 44

0₀(34) → 31

s₀(2) → 7

s₀(45) → 46

s₀(26) → 27

s₀(19) → 20

s₀(32) → 33

s₀(28) → 29

s₀(37) → 35

s₀(4) → 5

s₀(18) → 19

s₀(23) → 24

s₀(13) → 14

s₀(17) → 18

s₀(15) → 16

s₀(33) → 34

s₀(3) → 4

s₀(10) → 11

s₀(29) → 30

s₀(40) → 41

s₀(7) → 8

f8₀ → 2

p₀(21) → 12

p₀(8) → 9

p₀(11) → 6

p₀(27) → 28

p₀(7) → 13

p₀(13) → 23

p₀(20) → 21

p₀(9) → 36

p₀(14) → 15

p₀(30) → 22

p₀(24) → 25

p₀(2) → 3

g₀(9) → 10

f₁(76) → 77

23	→	25
29	→	22
89	→	109
87	→	89
80	→	82
10	→	6
15	→	71
96	→	6
96	→	10
84	→	74
136	→	112
18	→	12
18	→	54
120	→	91
108	→	96
31	→	32
31	→	37
1	→	112
1	→	84
1	→	3
1	→	25
1	→	23
1	→	48
1	→	136
71	→	73
71	→	83
13	→	15
73	→	87
26	→	28
38	→	39
6	→	117
6	→	79
6	→	28
6	→	26
6	→	77
6	→	115
109	→	111
109	→	135
54	→	12
82	→	17
2	→	13
2	→	47
2	→	36
2	→	56
2	→	112
2	→	84
2	→	3
2	→	25
2	→	23
2	→	48
2	→	136
118	→	120
93	→	95
93	→	107
112	→	114
77	→	79
7	→	9
7	→	55
35	→	32
35	→	37
115	→	117
48	→	23
74	→	76
92	→	96
92	→	108
19	→	21
19	→	53
56	→	36
p₂(113)	→	114
p₂(116)	→	117
p₂(110)	→	111
p₂(83)	→	84
p₂(107)	→	108
p₂(119)	→	120
p₂(111)	→	112
p₁(73)	→	74
p₁(47)	→	48
p₁(95)	→	96
p₁(75)	→	76
p₁(72)	→	73
p₁(53)	→	54
p₁(81)	→	82
p₁(78)	→	79
p₁(88)	→	89
p₁(94)	→	95
p₁(55)	→	56
s₁(79)	→	80
s₁(77)	→	78
s₁(80)	→	81
s₁(71)	→	72
s₁(93)	→	94
s₁(74)	→	75
s₁(92)	→	93
s₁(89)	→	90
s₁(87)	→	88
s₁(91)	→	92
rd₀(2)	→	39
s₂(112)	→	113
s₂(118)	→	119
s₂(115)	→	116
s₂(117)	→	118
s₂(109)	→	110
p₃(135)	→	136
half₀(15)	→	32
half₀(36)	→	37
f₂(114)	→	115
j₀(16)	→	17
j₁(90)	→	91
f₀(25)	→	26
0₀(46)	→	38
0₀(41)	→	42
0₀(44)	→	45
0₀(39)	→	40
0₀(42)	→	43
0₀(5)	→	1
0₀(43)	→	44
0₀(34)	→	31
s₀(2)	→	7
s₀(45)	→	46
s₀(26)	→	27
s₀(19)	→	20
s₀(32)	→	33
s₀(28)	→	29
s₀(37)	→	35
s₀(4)	→	5
s₀(18)	→	19
s₀(23)	→	24
s₀(13)	→	14
s₀(17)	→	18
s₀(15)	→	16
s₀(33)	→	34
s₀(3)	→	4
s₀(10)	→	11
s₀(29)	→	30
s₀(40)	→	41
s₀(7)	→	8
f8₀	→	2
p₀(21)	→	12
p₀(8)	→	9
p₀(11)	→	6
p₀(27)	→	28
p₀(7)	→	13
p₀(13)	→	23
p₀(20)	→	21
p₀(9)	→	36
p₀(14)	→	15
p₀(30)	→	22
p₀(24)	→	25
p₀(2)	→	3
g₀(9)	→	10
f₁(76)	→	77